aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/subtac.ml
Commit message (Expand)AuthorAge
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Fix define body bug fixGravatar msozeau2007-10-24
* Fix define body bugGravatar msozeau2007-10-24
* Fix some bugs, add possibility of automatically solving a proof statement's o...Gravatar msozeau2007-10-24
* Fix dependency bugs due to Program modules renamings.Gravatar msozeau2007-08-08
* Move Program tactics into a proper theories/ directory as they are general pu...Gravatar msozeau2007-08-07
* Remove dead modules in Subtac.Gravatar msozeau2007-07-12
* Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...Gravatar msozeau2007-06-09
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Correct implementation of undo in obligations handling code, correct some bug...Gravatar msozeau2007-04-17
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Update implementation for dependent types. Works just as well as before for s...Gravatar msozeau2007-02-16
* Various subtac fixes. Add inequalities in pattern matching branches when need...Gravatar msozeau2007-02-07
* Various subtac fixes.Gravatar msozeau2007-01-15
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
* Default tactic for solving goals.Gravatar msozeau2006-12-22
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
* Facilities to automatically solve obligationsGravatar msozeau2006-10-26
* New handling of obligations.Gravatar msozeau2006-09-01
* Subtac fixes, new way of handling obligations in progress.Gravatar msozeau2006-09-01
* Rewrite of the recursive defs handling in progress.Gravatar msozeau2006-06-20
* Fix some nasty bug with the evars-to-dependent sum encoding.Gravatar msozeau2006-06-01
* Added code to support "Program Lemma/Example... etc"Gravatar msozeau2006-04-16
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Subtac fixes, single fixpoint definitions are working again. Added a toggle o...Gravatar msozeau2006-03-22
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* New files for subtacGravatar coq2006-03-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-03 06:27:49 +0000