aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml7
-rw-r--r--vernac/command.ml13
-rw-r--r--vernac/command.mli4
-rw-r--r--vernac/mltop.ml2
-rw-r--r--vernac/obligations.ml9
-rw-r--r--vernac/obligations.mli3
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/topfmt.ml17
8 files changed, 35 insertions, 22 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index cb1d2f7c73..3e47f881c1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -114,9 +114,10 @@ let instance_hook k info global imps ?hook cst =
let declare_instance_constant k info global imps ?hook id decl poly evm term termtype =
let kind = IsDefinition Instance in
- let evm =
- let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
- (Univops.universes_of_constr term) in
+ let evm =
+ let env = Global.env () in
+ let levels = Univ.LSet.union (Univops.universes_of_constr env termtype)
+ (Univops.universes_of_constr env term) in
Evd.restrict_universe_context evm levels
in
let uctx = Evd.check_univ_decl ~poly evm decl in
diff --git a/vernac/command.ml b/vernac/command.ml
index 66d4fe9847..23be2c3082 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -105,7 +105,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
- let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
let () = evdref := Evd.restrict_universe_context !evdref vars in
let uctx = Evd.check_univ_decl ~poly !evdref decl in
imps1@(Impargs.lift_implicits nb_args imps2),
@@ -130,8 +130,8 @@ let interp_definition pl bl poly red_option c ctypopt =
in
if not (try List.for_all chk imps2 with Not_found -> false)
then warn_implicits_in_term ();
- let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
- let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+ let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
+ let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in
let vars = Univ.LSet.union bodyvars tyvars in
let () = evdref := Evd.restrict_universe_context !evdref vars in
let uctx = Evd.check_univ_decl ~poly !evdref decl in
@@ -315,7 +315,7 @@ let do_assumptions kind nl l =
let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in
let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
let t = nf_evar t in
- let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+ let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
uvars, (coe,t,imps))
Univ.LSet.empty l
in
@@ -1188,7 +1188,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
let env = Global.env() in
let indexes = search_guard env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
- let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+ let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
@@ -1221,7 +1221,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
- let vars = Univops.universes_of_constr (List.hd fixdecls) in
+ let env = Global.env () in
+ let vars = Univops.universes_of_constr env (List.hd fixdecls) in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
diff --git a/vernac/command.mli b/vernac/command.mli
index a1f916c782..c7342e6da9 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -82,7 +82,7 @@ type one_inductive_impls =
val interp_mutual_inductive :
structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
- polymorphic -> private_flag -> Decl_kinds.recursivity_kind ->
+ polymorphic -> private_flag -> Declarations.recursivity_kind ->
mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
(** Registering a mutual inductive definition together with its
@@ -96,7 +96,7 @@ val declare_mutual_inductive_with_eliminations :
val do_mutual_inductive :
(one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
- polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit
+ polymorphic -> private_flag -> Declarations.recursivity_kind -> unit
(** {6 Fixpoints and cofixpoints} *)
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index d3de10235f..00554e3bae 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -378,7 +378,7 @@ let unfreeze_ml_modules x =
(fun (name,path) -> trigger_ml_object false false false ?path name) x
let _ =
- Summary.declare_summary Summary.ml_modules
+ Summary.declare_ml_modules_summary
{ Summary.freeze_function = (fun _ -> get_loaded_modules ());
Summary.unfreeze_function = unfreeze_ml_modules;
Summary.init_function = reset_loaded_modules }
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 24d6649515..181068089e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-let from_prg : program_info ProgMap.t ref =
- Summary.ref ProgMap.empty ~name:"program-tcc-table"
+let from_prg, program_tcc_summary_tag =
+ Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
let close sec =
if not (ProgMap.is_empty !from_prg) then
@@ -477,7 +477,10 @@ let declare_definition prg =
let fix_exn = Hook.get get_fix_exn () in
let typ = nf typ in
let body = nf body in
- let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in
+ let env = Global.env () in
+ let uvars = Univ.LSet.union
+ (Univops.universes_of_constr env typ)
+ (Univops.universes_of_constr env body) in
let uctx = UState.restrict prg.prg_ctx uvars in
let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 0602e52e9a..bdc97d48c0 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option
val explain_no_obligations : Names.Id.t option -> Pp.t
val set_program_mode : bool -> unit
+
+type program_info
+val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag
diff --git a/vernac/record.mli b/vernac/record.mli
index 9fdd5e1c46..e632e7bbff 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -15,7 +15,7 @@ val primitive_flag : bool ref
val definition_structure :
inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
- Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
+ Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 6a10eb43a2..7e96f28de4 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -288,7 +288,6 @@ let init_terminal_output ~color =
*)
let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
-
(* This is specific to the toplevel *)
let pr_loc loc =
let fname = loc.Loc.fname in
@@ -311,17 +310,23 @@ let print_err_exn ?extra any =
std_logger ~pre_hdr Feedback.Error msg
let with_output_to_file fname func input =
- (* XXX FIXME: redirect std_ft *)
- (* let old_logger = !logger in *)
let channel = open_out (String.concat "." [fname; "out"]) in
- (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *)
+ let old_fmt = !std_ft, !err_ft, !deep_ft in
+ let new_ft = Format.formatter_of_out_channel channel in
+ std_ft := new_ft;
+ err_ft := new_ft;
+ deep_ft := new_ft;
try
let output = func input in
- (* logger := old_logger; *)
+ std_ft := Util.pi1 old_fmt;
+ err_ft := Util.pi2 old_fmt;
+ deep_ft := Util.pi3 old_fmt;
close_out channel;
output
with reraise ->
let reraise = Backtrace.add_backtrace reraise in
- (* logger := old_logger; *)
+ std_ft := Util.pi1 old_fmt;
+ err_ft := Util.pi2 old_fmt;
+ deep_ft := Util.pi3 old_fmt;
close_out channel;
Exninfo.iraise reraise
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:53:51 +0000