aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_tactic.ml4
Commit message (Expand)AuthorAge
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...Gravatar herbelin2001-10-05
* TransparentGravatar barras2001-09-20
* Ajout syntaxe "Assert H:T."Gravatar herbelin2001-09-14
* Remplace numarg -> pure_numarg dans Double InductionGravatar mohring2001-08-28
* ParsingGravatar herbelin2001-08-10
* Renommage TrueCut -> AssertGravatar herbelin2001-08-08
* Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...Gravatar herbelin2001-08-07
* Mise en place d'un nouveau Destruct sur le modèle du nouvel InductionGravatar herbelin2001-08-05
* Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...Gravatar herbelin2001-07-02
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...Gravatar herbelin2001-06-25
* Extension des parametres de Clear + InstGravatar delahaye2001-06-19
* Interpretation MetaId + Progress + InstGravatar delahaye2001-06-18
* Fix de quelques bugs syntaxiques de LtacGravatar delahaye2001-06-11
* Les clauses de Rec doivent prendre des tactic_atom'sGravatar delahaye2001-04-24
* Petit menageGravatar delahaye2001-04-20
* *** empty log message ***Gravatar mayero2001-04-19
* Essais dans LtacGravatar delahaye2001-04-19
* Non parenthesage des applications de tactiquesGravatar delahaye2001-04-14
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* entetesGravatar filliatr2001-03-15
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Modif pour les patterns de sous-termesGravatar delahaye2001-02-07
* *** empty log message ***Gravatar mohring2001-02-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* ajout ident_or_constrarg pour NewInductionGravatar herbelin2000-12-20
* Correction associativite de Repeat/OrelseGravatar delahaye2000-12-19
* numarg -> pure_numarg a poursuivreGravatar mohring2000-12-11
* Extension de la syntaxe de LetTacGravatar herbelin2000-12-06
* Correction pour les qualidconstargGravatar delahaye2000-12-06
* Plus de quote devant les ident et les ?Gravatar delahaye2000-12-05
* Elimination du 'Gravatar delahaye2000-11-28
* Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...Gravatar herbelin2000-11-26
* Bug qualidconstarg (intervient pour Transparent)Gravatar herbelin2000-11-23
* Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT pou...Gravatar herbelin2000-11-20
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* Priorite du Try/Orelse + Debug switch + correction bug dans PatternGravatar delahaye2000-10-30
* Ajout castedopenconstrarg; Renommage tactique Let en LetTacGravatar herbelin2000-10-03
* Pattern matching de sous-termes + exceptions dans le lexerGravatar delahaye2000-08-17
* Modifs d'interpretation de patterns + exceptions dans le lexerGravatar delahaye2000-07-21
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Fin du changement comarg -> constrargGravatar herbelin2000-01-26
* Nettoyage des fichiers de parsingGravatar herbelin2000-01-13
* Renommage command en constrGravatar herbelin2000-01-07
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 12:58:28 +0000