aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/dependentind.v
Commit message (Expand)AuthorAge
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* Use a heuristic to not simplify equality hypotheses remaining after dependent...Gravatar msozeau2012-02-20
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...Gravatar msozeau2012-01-28
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Fix test-suite scripts: [Generalizable Variables] and small Gravatar msozeau2009-11-13
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
* Fixes in dependent induction tactic, putting things in better order forGravatar msozeau2008-09-11
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
* Various fixes:Gravatar msozeau2008-05-15
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* Misc: Add test for bug 1704, now closed. Add usual syntax for lists inGravatar msozeau2008-03-16
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Add a test case for the new "dependent" induction tactics.Gravatar msozeau2007-08-08