Files

 master

/

pretyping

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

maximedenes

Merge PR coq#6767: [ci] add elpi

Feb 21, 2018

cec8523 · Feb 21, 2018

History

History

This branch is 21541 commits behind coq/coq:master.

/

pretyping

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
arguments_renaming.ml		arguments_renaming.ml	Using a dedicated type for Lib.abstr_info.	Dec 30, 2017
arguments_renaming.mli		arguments_renaming.mli	[api] Move structures deprecated in the API to the core.	Nov 6, 2017
cases.ml		cases.ml	Moving the argument of CProdN/CLambdaN from binder_expr to local_bind…	Feb 20, 2018
cases.mli		cases.mli	[api] A few more minor deprecation notices.	Nov 22, 2017
cbv.ml		cbv.ml	[cbv] Fix evaluation of cofixpoints under primitive projections.	Jan 29, 2018
cbv.mli		cbv.mli	[api] Remove aliases of Evar.t	Nov 26, 2017
classops.ml		classops.ml	[proof] Embed evar_map in RefinerError exception.	Dec 11, 2017
classops.mli		classops.mli	[proof] Embed evar_map in RefinerError exception.	Dec 11, 2017
coercion.ml		coercion.ml	Efficient fresh name generation relying on sets.	Sep 28, 2017
coercion.mli		coercion.mli	Bump year in headers.	Jul 4, 2017
constr_matching.ml		constr_matching.ml	Fix context handling of fix and cofix in Ltac subterm matching.	Jan 19, 2018
constr_matching.mli		constr_matching.mli	Remove deprecated option Tactic Compat Context.	Dec 11, 2017
detyping.ml		detyping.ml	detype_case predicate is not optional	Feb 14, 2018
detyping.mli		detyping.mli	In printing, factorizing "match" clauses with same right-hand side.	Dec 12, 2017
doc.tex		doc.tex	ocamlweb	Nov 30, 1999
evarconv.ml		evarconv.ml	Simplification: cumulativity information is variance information.	Feb 10, 2018
evarconv.mli		evarconv.mli	[api] Move structures deprecated in the API to the core.	Nov 6, 2017
evardefine.ml		evardefine.ml	Reductionops.nf_* now take an environment.	Feb 2, 2018
evardefine.mli		evardefine.mli	[api] Move structures deprecated in the API to the core.	Nov 6, 2017
evarsolve.ml		evarsolve.ml	[api] Deprecate Term destructors, move to Constr	Nov 22, 2017
evarsolve.mli		evarsolve.mli	[api] Remove aliases of Evar.t	Nov 26, 2017
find_subterm.ml		find_subterm.ml	[api] Another large deprecation, Nameops	Nov 13, 2017
find_subterm.mli		find_subterm.mli	Bump year in headers.	Jul 4, 2017
geninterp.ml		geninterp.ml	[api] Miscellaneous consolidation + moves to engine.	Nov 21, 2017
geninterp.mli		geninterp.mli	[api] Miscellaneous consolidation + moves to engine.	Nov 21, 2017
glob_ops.ml		glob_ops.ml	Using an "as" clause when needed for printing irrefutable patterns.	Feb 20, 2018
glob_ops.mli		glob_ops.mli	Using an "as" clause when needed for printing irrefutable patterns.	Feb 20, 2018
indrec.ml		indrec.ml	[api] Another large deprecation, Nameops	Nov 13, 2017
indrec.mli		indrec.mli	[api] Move structures deprecated in the API to the core.	Nov 6, 2017
inductiveops.ml		inductiveops.ml	Use specialized function for inductive subtyping inference.	Feb 11, 2018
inductiveops.mli		inductiveops.mli	Use specialized function for inductive subtyping inference.	Feb 11, 2018
inferCumulativity.ml		inferCumulativity.ml	Cleaner treatment of parameters in inferCumulativity	Feb 16, 2018
inferCumulativity.mli		inferCumulativity.mli	Use specialized function for inductive subtyping inference.	Feb 11, 2018
locusops.ml		locusops.ml	Bump year in headers.	Jul 4, 2017
locusops.mli		locusops.mli	Bump year in headers.	Jul 4, 2017
ltac_pretype.ml		ltac_pretype.ml	[general] Remove Econstr dependency from intf	Oct 25, 2017
miscops.ml		miscops.ml	Proper nametab handling of global universe names	Dec 1, 2017
miscops.mli		miscops.mli	Bump year in headers.	Jul 4, 2017
nativenorm.ml		nativenorm.ml	[native_compute] Fix handling of evars in conversion	Feb 5, 2018
nativenorm.mli		nativenorm.mli	Add native compute profiling, BZ#5170	Aug 17, 2017
patternops.ml		patternops.ml	Use r.(p) syntax to print primitive projections.	Jan 30, 2018
patternops.mli		patternops.mli	Fixing coq#5401 (printing of patterns with bound anonymous variables).	Oct 28, 2017
pretype_errors.ml		pretype_errors.ml	[api] Remove aliases of Evar.t	Nov 26, 2017
pretype_errors.mli		pretype_errors.mli	[api] Remove aliases of Evar.t	Nov 26, 2017
pretyping.ml		pretyping.ml	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Feb 19, 2018
pretyping.mli		pretyping.mli	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Feb 19, 2018
pretyping.mllib		pretyping.mllib	Use specialized function for inductive subtyping inference.	Feb 11, 2018
program.ml		program.ml	Bump year in headers.	Jul 4, 2017
program.mli		program.mli	Bump year in headers.	Jul 4, 2017
recordops.ml		recordops.ml	More detailed error messages for Canonical Structure, coq#6398	Feb 6, 2018
recordops.mli		recordops.mli	[api] Move structures deprecated in the API to the core.	Nov 6, 2017
redops.ml		redops.ml	Bump year in headers.	Jul 4, 2017
redops.mli		redops.mli	Bump year in headers.	Jul 4, 2017
reductionops.ml		reductionops.ml	[get_cumulativity_constraints] allowing further code sharing.	Feb 10, 2018
reductionops.mli		reductionops.mli	Reductionops.nf_* now take an environment.	Feb 2, 2018
retyping.ml		retyping.ml	[lib] Rename Profile to CProfile	Dec 9, 2017
retyping.mli		retyping.mli	Adding a variant get_truncation_family_of of get_sort_family_of.	Nov 28, 2017
tacred.ml		tacred.ml	Reductionops.nf_* now take an environment.	Feb 2, 2018
tacred.mli		tacred.mli	[general] Remove Econstr dependency from intf	Oct 25, 2017
typeclasses.ml		typeclasses.ml	Using a dedicated type for Lib.abstr_info.	Dec 30, 2017
typeclasses.mli		typeclasses.mli	Remove the local polymorphic flag hack.	Dec 27, 2017
typeclasses_errors.ml		typeclasses_errors.ml	Bump year in headers.	Jul 4, 2017
typeclasses_errors.mli		typeclasses_errors.mli	Bump year in headers.	Jul 4, 2017
typing.ml		typing.ml	Define EConstr version of [push_rec_types].	Jan 19, 2018
typing.mli		typing.mli	Use r.(p) syntax to print primitive projections.	Jan 30, 2018
unification.ml		unification.ml	Reductionops.nf_* now take an environment.	Feb 2, 2018
unification.mli		unification.mli	[api] Move structures deprecated in the API to the core.	Nov 6, 2017
univdecls.ml		univdecls.ml	Fix interpretation of global universes in univdecl constraints.	Nov 25, 2017
univdecls.mli		univdecls.mli	Allow declaring universe constraints at definition level.	Sep 19, 2017
vnorm.ml		vnorm.ml	Merge PR coq#1082: Fixing Print for inductive types with let-in in pa…	Feb 12, 2018
vnorm.mli		vnorm.mli	Bump year in headers.	Jul 4, 2017
View all files