aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/dependentind.v
AgeCommit message (Expand)Author
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
2009-11-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-06-02Fix script file using the "Manual Implicit" flag.msozeau
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-02-04Report r11631 from 8.2 and handle non-dependent goals better inmsozeau
2008-11-07Fix a bug in the specialization by unification tactic related to the problemsmsozeau
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-09-15Report improvements in Equations to the dependent elimination tactic:msozeau
2008-09-11Fixes in dependent induction tactic, putting things in better order formsozeau
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-15Various fixes:msozeau
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-16Misc: Add test for bug 1704, now closed. Add usual syntax for lists inmsozeau
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
2008-01-31Debug implementation of dependent induction/dependent destruction and documen...msozeau
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
2008-01-02Better resolution of implicit parameters in typeclass binders, add extensiona...msozeau
2007-08-08Add a test case for the new "dependent" induction tactics.msozeau