3 files changed, 10 insertions, 1 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 9c50109bb3..7cabd850ad 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -53,7 +53,7 @@ GRAMMAR EXTEND Gram
     bignat bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
     ne_string string lstring pattern_ident pattern_identref by_notation
-    smart_global bar_cbrace;
+    smart_global bar_cbrace strategy_level;
   preident:
     [ [ s = IDENT -> { s } ] ]
   ;
@@ -140,4 +140,10 @@ GRAMMAR EXTEND Gram
   bar_cbrace:
     [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
+  strategy_level:
+    [ [ IDENT "expand" -> { Conv_oracle.Expand }
+      | IDENT "opaque" -> { Conv_oracle.Opaque }
+      | n=integer -> { Conv_oracle.Level n }
+      | IDENT "transparent" -> { Conv_oracle.transparent } ] ]
+  ;
 END
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 5b0562fb0d..2cc16f85d5 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -276,6 +276,7 @@ module Prim =
     let reference = make_gen_entry uprim "reference"
     let by_notation = Entry.create "by_notation"
     let smart_global = Entry.create "smart_global"
+    let strategy_level = gec_gen "strategy_level"
 
     (* parsed like ident but interpreted as a term *)
     let var = gec_gen "var"
@@ -505,6 +506,7 @@ let () =
   Grammar.register0 wit_ident (Prim.ident);
   Grammar.register0 wit_var (Prim.var);
   Grammar.register0 wit_ref (Prim.reference);
+  Grammar.register0 wit_smart_global (Prim.smart_global);
   Grammar.register0 wit_sort_family (Constr.sort_family);
   Grammar.register0 wit_constr (Constr.constr);
   ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 90088be307..bd64d21518 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -170,6 +170,7 @@ module Prim :
     val ne_lstring : lstring Entry.t
     val var : lident Entry.t
     val bar_cbrace : unit Entry.t
+    val strategy_level : Conv_oracle.level Entry.t
   end
 
 module Constr :