| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
Example: "Notation reflexive R := (forall x, R x x)."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Au passage, un peu plus de standardisation des noms de fonctions de
globalisation
Principe de base :
locate_foo : qualid -> foo (échoue avec Not_found)
global : reference -> global_reference (échoue avec UserError)
global_of_foo : foo -> global_reference (échoue avec UserError)
f_with_alias : se comporte comme f mais prenant aussi en compte les
notations de la forme "Notation id:=ref"
Principale exception :
locate, au lieu de locate_global
locate_global_with_alias, qui prend en entrée un "qualid located"
Restent beaucoup de fonctions qui pourraient utiliser
global_with_alias au lieu de global, notamment dans contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
vers syntax_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7051 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5911 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 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
|
herbelin