coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\|
*	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
\|
*	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
\|
*	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Classops 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
\|
*	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
\|
*	Recordops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Evardefine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Find_subterm API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Cbv 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
\|
*	Introducing a new EConstr.t type to perform the nf_evar operation on demand.	Pierre-Marie Pédrot	2016-11-08
\|
*	Revert "Better Arguments compatibility."	Maxime Dénès	2016-11-03
\| \| \| \| \| \|	This reverts commit 5358515f23d1cd47d4914c55dcf049df858b9dc7. The syntax is deprecated in 8.6, so we now remove it from trunk.
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2016-11-03
\|\
\| *	Merge remote-tracking branch 'github/pr/341' into v8.6	Maxime Dénès	2016-11-03
\| \|\ \| \| \| \| \| \| \| \| \|	Was PR#341: Better Arguments compatibility.
* \| \|	updating ".merlin" file	Matej Kosik	2016-11-03
\| \| \|
\| \| *	Better Arguments compatibility.	Maxime Dénès	2016-11-02
\| \|/ \| \| \| \| \| \| \| \|	With multiple arguments list, repeating the "/" modifier used to be mandatory. So instead of forbidding it, we issue a deprecation warning.
* \|	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there.
* \|	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
\| \| \| \| \| \| \| \| \| \|	We return an option type, as constraints were always dropped if the boolean was false. They did not make much sense anyway.
* \|	Code factorization in Universes.	Pierre-Marie Pédrot	2016-10-31
\| \|
* \|	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
\| \| \| \| \| \| \| \| \| \| \| \|	Before this patch, this module was a member of the library folder, which had little to do with its actual use. A tiny part relative to global registering of universe names has been effectively moved to the Global module.
* \|	Reordering Termops w.r.t. Evd and Namegen in engine folder.	Pierre-Marie Pédrot	2016-10-30
\| \|
\| *	Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.	Pierre-Marie Pédrot	2016-10-30
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-29
\| \|\
\| * \|	Removing dead code.	Hugo Herbelin	2016-10-29
\| \| \|
\| * \|	Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).	Hugo Herbelin	2016-10-29
\| \| \| \| \| \| \| \| \| \| \| \|	(May it fell in the case mentioned in the inner comment of Exninfo.info?)
\| * \|	Fixing #5164 (regression in locating error in argument of "refine").	Hugo Herbelin	2016-10-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reporting location was not expecting a term passed to an ML tactic to be interpreted by the ML tactic itself. Made an empirical fix to report about the as-precise-as-possible location available.