Des abbreviations pour constrintern.ml

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

2 files changed, 10 insertions, 13 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f9d927f62..e8e5a4a7c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -26,6 +26,9 @@ open Pcoq
 open Rawterm
 open Libnames
 
+let interp_global_rawconstr_with_vars vars c =
+  interp_rawconstr_gen false Evd.empty (Global.env()) false (vars,[]) c
+
 (*************************
  **** PRETTY-PRINTING ****
  *************************)
@@ -900,8 +903,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
     (* Used only by v7 *)
     if onlyparse then None
     else
-      let r = interp_rawconstr_gen
-          false Evd.empty (Global.env()) [] false (vars,[]) c in
+      let r = interp_global_rawconstr_with_vars vars c in
       Some (make_old_pp_rule n symbols typs r notation scope vars) in
   let onlyparse = onlyparse or !Options.v7_only in
   let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
@@ -982,8 +984,7 @@ let add_notation_v8only local c (df,modifiers) sc =
 		let (vars,symbs) = analyse_tokens toks in
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr vars c in
-		let a_for_old = interp_rawconstr_gen
-		  false Evd.empty (Global.env()) [] false (vars,[]) c in
+		let a_for_old = interp_global_rawconstr_with_vars vars c in
 		add_notation_interpretation_core local symbs None df a sc 
 		  onlyparse true
 	  | Some n ->
@@ -1022,8 +1023,7 @@ let add_notation local c dfmod mv8 sc =
 		let (vars,symbs) = analyse_tokens toks in
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr vars c in
-		let a_for_old = interp_rawconstr_gen
-		  false Evd.empty (Global.env()) [] false (vars,[]) c in
+		let a_for_old = interp_global_rawconstr_with_vars vars c in
 		let for_old = Some (a_for_old,vars) in
 		add_notation_interpretation_core local symbs for_old df a
 		  sc onlyparse false
@@ -1075,8 +1075,7 @@ let add_infix local (inf,modl) pr mv8 sc =
       (* Declare only interpretation *)
       let (vars,symbs) = analyse_tokens toks in
       let a' = interp_aconstr vars a in
-      let a_for_old = interp_rawconstr_gen
-	false Evd.empty (Global.env()) [] false (vars,[]) a in
+      let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
 	onlyparse true
     else
@@ -1104,8 +1103,7 @@ let add_infix local (inf,modl) pr mv8 sc =
     (* Declare only interpretation *)
     let (vars,symbs) = analyse_tokens toks in
     let a' = interp_aconstr vars a in
-    let a_for_old = interp_rawconstr_gen
-      false Evd.empty (Global.env()) [] false (vars,[]) a in
+    let a_for_old = interp_global_rawconstr_with_vars vars a in
     let for_old = Some (a_for_old,vars) in
     add_notation_interpretation_core local symbs for_old df a' sc 
       onlyparse false
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 3b4f3296c..03e83caca 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -577,8 +577,7 @@ let transf istype env n iscast c =
   if Options.do_translate() then
     let r = 
       Constrintern.for_grammar
-        (Constrintern.interp_rawconstr_gen istype Evd.empty env [] false 
-	  ([],[]))
+        (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[]))
 	c in
     begin try
       (* Try to infer old case and type annotations *)
@@ -608,7 +607,7 @@ let transf_pattern env c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env env)
       (Constrintern.for_grammar
-	(Constrintern.interp_rawconstr_gen false Evd.empty env [] true ([],[]))
+	(Constrintern.interp_rawconstr_gen false Evd.empty env true ([],[]))
 	c)
   else c