aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_coercion.ml
AgeCommit message (Expand)Author
2007-01-15Various subtac fixes.msozeau
2006-12-08Subtac bug fix, add list take example.msozeau
2006-11-29Fork of cases impl for subtac.msozeau
2006-11-16Work on dep types pattern matchingmsozeau
2006-10-26Facilities to automatically solve obligationsmsozeau
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-10Fixes for new unification, not used in default version as it really changes u...msozeau
2006-04-10Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-02-22Work on recursive definitionscoq
2006-02-21Work with binder lists, problem of tyconscoq
2006-02-21Latest fixes, should work fine now for non recursive definitions, although st...coq
2006-02-20Fix minor bugcoq
2006-02-20Forgot a filecoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 23:17:28 +0000