adds the possibility to have terms (and not just identifiers) as hints

Adds the 'Reserved Notation' command


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

2 files changed, 30 insertions, 0 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 36b9b678de..6282d1860d 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -78,6 +78,8 @@ and ct_COMMAND =
   | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM
   | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
+  | CT_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
+  | CT_hints_resolve of ct_FORMULA_NE_LIST * ct_ID_LIST
   | CT_implicits of ct_ID * ct_ID_LIST_OPT
   | CT_import_id of ct_ID_NE_LIST
   | CT_ind_scheme of ct_SCHEME_SPEC_LIST
@@ -90,8 +92,11 @@ and ct_COMMAND =
   | CT_local_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_local_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_local_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
+  | CT_local_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
+  | CT_local_hints_resolve of ct_FORMULA_NE_LIST * ct_ID_LIST
   | CT_local_infix of ct_STRING * ct_ID * ct_MODIFIER_LIST * ct_ID_OPT
   | CT_local_open_scope of ct_ID
+  | CT_local_reserve_notation of ct_STRING * ct_MODIFIER_LIST
   | CT_locate of ct_ID
   | CT_locate_file of ct_STRING
   | CT_locate_lib of ct_ID
@@ -144,6 +149,7 @@ and ct_COMMAND =
   | CT_remove_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_require of ct_IMPEXP * ct_SPEC_OPT * ct_ID_NE_LIST_OR_STRING
   | CT_reserve of ct_ID_NE_LIST * ct_FORMULA
+  | CT_reserve_notation of ct_STRING * ct_MODIFIER_LIST
   | CT_reset of ct_ID
   | CT_reset_section of ct_ID
   | CT_restart
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 94d338b10d..ddf005dbd7 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -249,6 +249,14 @@ and fCOMMAND = function
    fID_NE_LIST x2;
    fID_LIST x3;
    fNODE "hints" 3
+| CT_hints_immediate(x1, x2) ->
+   fFORMULA_NE_LIST x1;
+   fID_LIST x2;
+   fNODE "hints_immediate" 2
+| CT_hints_resolve(x1, x2) ->
+   fFORMULA_NE_LIST x1;
+   fID_LIST x2;
+   fNODE "hints_resolve" 2
 | CT_implicits(x1, x2) ->
    fID x1;
    fID_LIST_OPT x2;
@@ -303,6 +311,14 @@ and fCOMMAND = function
    fID_NE_LIST x2;
    fID_LIST x3;
    fNODE "local_hints" 3
+| CT_local_hints_immediate(x1, x2) ->
+   fFORMULA_NE_LIST x1;
+   fID_LIST x2;
+   fNODE "local_hints_immediate" 2
+| CT_local_hints_resolve(x1, x2) ->
+   fFORMULA_NE_LIST x1;
+   fID_LIST x2;
+   fNODE "local_hints_resolve" 2
 | CT_local_infix(x1, x2, x3, x4) ->
    fSTRING x1;
    fID x2;
@@ -312,6 +328,10 @@ and fCOMMAND = function
 | CT_local_open_scope(x1) ->
    fID x1;
    fNODE "local_open_scope" 1
+| CT_local_reserve_notation(x1, x2) ->
+   fSTRING x1;
+   fMODIFIER_LIST x2;
+   fNODE "local_reserve_notation" 2
 | CT_locate(x1) ->
    fID x1;
    fNODE "locate" 1
@@ -456,6 +476,10 @@ and fCOMMAND = function
    fID_NE_LIST x1;
    fFORMULA x2;
    fNODE "reserve" 2
+| CT_reserve_notation(x1, x2) ->
+   fSTRING x1;
+   fMODIFIER_LIST x2;
+   fNODE "reserve_notation" 2
 | CT_reset(x1) ->
    fID x1;
    fNODE "reset" 1