aboutsummaryrefslogtreecommitdiff
path: root/tactics/dhyp.ml
AgeCommit message (Expand)Author
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-13compat ocaml 3.03filliatr
2001-08-10Parsingherbelin
2001-07-10Branchement sur bad_tactic_argsherbelin
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-15methode exportfilliatr
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-11-02suppression des (* open Generic *)filliatr
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
2000-01-07Renommage command en constrherbelin
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-11-24MAJ pour fusion avec pretypingherbelin
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr