coq - The formal proof system

Age	Commit message (Expand)	Author
2011-07-29	generic = on named_context replaced by named_context_equal	puech
2011-07-29	Tactics: replace generic = on constr by destructors	puech
2011-07-29	Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ord	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-07-29	Class_tactics: generic equality on named_context_val replaced by eq_named_con...	puech
2011-07-29	Eqschemes: generic equality on constr replaced by eq_constr	puech
2011-07-29	Equality: generic equality on constr replaced by eq_constr	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-07-29	Equality: generic equality on constr replaced by eq_constr	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-07-29	Tactics: generic equality on named_declaration replaced by eq_named_declaration	puech
2011-07-29	Hipattern: two generic equalities on constr spotted & rewritten	puech
2011-07-18	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin
2011-07-16	Changed name of internally defined "_sym" scheme to avoid confusion with Logi...	herbelin
2011-07-16	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin
2011-06-18	Relaxed the constraint introduced in r14190 that froze the existing	herbelin
2011-06-18	Generalizing flag use_evars_pattern_unification into a flag	herbelin
2011-06-13	A few comments and a dev file to summarize issues with unification	herbelin
2011-06-13	Added a flag to restrict conversion in tactic unification on the	herbelin
2011-06-12	Added a new flag for freezing evars in tactic unification. Used this	herbelin
2011-06-10	Moved allow_K to a unification flag	herbelin
2011-06-10	Fixing another bug with "_" intro pattern.	herbelin
2011-06-10	Fixing the "buggy" first_name and prepare multi-induction.	herbelin
2011-06-10	Made use of "_" in repeated use of intros_patterns work (with	herbelin
2011-06-10	Integrating onLastHypId into intro so that we can get the introduction	herbelin
2011-06-07	Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...	msozeau
2011-05-26	Fixing discriminate for identity.	herbelin
2011-05-17	Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)	letouzey
2011-05-17	More work on error handling	letouzey
2011-05-05	Merge branch 'subclasses' into coq-trunk	msozeau
2011-04-28	Revert r14078 "Partial backtrack on the support for open terms in destruct/in...	gmelquio
2011-04-28	Partial backtrack on the support for open terms in destruct/induction:	gmelquio
2011-04-26	Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).	herbelin
2011-04-25	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin
2011-04-24	Fixed a bug of destruct which was sometimes forgetting local definitions behi...	herbelin
2011-04-20	Don't force progress on instance applications, there is always progress when ...	msozeau
2011-04-20	This is used in the rippling plugin. This also allows fixing bug #2188.	msozeau
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-04-14	More informative anomaly.	herbelin
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Put dependent subgoals first so as to allow backtracking on them, might chang...	msozeau
2011-04-13	- 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	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-08	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin
2011-03-18	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-11	Keep information on which fields are subclasses in class declarations,	msozeau