aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hiddentac.mli
Commit message (Expand)AuthorAge
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
* bugs avec Pose et AssertGravatar barras2004-01-09
* Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...Gravatar herbelin2003-11-25
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Added Instantiate ... inGravatar corbinea2003-11-06
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesGravatar herbelin2002-10-21
* NewDestruct/NewInduction acceptent l'option "using"Gravatar herbelin2002-10-21
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23