aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Remove legacy export_* functionsGravatar glondu2009-09-29
* Apply "Declare Implicit Tactic" also to terms interpreted as "openGravatar herbelin2009-09-27
* 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
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Better use of transparency information for local hypotheses: Gravatar msozeau2009-09-22
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Allow setoid rewrite to rewrite in pattern-matching scrutinees orGravatar msozeau2009-09-09
* 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
* Support globality flag properly for "Add Morphism foo : foo_mor" syntax.Gravatar msozeau2009-09-03
* Stop unnecessary use of lazy values for constraints, simplifyingGravatar msozeau2009-09-02
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* 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
* Fixed a typo in "info" for tactic "right".Gravatar herbelin2009-08-02
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Simplify addition of hints to a hint_db. Rebuild the dnet associatedGravatar msozeau2009-07-08
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Raise an error and not an anomaly if a rewrite is attempted on aGravatar msozeau2009-06-28
* Correct treatment of dependent products in signatures: create the evarsGravatar msozeau2009-06-22
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* When typing a non-dependent arrow, do not put the (anonymous) variableGravatar msozeau2009-06-11
* Use the projections for reflexivity, symmetry and transitivity proofs toGravatar msozeau2009-06-10
* Correct handling of the initial existentials from the goal and the onesGravatar msozeau2009-06-09
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* ## Lines starting with '## ' will be removed from the log message.Gravatar msozeau2009-06-01
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Minor unification changes:Gravatar msozeau2009-05-18
* - Allowing multiple calls to tactic fix with automatic generation ofGravatar herbelin2009-05-17
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 22:42:55 +0000