aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/dhyp.ml
Commit message (Expand)AuthorAge
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* L'application de ltac attend une référence; meilleure protection contreGravatar herbelin2002-10-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTGravatar herbelin2002-06-06
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* compat ocaml 3.03Gravatar filliatr2001-12-13
* ParsingGravatar herbelin2001-08-10
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
* Renommage command en constrGravatar herbelin2000-01-07
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:02:55 +0000