coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
\| *	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\| \|\
* \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\\| \|
* \| \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* \| \|	Fix call to broken unsafe_type_of in apply tactic.	Maxime Dénès	2017-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This broke the build of iris-coq in the EConstr branch. Each time you use unsafe_type_of, I loose a night of sleep, so please stop.
* \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\ \ \
\| \| * \|	[nit] Fix a couple incorrect uses of msg_error.	Emilio Jesus Gallego Arias	2017-03-24
\| \|/ /
\| \| *	Fast path for implicit tactic solving.	Pierre-Marie Pédrot	2017-03-23
\| \|/ \| \| \| \| \| \| \| \| \| \|	We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately.
\| *	[pp] [ide] Minor cleanups in pp code.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics.
\| *	Remove a dead exception catching code.	Théo Zimmermann	2017-03-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The code was assuming that Proofview.tclFOCUS could raise a CList.IndexOutOfRange exception but this isn't the case. The focusing functions already catch this exception and raises an algebraic exception within the tactic mechanism.
\| *	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	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.
* \|	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.
* \|	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	2017-02-14
\| \| \| \| \| \| \| \| \| \|	This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* \|	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.
* \|	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \|	This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
* \|	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
\| \|
* \|	Funind API using EConstr.	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
\| \|
* \|	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
\| \|
* \|	Eqdecide API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Tactics 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
\| \|
* \|	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Refine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Goal API using EConstr.	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
\| \|
* \|	Coercion 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
\| \|
* \|	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Nativenorm API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	Vnorm 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
\| \|