Ajout de remarques diverses sur les commandes vernaculaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8287 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 31 insertions, 1 deletions

diff --git a/doc/discussion-syntaxe.txt b/doc/discussion-syntaxe.txt
index 23b5cd9774..658c67c721 100644
--- a/doc/discussion-syntaxe.txt
+++ b/doc/discussion-syntaxe.txt
@@ -313,7 +313,37 @@ Questions ouvertes :
   Suggestion de CP : on réécrit le but avec des _ à la place des occurrences
   souhaitées.
 
+IV) Vernac
 
-IV) Bibliothèque standard
+Mots-cles Variables/Hypotheses/Parameters ? Si oui, pourquoi pas Axioms ?
+
+Intégrer Eval In à Constr ? Oui, mais avec une syntax plus légère
+Ou alors standardiser
+Definition_kind id params := red_expr c : t.
+
+Intégrer "with_binding" à Constr !
+
+Faut-il séparer command/gallina/gallina_ext/syntax, sachant que si
+l'on sépare, alors il ne faut plus partager de premier mot-clé (ex:
+Add et Print seront réservé pour command) ?
+
+Virer theorem_body_line ?
+
+Virer le Mutual old syntax ! Et même implanter le future style de
+Christine avec paramètres engendrés automatiquement et propre à chaque inductif
+
+Scheme est-il Gallina ou pas ?
+Require est-il gallina_ext ou commande ? Et faut-il garder specif ?
+Utilite de RequireFrom ?
+
+Faire des qualid un token ?
+
+EVAL et CONTEXT dans constr: partout ou seulement en tete ?
+Supprimer Specialize, supprimer with c (sans nom)
+
+Ltac impose que "?" soit utilisable là où un identificateur ou un nom
+long est attendu (p.ex. dans Clear). Accepte-t-on le principe ?
+
+V) Bibliothèque standard
 
 Zcompare_EGAL -> Zcompare_EQUAL