diff options
| -rw-r--r-- | toplevel/metasyntax.ml | 18 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 5 |
2 files changed, 10 insertions, 13 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index f9d927f627..e8e5a4a7c6 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 3b4f3296cb..03e83caca6 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 |