diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/funind/recdef.ml | 12 | ||||
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 182 | ||||
-rw-r--r-- | plugins/ltac/pptactic.mli | 25 | ||||
-rw-r--r-- | plugins/ltac/taccoerce.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 18 | ||||
-rw-r--r-- | plugins/micromega/persistent_cache.ml | 4 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml | 3 |
8 files changed, 169 insertions, 79 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b..766adfc63 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 34fea6175..8b9eb3983 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -471,7 +471,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> + [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d70751245..6aa2f6f89 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,24 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function | ListArg t -> aux t ^ "_list" @@ -127,9 +145,9 @@ let string_of_genarg_arg (ArgumentType arg) = | Some Refl -> let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -723,8 +741,10 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> - hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -1192,42 +1212,77 @@ let declare_extra_genarg_pprule wit | ExtraArg s -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = + Genprint.PrinterBasic (fun () -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = + Genprint.PrinterBasic (fun () -> let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) in let h x = - Genprint.PrinterNeedsContext (fun env sigma -> + Genprint.TopPrinterNeedsContext (fun env sigma -> h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_genarg_pprule_with_level wit + (f : 'a raw_extra_genarg_printer_with_level) + (g : 'b glob_extra_genarg_printer_with_level) + (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded = + begin match wit with + | ExtraArg s -> () + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") + end; + let open Genprint in + let f x = + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + let g x = + let env = Global.env () in + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + in + let h x = + TopPrinterNeedsContextAndLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun env sigma n -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } + in + Genprint.register_print0 wit f g h + let declare_extra_vernac_genarg_pprule wit f = - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in Genprint.register_vernac_print0 wit f (** Registering *) -let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in Miscprint.pr_intro_pattern print_constr p) -let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) -let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in Miscprint.pr_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in pr_with_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, c = match c with | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) | clear_flag,ElimOnAnonHyp n as x -> sigma, x @@ -1236,12 +1291,16 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) let make_constr_printer f c = - Genprint.PrinterNeedsContextAndLevel { + Genprint.TopPrinterNeedsContextAndLevel { Genprint.default_already_surrounded = Ppconstr.ltop; Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) + +let register_basic_print0 wit f g h = + Genprint.register_print0 wit (lift f) (lift g) (lift_top h) let pr_glob_constr_pptac c = @@ -1255,80 +1314,81 @@ let pr_lglob_constr_pptac c = let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) (lift int); - Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); - Genprint.register_print0 wit_ident - pr_id pr_id (lift pr_id); - Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) (lift pr_id); - Genprint.register_print0 + let open Genprint in + register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_ident pr_id pr_id pr_id; + register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_print0 wit_intro_pattern - (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) + (lift (Miscprint.pr_intro_pattern pr_constr_expr)) + (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) pr_lident) - (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (lift (pr_clauses (Some true) pr_lident)) + (lift (pr_clauses (Some true) pr_lident)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_lconstr_expr) + (lift (fun (c, _) -> pr_lglob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c,_) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c, _) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; - Genprint.register_print0 wit_red_expr - (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) + Genprint.register_print0 + wit_red_expr + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); - Genprint.register_print0 wit_bindings - (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + register_print0 wit_bindings + (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) + (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_bindings_env ; - Genprint.register_print0 wit_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 wit_open_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_open_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 Tacarg.wit_destruction_arg - (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 Tacarg.wit_destruction_arg + (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) + (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_destruction_arg_env ; - Genprint.register_print0 Stdarg.wit_int int int (lift int); - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); - Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); - Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) + register_basic_print0 Stdarg.wit_int int int int; + register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + register_basic_print0 Stdarg.wit_pre_ident str str str; + register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_tactic printer printer printer + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_tactic printer printer printer + ltop (0,E) let () = - let pr_unit _ _ _ () = str "()" in - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_ltac printer printer pr_unit + let pr_unit _ _ _ _ () = str "()" in + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit + ltop (0,E) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5ecfaf590..bda5774ab 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -40,12 +40,37 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_genarg_pprule_with_level : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer_with_level -> + 'b glob_extra_genarg_printer_with_level -> + 'c extra_genarg_printer_with_level -> + (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> unit diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index c03a86732..9ae112d37 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -33,7 +33,7 @@ let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_bin let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) (fun c -> - Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in + Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 14b79d73e..e0d7eca5f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -242,9 +242,9 @@ let pr_value env v = | None -> str "a value of type" ++ spc () ++ pr_argument_type v in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = @@ -821,9 +821,9 @@ let message_of_value v = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> Ftactic.return (pr ()) - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> Ftactic.return (pr ()) + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function @@ -1353,8 +1353,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = begin let open Genprint in match generic_val_print v with - | PrinterBasic _ -> call_debug None - | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + | TopPrinterBasic _ -> call_debug None + | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ -> Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 49ccb468c..387a52514 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -149,7 +149,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.add htbl key elem ; + Table.replace htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -195,7 +195,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; + Table.replace tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f22f00839..e3e749b75 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) |