aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
2009-09-26Fixed a hole in glob_tactic that allowed some Ltac code to refer toherbelin
2009-09-22Better use of transparency information for local hypotheses: msozeau
2009-09-20Only one "in" clause in "destruct" even for a multiple "destruct".herbelin
2009-09-18- Fixed a bug in checking that implicit arguments are all correctlyherbelin
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-13- Inductive types in the "using" option of auto/eauto/firstorder areherbelin
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-09-10Added syntax "exists bindings, ..., bindings" for iterated "exists".herbelin
2009-09-09Allow setoid rewrite to rewrite in pattern-matching scrutinees ormsozeau
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
2009-09-03Support globality flag properly for "Add Morphism foo : foo_mor" syntax.msozeau
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-06Move out JMeq of subst for compatibility (it affects e.g. theherbelin
2009-08-04- Add more precise error localisation when one of the application failsherbelin
2009-08-04Fixed subst failing when a truly heterogeneous JMeq hyp is in theherbelin
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-08-02Fixed a typo in "info" for tactic "right".herbelin
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
2009-07-08Simplify addition of hints to a hint_db. Rebuild the dnet associatedmsozeau
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
2009-06-28Raise an error and not an anomaly if a rewrite is attempted on amsozeau
2009-06-22Correct treatment of dependent products in signatures: create the evarsmsozeau
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-16Reimplementation of leibniz rewrite to control the instantiation of themsozeau
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-06-11When typing a non-dependent arrow, do not put the (anonymous) variablemsozeau
2009-06-10Use the projections for reflexivity, symmetry and transitivity proofs tomsozeau
2009-06-09Correct handling of the initial existentials from the goal and the onesmsozeau
2009-06-08Do a fixpoint on the result of typeclass search to force themsozeau
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
2009-06-01## Lines starting with '## ' will be removed from the log message.msozeau
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
2009-05-18Minor unification changes:msozeau
2009-05-17- Allowing multiple calls to tactic fix with automatic generation ofherbelin
2009-05-16Minor fixes in typeclasses:msozeau
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-05-05Improvements in typeclasses eauto and generalized rewriting:msozeau
2009-04-28Fixes for bugs in r12110:msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:45:08 +0000