coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Porting the ssrmatching plugin to the new EConstr API.	Enrico Tassi	2017-02-14
\| \|
* \|	Quick hack to fix interpretation of patterns in Ltac.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip through the pretyper, and relies on suspicious flagging of evars in the evar source field to recognize original pattern holes. After the pattern_of_constr function was made evar-insensitive, it expanded evars that were solved by magical side-effects of the pretyper, even if it hadn't been asked to perform any heuristics. We backtrack on the insensitivity of the pattern_of_constr function. This may have a performance penalty in other dubious code, e.g. hints. In the long run we should get rid of the pattern_of_constr function.
* \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \|	Now they are useless because all of the primitives are (should?) be evar-insensitive.
* \|	Fix a mishandled exception in Omega.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \|	Due to the introduction of the monadic layer, an exception was raised at a later time and not caught properly.
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing compatibility layers from Tacticals	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Omega API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Micromega API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Setoid_ring API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Cc API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Quote API using EConstr.	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
\| \|
* \|	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Hints 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
\| \|
* \|	Elim 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
\| \|
* \|	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Cleaning up opening of the EConstr module in pretyping folder.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	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
\| \|
* \|	Tacred API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Constr_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Patternops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Typing 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
\| \|
* \|	Retyping 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-14
\| \|
\| *	Merge PR#393: Replace Typeops with Fast_typeops	Maxime Dénès	2017-02-08
\| \|\
\| * \|	Revert "Extraction: avoid deprecated functions of module String"	Pierre Letouzey	2017-02-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...