coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Stopping injection not to work on discriminable atoms (see #4890).	Hugo Herbelin	2017-05-17
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| *	Fix the API of the new pf_constr_of_global.	Pierre-Marie Pédrot	2017-04-24
\| *	Removing the tclNOTSAMEGOAL primitive from the API.	Pierre-Marie Pédrot	2017-04-24
\|/
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Chasing a few unsafe constr coercions.	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 compatibility layers from Tacticals	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers in Retyping	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
* \|	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
* \|	Tacmach API using EConstr.	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
* \|	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
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Fixing injection in the presence of let-in in constructors.	Hugo Herbelin	2016-12-22
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|/\|
\| *	Renamings to avoid confusion deprecating old names	Matthieu Sozeau	2016-10-22
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	fixing bug 4609: document an option governing the generation of equalities	Yves Bertot	2016-10-03
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-02
\| \|\
\| \| *	Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.	Hugo Herbelin	2016-09-30
\| * \|	Merge branch 'v8.5' into v8.6	Maxime Dénès	2016-09-30
\| \|\\|
\| \| *	Fix a bug in subst releaved by an OCaml warning.	Maxime Dénès	2016-09-29
* \| \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \| \| \|	CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function	Matej Kosik	2016-08-25
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\ \ \ \| \| \|/ \| \|/\|