aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac
AgeCommit message (Collapse)Author
2007-02-16lift params appropriately, do not need to coerce to tyconmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9653 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Update implementation for dependent types. Works just as well as before for ↵msozeau
simple cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9651 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-12Fix matching on dependent types, taking a safe stand.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9641 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-09Separate Tactics in subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9627 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-08Add lif then else for if in bool.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9626 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-08Fix myinjection tactic, generalize coercion for applicationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9625 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Fix mistake naming my Tactics file Tactics :)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9624 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Add tactics for induction on subterms.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9623 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Various subtac fixes. Add inequalities in pattern matching branches when ↵msozeau
needed, handle undo for the default tactic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9608 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-03Work on ineqs generation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9590 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterherbelin
de cacher l'instance de la règle figurant dans g_constr (report révision 9588 de 8.1 vers trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9589 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Abbreviation of order notation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9576 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-30constr_of_pat bug with nested patterns.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9556 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Various fixes in subtac, update some test cases.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9553 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24Update some tests and fix section bug.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9530 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-15Various subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9473 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-02Rework subtac pattern matching equalities generation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9470 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-22Default tactic for solving goals.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9460 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-14Reimplemented equality generation for pattern matching at typing time. First ↵msozeau
version. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9451 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Subtac: work on cases.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9444 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Subtac bug fix, add list take example.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9411 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-29Fork of cases impl for subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9407 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Suppression du type 'tac dans les abstract_argument_type: devenu inutile herbelin
suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des wit_tactic en types créés dynamiquement (révisions 8917 et 8926). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16Work on dep types pattern matchingmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9380 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-15Some usability enhancements.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9376 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Better solve using tactics impl.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9374 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Work on mutual defs, various bug fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9360 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Work on pattern inequalities for pattern matching branches.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9358 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-09Support for mutual defs in obligation handling.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9357 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Debug obligation handling codemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9329 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Fix compile errormsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9327 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Work on obligation separation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9326 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-29Suite commit polymorphismeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9316 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Facilities to automatically solve obligationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9284 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-10Fix 0 obligations bugmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9231 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28Add dependent list combinators test.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9184 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
en dernière étape de la procédure d'unification - Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution de l'unification premier ordre flexible/rigide - Déplacement check_evars dans Evarutil Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ? (cf exemples d'application dans test-suite/success/evars.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-04Fix wrong order for building library, add informative messages.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9121 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01New handling of obligations.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9120 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Forgot to add this one.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9118 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Subtac fixes, new way of handling obligations in progress.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9117 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Fix wrong order of existentials in eterm.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8984 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Mutually structurally recursive defs and rec using measures added.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8968 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Wellfounded recursion using subtac working again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8966 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Progress in new wf def typing.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8965 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-23 04:57:03 +0000