| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
qu'il entre en conflit avec le module Errors ajouté dans OCaml courant
(future version OCaml 3.05).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
- commande Back
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
le source cite et la ligne de ^^^
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1720 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
at the time the protected loop was started. This makes it possible
to have modifications of commands specific to the protected loop remembered
throughout the session.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1371 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@993 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@477 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
- #use "include.ml";;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@198 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@88 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@83 85f007b7-540e-0410-9357-904b9bb8a0f7
|
barras
filliatr
herbelin
ddr
bertot