aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
2011-07-18Fixed a "feature" of "inversion" and "dependent rewrite" revealed byherbelin
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...herbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-05Fixing injection bug #2493 (regression introduced by fixing injectionherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-10-27correction of bug #2414 (report of r 13586)jforest
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-29New pass on inductive schemesherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
2010-03-27Applied greenrd's patch to fix bug 2255 (injection failed toherbelin
2009-12-28Safer, though ad hoc, approach to re-interpretation of the argument ofherbelin
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-12-13Completion of r12580 (better rendering of dependent rewrite and inversion).herbelin
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-12-12Improved the rendering of "dependent rewrite" and hence of "inversion"herbelin
2009-12-03Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameherbelin
2009-11-12Addendum to revision 12501.herbelin
2009-11-11Backtracking on the use of automatically generated schemes forherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-09Quick fix for restoring a left-to-right rewriting lemma compatibleherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-28Remove old compatibility stuff (Tacred.nf)glondu
2009-10-04Changed the way to support compatibility with previous versions.herbelin
2009-09-27Fixed a bug in the interaction between dEqThen and inject_at_positionsherbelin
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-09Stop trying to search if the relation is declared as a [RewriteRelation]msozeau
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 02:33:14 +0000