coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	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	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	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	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-14
\| *	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\| \|\
\| \| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2017-01-23
\| * \|	Adding a new evar source to remember the name of evars which were	Hugo Herbelin	2017-01-22
\| * \|	Merge remote-tracking branch 'github/pr/350' into trunk	Maxime Dénès	2017-01-09
\| \|\ \
\| * \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| \| * \|	Document changes	Matthieu Sozeau	2016-12-02
\| \| * \|	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\| * \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\| \|\\| \|
* \| \| \|	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	2016-11-08
\| \|/ \|/\|
\| *	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\| \|\
\| \| *	Fixes to compile with ocaml 4.01	Matthieu Sozeau	2016-11-07
\| * \|	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\| \|\ \ \| \| \|/ \| \|/\|
* \| \|	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
* \| \|	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31