aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Equality: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Equality: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Fixed a "feature" of "inversion" and "dependent rewrite" revealed byGravatar herbelin2011-07-18
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...Gravatar herbelin2011-07-16
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
* A few comments and a dev file to summarize issues with unificationGravatar herbelin2011-06-13
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* Fixing discriminate for identity.Gravatar herbelin2011-05-26
* Add a flag to control betaiota reduction during unification to maintain backw...Gravatar msozeau2011-04-18
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Fixing injection bug #2493 (regression introduced by fixing injectionGravatar herbelin2011-03-05
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* correction of bug #2414 (report of r 13586)Gravatar jforest2010-10-27
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New pass on inductive schemesGravatar herbelin2010-05-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
* Applied greenrd's patch to fix bug 2255 (injection failed toGravatar herbelin2010-03-27
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Completion of r12580 (better rendering of dependent rewrite and inversion).Gravatar herbelin2009-12-13
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Improved the rendering of "dependent rewrite" and hence of "inversion"Gravatar herbelin2009-12-12
* Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameGravatar herbelin2009-12-03
* Addendum to revision 12501.Gravatar herbelin2009-11-12
* Backtracking on the use of automatically generated schemes forGravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Fixed a bug in the interaction between dEqThen and inject_at_positionsGravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Stop trying to search if the relation is declared as a [RewriteRelation]Gravatar msozeau2009-09-09
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* Fixed subst failing when a truly heterogeneous JMeq hyp is in theGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 02:37:54 +0000