coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7358: Fix #7356: missing lift when interpreting default instances o...	Enrico Tassi	2018-04-27
\|\
\| *	Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.	Hugo Herbelin	2018-04-26
* \|	Always print explanation for univ inconsistency, rm Flags.univ_print	Gaëtan Gilbert	2018-04-26
\|/
*	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias	2018-04-23
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...	Pierre-Marie Pédrot	2018-04-13
\|\
* \	Merge PR #6972: [api] Deprecate a couple of aliases that we missed.	Maxime Dénès	2018-04-12
\|\ \
* \ \	Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)	Pierre-Marie Pédrot	2018-04-01
\|\ \ \
\| \| \| *	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\| \|_\|/ \|/\| \|
\| * \|	Supporting fix/cofix in Ltac pattern-matching (wish #7092).	Hugo Herbelin	2018-03-28
\| * \|	Patterns: Accepting patterns in PFix and PCofix and not only constr.	Hugo Herbelin	2018-03-28
\| * \|	Detyping: Adding a variant of share_names for patterns.	Hugo Herbelin	2018-03-28
\| * \|	Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).	Hugo Herbelin	2018-03-28
\| * \|	Patternops: renaming an internal function to more closely match its effect.	Hugo Herbelin	2018-03-28
\| * \|	Glob_ops: cosmetic renaming to reflect the type of objects.	Hugo Herbelin	2018-03-28
\| \| *	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
\| \|/ \|/\|
* \|	Slightly refining some error messages about unresolvable evars.	Hugo Herbelin	2018-03-24
\|/
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6806: Adding missing unification constraint noticed by @skyskimmer	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\ \ \
\| \| \| *	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	2018-03-09
\| \| \| *	Statically enforce that ULub is only between levels.	Gaëtan Gilbert	2018-03-09
\| \| \| *	Option for messing with inference of irrelevant constraints	Gaëtan Gilbert	2018-03-09
\| \| \| *	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
\| \| \| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
\| \|_\|/ \|/\| \|
\| \| *	Adding a missing unification in typing.ml.	Hugo Herbelin	2018-03-09
* \| \|	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès	2018-03-09
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6747: Relax conversion of constructors according to the pCuIC model	Maxime Dénès	2018-03-09
\|\ \ \
* \ \ \	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\ \ \ \
\| \| \| * \|	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Leave cumul constructor universes as is during unif	Matthieu Sozeau	2018-03-08
\| \| * \|	Relax conversion of constructors according to the pCuIC model	Matthieu Sozeau	2018-03-08
\| \|/ / \|/\| \|
* \| \|	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \ \
* \ \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \ \
\| \| \| * \|	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #6900: [compat] Remove "Tactic Pattern Unification"	Maxime Dénès	2018-03-06
\|\ \ \ \
\| \| \| * \|	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
* \| \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \
* \ \ \ \	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| * \| \| \|	reductionops: remove dead code "bind_assum"	Enrico Tassi	2018-03-04
* \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot	2018-03-04
\| \| \| * \| \| \|	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \|_\|/ \| \| \| \|/\| \|
\| \| \| \| \| *	[compat] Remove "Tactic Pattern Unification"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \|/ \| \| \| \|/\|
\| \| * \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02