aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/dhyp.ml
Commit message (Expand)AuthorAge
* 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