diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 11 | ||||
| -rw-r--r-- | vernac/mltop.ml | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 29 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 11 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 4 |
8 files changed, 39 insertions, 28 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1a6eda446c..8f155adb8a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -483,7 +483,7 @@ let save_proof ?proof = function let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in let typ = EConstr.Unsafe.to_constr typ in - let universes = Proof.initial_euctx pftree in + let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 790b62c9d0..3da12e7714 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1359,7 +1359,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:`No in + let fs = Lib.freeze ~marshallable:false in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in @@ -1563,14 +1563,17 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None) let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) - let metas = [inject_var "x"; inject_var "y"] in + let vars = names_of_constr_expr pr in + let x = Namegen.next_ident_away (Id.of_string "x") vars in + let y = Namegen.next_ident_away (Id.of_string "y") vars in + let metas = [inject_var x; inject_var y] in let c = mkAppC (pr,metas) in - let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in + let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in add_notation local env c (df,modifiers) sc (**********************************************************************) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 3620e177fe..8d6268753e 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -394,7 +394,7 @@ let unfreeze_ml_modules x = let _ = Summary.declare_ml_modules_summary - { Summary.freeze_function = (fun _ -> get_loaded_modules ()); + { Summary.freeze_function = (fun ~marshallable -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8535585749..e0dd3380f9 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -700,7 +700,7 @@ open Pputils | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -1134,7 +1134,7 @@ open Pputils let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in @@ -1146,7 +1146,7 @@ open Pputils | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index f26e0d0885..a647b2ef73 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref let () = - register_grammar Stdarg.wit_red_expr (Vernac_.red_expr); + register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr); diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3fa3681661..e6e3db4beb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -82,12 +82,12 @@ let show_proof () = let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls,_,shelf,givenup,sigma = Proof.proof pfts in - pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma) + let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in + pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in - let gls,_,_,_,sigma = Proof.proof pfts in + let Proof.{goals;sigma} = Proof.data pfts in let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx @@ -96,9 +96,9 @@ let show_universes () = let show_intro all = let open EConstr in let pf = Proof_global.give_me_the_proof() in - let gls,_,_,_,sigma = Proof.proof pf in - if not (List.is_empty gls) then begin - let gl = {Evd.it=List.hd gls ; sigma = sigma; } in + let Proof.{goals;sigma} = Proof.data pf in + if not (List.is_empty goals) then begin + let gl = {Evd.it=List.hd goals ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in @@ -1047,8 +1047,9 @@ let vernac_set_end_tac tac = let vernac_set_used_variables e = let env = Global.env () in + let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in let tys = - List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in + List.map snd (initial_goals (Proof_global.give_me_the_proof ())) in let tys = List.map EConstr.Unsafe.to_constr tys in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in @@ -1221,11 +1222,9 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let rec check_extra_args extra_args = match extra_args with | [] -> () - | { notation_scope = None } :: _ -> err_extra_args (names_of extra_args) - | { name = Anonymous; notation_scope = Some _ } :: args -> - check_extra_args args - | _ -> - user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.") + | { notation_scope = None } :: _ -> + user_err Pp.(str"Extra arguments should specify a scope.") + | { notation_scope = Some _ } :: args -> check_extra_args args in let args, scopes = @@ -1817,8 +1816,8 @@ let vernac_global_check c = let get_nth_goal n = let pf = Proof_global.give_me_the_proof() in - let gls,_,_,_,sigma = Proof.proof pf in - let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in + let Proof.{goals;sigma} = Proof.data pf in + let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl exception NoHyp @@ -2437,7 +2436,7 @@ let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + Vernacstate.freeze_interp_state ~marshallable:false with exn -> let exn = CErrors.push exn in Vernacstate.invalidate_cache (); diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index aa8bcdc328..b40bccf27e 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -33,11 +33,18 @@ let do_if_not_cached rf f v = | Some _ -> () -let freeze_interp_state marshallable = +let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); proof = update_cache s_proof (Proof_global.freeze ~marshallable); - shallow = marshallable = `Shallow } + shallow = marshallable } let unfreeze_interp_state { system; proof } = do_if_not_cached s_cache States.unfreeze system; do_if_not_cached s_proof Proof_global.unfreeze proof + +let make_shallow st = + let lib = States.lib_of_state st.system in + { st with + system = States.replace_lib st.system @@ Lib.drop_objects lib; + shallow = true; + } diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b4d478d12d..ed20cb935a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -14,8 +14,10 @@ type t = { shallow : bool (* is the state trimmed down (libstack) *) } -val freeze_interp_state : Summary.marshallable -> t +val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit +val make_shallow : t -> t + (* WARNING: Do not use, it will go away in future releases *) val invalidate_cache : unit -> unit |