coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Use evd_combX in Cases.	Gaëtan Gilbert	2018-05-14
*	Typing implementation doesn't use evdref.	Gaëtan Gilbert	2018-05-14
*	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
*	Typing: define functional alternatives to e_* functions	Gaëtan Gilbert	2018-05-14
*	set_solve_evars doesn't use an evar_map ref	Gaëtan Gilbert	2018-05-11
*	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
*	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.	Pierre-Marie Pédrot	2018-05-04
\|\
* \|	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
* \|	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
* \|	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
\| \| *	[api] Move `hint_info_expr` to `Typeclasses`.	Emilio Jesus Gallego Arias	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
\|\ \ \ \