coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \| \| \| \| \| \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| * \| \| \| \| \| \| \|	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| \| \| \| * \| \| \| \|	A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".	Hugo Herbelin	2017-04-27
\| \| \|_\|/ / / / / \| \|/\| \| \| \| \| \|
\| * \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-04-27
\| \|\ \ \ \ \ \ \ \| \| \| \|_\|/ / / / \| \| \|/\| \| \| \| \|
* \| \| \| \| \| \| \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \| \| \| \| \| \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \| \| \| \| \| \|	[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 #5377: @? patterns broken.	Pierre-Marie Pédrot	2017-04-20
* \| \| \| \| \| \| \|	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
\|\\| \| \| \| \| \|
\| \| \| \| \| * \|	Reinstate fixpoint refolding in [cbn], deactivated by mistake.	Matthieu Sozeau	2017-04-13
\| \| \|_\|_\|/ / \| \|/\| \| \| \|
\| \| \| * \| \|	Using fold_glob_constr_with_binders to code bound_glob_vars.	Hugo Herbelin	2017-04-13
\| \| \| * \| \|	Adding a fold_glob_constr_with_binders combinator.	Hugo Herbelin	2017-04-13
* \| \| \| \| \|	Silence a few OCaml warnings.	Guillaume Melquiond	2017-04-13
* \| \| \| \| \|	Merge PR#543: Sanitize instance interpretation	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| \| * \| \|	Update various comments to use "template polymorphism"	Gaetan Gilbert	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
\| \| \| \| * \|	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
\| \| \| \|/ /
\| * \| \| \|	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
\|\ \ \