aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacinterp.mli
AgeCommit message (Expand)Author
2002-05-29Déplacement de proofs vers tacticsherbelin
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
2002-05-15Contournement de la fermeture ML dans VContextherbelin
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
2002-03-12Retablissement de interp_tab + injection id -> constr sans goaldelahaye
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
2001-09-20Transparentbarras
2001-08-10Parsingherbelin
2001-06-29Backtracking pour le Matchdelahaye
2001-04-19Metas dans les Unfold'sdelahaye
2001-03-15entetesfilliatr
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
2001-01-27make docherbelin
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-21Traitement du pretty-print des Redexpdelahaye
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-10-30Tactiques utilisateur + debuggerdelahaye
2000-10-18Renommage canonique :herbelin
2000-07-25retablissement make doc et make minicoqfilliatr
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-06-28Modifs de presentation.delahaye
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-05-03Ajout du langage de tactiquesdelahaye
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-11-24Vernacinterp et Vernacentries (partiellement)filliatr
1999-10-22module Macros et Tacinterpfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:23:13 +0000