coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evarutil: replace generic list_distinct on constr by constr_list_distinct	puech	2011-07-29
*	Evarutil: replaced some generic = on constr by destructors	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by destructors	puech	2011-07-29
*	Evarconv: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Cases: generic equality on constr replaced by destructors	puech	2011-07-29
*	Classops: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr (x2)	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tacred: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	This is exactly the structure needed to handle controlling printing	herbelin	2011-07-16
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Fixing two typos introduced in r14217 and r14223	herbelin	2011-06-20
*	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin	2011-06-19
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Activating flags betaiota by default for apply	herbelin	2011-06-18
*	The ad hoc version for first-order unification at toplevel of "?n args	herbelin	2011-06-18
*	Added full pattern-unification on Meta for tactic unification.	herbelin	2011-06-13
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Oups, typo in previous commit	herbelin	2011-06-12
*	Removed what looks like a (very old) useless f.o. unification pass	herbelin	2011-06-12
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Fixes in pruning, do not fail if pruning is impossible due to typing constrai...	msozeau	2011-06-10
*	More fixes in pruning/restriction of evars during unification.	msozeau	2011-06-09
*	Fixes in pruning in unification.	msozeau	2011-06-08
*	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau	2011-06-07
*	Applying Enrico Tassi's patch for giving priority to delta over eta in	herbelin	2011-05-24
*	Failing instead of switching to the coercion mechanism when VMcast	herbelin	2011-05-15
*	A better procedure for checking presence of undefined evars.	aspiwack	2011-05-13
*	Fix merge, Cumul moved to CUMUL	msozeau	2011-05-05
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	First phase removing obsolete support for eta up to conversion in	herbelin	2011-05-04
*	Fixing bug in printing let-in binders in fix/cofix	herbelin	2011-04-24
*	Allow betaiota when checking unification of the types of metas (fixes ATBR co...	msozeau	2011-04-20
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	Fix unification of types of metavariables and error message for sort unificat...	msozeau	2011-04-16
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	- Make typeclass transparency information directly available	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	- Improve unification (beta-reduction, and same heuristic as evarconv for red...	msozeau	2011-04-13
*	Unify meta types with the right flags, add betaiotazeta reduction to unificat...	msozeau	2011-04-13
*	Proper typing of metavariables, type errors were completely ignored before......	msozeau	2011-04-13
*	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau	2011-04-13
*	Catch NotArity exception and transform it into an anomaly in retyping.	msozeau	2011-04-11
*	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin	2011-04-08
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin	2011-04-06
*	As remarked by Enrico, we'd better use eq_constr than structural equality	herbelin	2011-03-31
*	- Remove useless grammar rule	msozeau	2011-03-23