coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#594: An example showing the benefit of Econstr	Maxime Dénès	2017-05-11
\|\
* \	Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...	Maxime Dénès	2017-05-11
\|\ \
* \ \	Merge PR#606: Added an option Set Debug Cbv	Maxime Dénès	2017-05-09
\|\ \ \
* \| \| \|	Remove dead code and unused open.	Maxime Dénès	2017-05-05
* \| \| \|	Merge PR#558: Adding a fold_glob_constr_with_binders combinator	Maxime Dénès	2017-05-05
\|\ \ \ \
\| \| \| \| *	Upgrading some local function as a general-purpose combinator Option.List.map.	Hugo Herbelin	2017-05-05
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR#544: Anonymous universes	Maxime Dénès	2017-05-05
\|\ \ \ \
* \ \ \ \	Merge PR#404: patch for printing types of let bindings	Maxime Dénès	2017-05-03
\|\ \ \ \ \
\| \| \| \| * \|	Added an option Set Debug Cbv.	Hugo Herbelin	2017-05-03
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| * \| \|	Type@{_} should not produce a flexible algebraic universe.	Gaetan Gilbert	2017-05-03
\| \| * \| \|	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
* \| \| \| \|	Merge PR#411: Mention template polymorphism in the documentation.	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	applied the patch for printing types of let bindings by @herbelin	Abhishek Anand (@brixpro-home)	2017-05-02
\| \|/ / / \|/\| \| \|
* \| \| \|	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
* \| \| \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
* \| \| \|	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \| \| \|	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
\|\ \ \
* \ \ \	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
\|\\| \| \|
\| \| \| *	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
\| * \| \|	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
\| \|_\|/ / \|/\| \| \|