aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/dhyp.ml
Commit message (Expand)AuthorAge
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove legacy export_* functionsGravatar glondu2009-09-29
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nouvelle en-têteGravatar herbelin2004-07-16
* 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