coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
*	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
*	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
*	[location] Move Glob_term.predicate_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
*	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
*	Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.	Maxime Dénès	2017-04-24
\|\
\| *	[flags] Deprecate is_silent/is_verbose in favor of single flag.	Emilio Jesus Gallego Arias	2017-04-21
* \|	Fix bug #5476: Ltac has an inconsistent view of hypotheses.	Pierre-Marie Pédrot	2017-04-19
\|/
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
* \|	Silence a few OCaml warnings.	Guillaume Melquiond	2017-04-13
* \|	Merge PR#543: Sanitize instance interpretation	Maxime Dénès	2017-04-11
\|\ \
* \ \	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \
* \| \| \|	Revert "refactoring: Reductionops.contextual_reduction_function type"	Matej Košík	2017-04-10
* \| \| \|	refactoring: Reductionops.contextual_reduction_function type	Matej Kosik	2017-04-10
\| \| \| *	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08
\| * \| \|	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\| \|\ \ \
* \| \| \| \|	Turning the printing primitive projection parameter flag off by default.	Hugo Herbelin	2017-04-07
* \| \| \| \|	Turning the printing primitive projection compatibility flag off by default.	Hugo Herbelin	2017-04-07
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\|\ \ \ \
\| \| * \| \|	Fix a normalization hotspot in computation of constr keys.	Pierre-Marie Pédrot	2017-04-06
\| \| \| * \|	Factor interp_instance out of Pretyping.pretype_global	Gaetan Gilbert	2017-04-06
\| \| \| * \|	Avoid strange shadowing of Pretyping.interp_universe_level_name	Gaetan Gilbert	2017-04-06
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Removing a normalization hotspot from EConstr.	Pierre-Marie Pédrot	2017-04-05
\| \| * \|	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
\| \| * \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
\| \| * \|	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
\| \| * \|	Revert to incorrect heuristic in apply.	Maxime Dénès	2017-03-28
\| \| * \|	Fix interpretation of Ltac patterns episode 2.	Maxime Dénès	2017-03-24
\| \| * \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\| \| \|\ \
* \| \| \| \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \|_\|/ / \|/\| \| \|
\| * \| \|	Better algorithm for Evarconv.max_undefined_with_candidates.	Pierre-Marie Pédrot	2017-03-24
* \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \ \| \| \|_\|/ \| \|/\| \|
\| * \| \|	Intern names bound in match patterns	Tej Chajed	2017-03-23
\| \| * \|	Make the computation of frozen evars lazy in Pretyping.	Pierre-Marie Pédrot	2017-03-23
\| \| * \|	Fast path in computation of frozen evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
\| \| * \|	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
\| \|/ / \|/\| \|
* \| \|	Merge PR#437: Improve unification debug trace.	Maxime Dénès	2017-03-17
\|\ \ \
\| \| \| *	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \|\ \| \|_\|_\|/ \|/\| \| \|
\| \| \| *	Quick hack to fix interpretation of patterns in Ltac.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Dedicated datatype for aliases in Evarsolve.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Putting back the occur_meta_or_undefined_evar function in the old term API.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Namegen primitives now apply on evar constrs.	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
\| \| \| *	Putting back the subst_defined_metas_evars function in the old term API.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Cleaning up interfaces.	Pierre-Marie Pédrot	2017-02-14