aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacinterp.mli
Commit message (Expand)AuthorAge
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
* Ajout du printer de tactiques + modif du Dynamic ocamlGravatar delahaye2001-09-30
* TransparentGravatar barras2001-09-20
* ParsingGravatar herbelin2001-08-10
* Backtracking pour le MatchGravatar delahaye2001-06-29
* Metas dans les Unfold'sGravatar delahaye2001-04-19
* entetesGravatar filliatr2001-03-15
* Reparation du pretty-print pour les tactiquesGravatar delahaye2001-02-07
* make docGravatar herbelin2001-01-27
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Tactiques utilisateur + debuggerGravatar delahaye2000-10-30
* Renommage canonique :Gravatar herbelin2000-10-18
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Modifs de presentation.Gravatar delahaye2000-06-28
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24
* module Macros et TacinterpGravatar filliatr1999-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 21:29:56 +0000