coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \|	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
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Replace uses of Termops.dependent by more specific functions.	Pierre-Marie Pédrot	2018-04-10
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
\| \| \| * \| \| \|	Do not compute constr matching context if not used.	Pierre-Marie Pédrot	2018-04-10
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| \| \| \| *	Fixes #7195 (missing freshness condition in Ltac pattern-matching names).	Hugo Herbelin	2018-04-08
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| \| *	Fix #5539: algebraic universe produced by cases.	Gaëtan Gilbert	2018-04-06
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	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
\| \|/ / \|/\| \|
\| \| *	Fixes #7011 (Fix/CoFix were not considered in tactic unification).	Hugo Herbelin	2018-03-26
\| \|/
* /	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
\|\ \ \ \