coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès

2017-03-21	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias
	In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
2017-02-14	Merge branch 'master'.	Pierre-Marie Pédrot

2017-02-14	Missing API in EConstr.	Enrico Tassi

2017-02-14	Moving evar-normalization functions to EConstr.	Pierre-Marie Pédrot
	This removes code duplication between Evarutil and EConstr.
2017-02-14	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot
	Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
2017-02-14	Making Evd independent from Namegen.	Pierre-Marie Pédrot

2017-02-14	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot

2017-02-14	Chasing a few unsafe constr coercions.	Pierre-Marie Pédrot

2017-02-14	Do not ask for a normalized goal to get hypotheses and conclusions.	Pierre-Marie Pédrot
	This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
2017-02-14	Definining EConstr-based contexts.	Pierre-Marie Pédrot
	This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
2017-02-14	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot

2017-02-14	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot

2017-02-14	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot

2017-02-14	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot

2017-02-14	Reductionops now return EConstrs.	Pierre-Marie Pédrot

2017-02-14	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot

2017-02-14	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot

2017-02-14	Rewrite API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Hints API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Leminv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Inv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Contradiction API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Equality API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tactics API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Hipattern API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tacticals API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Clenv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Refine API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot
	This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
2017-02-14	Unification API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Pretyping API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Cases API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Typeclasses API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Tacred API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Evarconv API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Evarsolve API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Reductionops API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Termops API using EConstr.	Pierre-Marie Pédrot

2017-02-10	Proofview: tclINDEPENDENTL	Enrico Tassi

2017-02-01	Merge branch 'v8.6'	Pierre-Marie Pédrot

2017-01-23	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot

2017-01-22	Adding a new evar source to remember the name of evars which were	Hugo Herbelin
	named in the original term. Useful at least for debugging, useful to give a better message than "this placeholder", even if in the loc is known in this case.
2017-01-09	Merge remote-tracking branch 'github/pr/350' into trunk	Maxime Dénès
	Was PR#350: tclDISPATCH: more informative error message
2016-12-07	Merge branch 'v8.6'	Pierre-Marie Pédrot

2016-12-02	Document changes	Matthieu Sozeau

2016-11-30	Fix UGraph.check_eq!	Matthieu Sozeau
	Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code
2016-11-18	Merge branch 'v8.6'	Pierre-Marie Pédrot

2016-11-08	Introducing a new EConstr.t type to perform the nf_evar operation on demand.	Pierre-Marie Pédrot

2016-11-08	tclDISPATCH: more informative error message	Arnaud Spiwack
	"expected _n_ tactics" -> "exected _n_ tactics, was given _k_". Also affect other similar tacticals from `Proofview`. I used that for debugging once, I thought I might as well propose it for mergeing.