aboutsummaryrefslogtreecommitdiff
path: root/parsing/pretty.ml
AgeCommit message (Collapse)Author
2000-05-03suppression de Fw pour les implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Déplacement du type reference dans Termherbelin
Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@284 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration ↵herbelin
du let-in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Restructuration printer et parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@263 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modules et coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@239 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11Intégration initiale du Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@234 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09 - constantes avec recettesfilliatr
- discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-06declarations eliminations / debuggae inductifs (debut)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-05mise au point lexer / debugage PPfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@205 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02modifs pour premiere edition de liensfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02affichage classes et coercionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@187 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01mise au point Declare et avancee dans Asttermfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@175 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - Typing -> Safe_typingfilliatr
- proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-29portage Astterm (partiellement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26module Pretty (partiellement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@150 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:20:38 +0000