aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml4
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/class.ml6
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/discharge.ml34
-rw-r--r--vernac/discharge.mli3
-rw-r--r--vernac/himsg.ml1
-rw-r--r--vernac/ind_tables.ml203
-rw-r--r--vernac/ind_tables.mli51
-rw-r--r--vernac/indschemes.ml5
-rw-r--r--vernac/lemmas.ml9
-rw-r--r--vernac/obligations.ml36
-rw-r--r--vernac/record.ml51
-rw-r--r--vernac/search.ml4
-rw-r--r--vernac/topfmt.ml51
-rw-r--r--vernac/topfmt.mli4
-rw-r--r--vernac/vernacentries.ml6
17 files changed, 127 insertions, 347 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index db07bbd068..86bbf46a35 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -187,7 +187,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
traverse_object accu body (VarRef id)
| Const (kn, _) ->
- let body () = Global.body_of_constant_body (lookup_constant kn) in
+ let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
traverse_object accu body (ConstRef kn)
| Ind ((mind, _) as ind, _) ->
traverse_inductive accu mind (IndRef ind)
@@ -200,7 +200,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
| Lambda(_,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
- let body () = Global.body_of_constant_body (lookup_constant kn) in
+ let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
| _ ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 248224e6b7..59920742d8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -105,7 +105,7 @@ let mkFullInd (ind,u) n =
else mkIndU (ind,u)
let check_bool_is_defined () =
- try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
+ try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
diff --git a/vernac/class.ml b/vernac/class.ml
index 0b510bbcf0..be682977e5 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -62,7 +62,9 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
let check_reference_arity ref =
- if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then
+ let env = Global.env () in
+ let c, _ = Global.type_of_global_in_context env ref in
+ if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
raise (CoercionError (NotAClass ref))
let check_arity = function
@@ -252,7 +254,7 @@ let warn_uniform_inheritance =
let add_new_coercion_core coef stre poly source target isid =
check_source source;
- let t = Global.type_of_global_unsafe coef in
+ let t, _ = Global.type_of_global_in_context (Global.env ()) coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
let tg,lp = prods_of t in
let llp = List.length lp in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a528b96407..ab1892a18e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -68,7 +68,7 @@ let _ =
let existing_instance glob g info =
let c = global g in
let info = Option.default Hints.empty_hint_info info in
- let instance = Global.type_of_global_unsafe c in
+ let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
let _, r = decompose_prod_assum instance in
match class_of_constr Evd.empty (EConstr.of_constr r) with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
@@ -164,7 +164,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let ctx'' = ctx' @ ctx in
let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
let u = EConstr.EInstance.kind !evars u in
- let cl, u = Typeclasses.typeclass_univ_instance (k, u) in
+ let cl = Typeclasses.typeclass_univ_instance (k, u) in
let _, args =
List.fold_right (fun decl (args, args') ->
match decl with
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b6308aba00..474c0b4dd2 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -77,42 +77,36 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
let ctx = List.rev mip.mind_arity_ctxt in
mkArity (List.rev ctx, Type ar.template_level), true
-let process_inductive (sechyps,abs_ctx) modlist mib =
+let process_inductive (sechyps,_,_ as info) modlist mib =
+ let sechyps = Lib.named_of_variable_context sechyps in
let nparams = mib.mind_nparams in
- let subst, univs =
+ let subst, ind_univs =
match mib.mind_universes with
- | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+ | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
| Polymorphic_ind auctx ->
- Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+ let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let auctx = Univ.AUContext.repr auctx in
+ subst, Polymorphic_ind_entry auctx
| Cumulative_ind cumi ->
let auctx = Univ.ACumulativityInfo.univ_context cumi in
- Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+ let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let auctx = Univ.AUContext.repr auctx in
+ subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
in
+ let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
Array.map_to_list
(fun mip ->
let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
- let arity = expmod_constr modlist ty in
- let arity = Vars.subst_instance_constr subst arity in
- let lc = Array.map
- (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c))
- mip.mind_user_lc
- in
+ let arity = discharge ty in
+ let lc = Array.map discharge mip.mind_user_lc in
(mip.mind_typename,
arity, template,
Array.to_list mip.mind_consnames,
Array.to_list lc))
mib.mind_packets in
- let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
+ let sechyps' = Context.Named.map discharge sechyps in
let (params',inds') = abstract_inductive sechyps' nparams inds in
- let abs_ctx = Univ.instantiate_univ_context abs_ctx in
- let univs = Univ.UContext.union abs_ctx univs in
- let ind_univs =
- match mib.mind_universes with
- | Monomorphic_ind _ -> Monomorphic_ind_entry univs
- | Polymorphic_ind _ -> Polymorphic_ind_entry univs
- | Cumulative_ind _ ->
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
let record = match mib.mind_record with
| Some (Some (id, _, _)) -> Some (Some id)
| Some None -> Some None
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index a0dabe2f46..c8c7e3b8b8 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,5 +11,4 @@ open Entries
open Opaqueproof
val process_inductive :
- ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
- -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ca3fb392fe..784c6d3387 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,6 +909,7 @@ let explain_not_match_error = function
quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
| IncompatibleConstraints cst ->
str " the expected (polymorphic) constraints do not imply " ++
+ let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
let explain_signature_mismatch l spec why =
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
deleted file mode 100644
index 0407c1e36a..0000000000
--- a/vernac/ind_tables.ml
+++ /dev/null
@@ -1,203 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* File created by Vincent Siles, Oct 2007, extended into a generic
- support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
-
-(* This file provides support for registering inductive scheme builders,
- declaring schemes and generating schemes on demand *)
-
-open Names
-open Mod_subst
-open Libobject
-open Nameops
-open Declarations
-open Term
-open CErrors
-open Util
-open Declare
-open Entries
-open Decl_kinds
-open Pp
-
-(**********************************************************************)
-(* Registering schemes in the environment *)
-
-type mutual_scheme_object_function =
- internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
-type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
-
-type 'a scheme_kind = string
-
-let scheme_map = Summary.ref Indmap.empty ~name:"Schemes"
-
-let pr_scheme_kind = Pp.str
-
-let cache_one_scheme kind (ind,const) =
- let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in
- scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map
-
-let cache_scheme (_,(kind,l)) =
- Array.iter (cache_one_scheme kind) l
-
-let subst_one_scheme subst (ind,const) =
- (* Remark: const is a def: the result of substitution is a constant *)
- (subst_ind subst ind,subst_constant subst const)
-
-let subst_scheme (subst,(kind,l)) =
- (kind,Array.map (subst_one_scheme subst) l)
-
-let discharge_scheme (_,(kind,l)) =
- Some (kind,Array.map (fun (ind,const) ->
- (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
-
-let inScheme : string * (inductive * constant) array -> obj =
- declare_object {(default_object "SCHEME") with
- cache_function = cache_scheme;
- load_function = (fun _ -> cache_scheme);
- subst_function = subst_scheme;
- classify_function = (fun obj -> Substitute obj);
- discharge_function = discharge_scheme}
-
-(**********************************************************************)
-(* The table of scheme building functions *)
-
-type individual
-type mutual
-
-type scheme_object_function =
- | MutualSchemeFunction of mutual_scheme_object_function
- | IndividualSchemeFunction of individual_scheme_object_function
-
-let scheme_object_table =
- (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
-
-let declare_scheme_object s aux f =
- let () =
- if not (Id.is_valid ("ind" ^ s)) then
- user_err Pp.(str ("Illegal induction scheme suffix: " ^ s))
- in
- let key = if String.is_empty aux then s else aux in
- try
- let _ = Hashtbl.find scheme_object_table key in
-(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
- user_err ~hdr:"IndTables.declare_scheme_object"
- (str "Scheme object " ++ str key ++ str " already declared.")
- with Not_found ->
- Hashtbl.add scheme_object_table key (s,f);
- key
-
-let declare_mutual_scheme_object s ?(aux="") f =
- declare_scheme_object s aux (MutualSchemeFunction f)
-
-let declare_individual_scheme_object s ?(aux="") f =
- declare_scheme_object s aux (IndividualSchemeFunction f)
-
-(**********************************************************************)
-(* Defining/retrieving schemes *)
-
-let declare_scheme kind indcl =
- Lib.add_anonymous_leaf (inScheme (kind,indcl))
-
-let () = Declare.set_declare_scheme declare_scheme
-
-let is_visible_name id =
- try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true
- with Not_found -> false
-
-let compute_name internal id =
- match internal with
- | UserAutomaticRequest | UserIndividualRequest -> id
- | InternalTacticRequest ->
- Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
-
-let define internal id c p univs =
- let fd = declare_constant ~internal in
- let id = compute_name internal id in
- let ctx = Evd.normalize_evar_universe_context univs in
- let c = Vars.subst_univs_fn_constr
- (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
- let entry = {
- const_entry_body =
- Future.from_val ((c,Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_polymorphic = p;
- const_entry_universes = Evd.evar_context_universe_context ctx;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
- let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
- let () = match internal with
- | InternalTacticRequest -> ()
- | _-> definition_message id
- in
- kn
-
-let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
- let (c, ctx), eff = f mode ind in
- let mib = Global.lookup_mind mind in
- let id = match idopt with
- | Some id -> id
- | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
- let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
- declare_scheme kind [|ind,const|];
- const, Safe_typing.add_private
- (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
-
-let define_individual_scheme kind mode names (mind,i as ind) =
- match Hashtbl.find scheme_object_table kind with
- | _,MutualSchemeFunction f -> assert false
- | s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f mode names ind
-
-let define_mutual_scheme_base kind suff f mode names mind =
- let (cl, ctx), eff = f mode mind in
- let mib = Global.lookup_mind mind in
- let ids = Array.init (Array.length mib.mind_packets) (fun i ->
- try Int.List.assoc i names
- with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
- let consts = Array.map2 (fun id cl ->
- define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
- let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
- declare_scheme kind schemes;
- consts,
- Safe_typing.add_private
- (Safe_typing.private_con_of_scheme
- ~kind (Global.safe_env()) (Array.to_list schemes))
- eff
-
-let define_mutual_scheme kind mode names mind =
- match Hashtbl.find scheme_object_table kind with
- | _,IndividualSchemeFunction _ -> assert false
- | s,MutualSchemeFunction f ->
- define_mutual_scheme_base kind s f mode names mind
-
-let find_scheme_on_env_too kind ind =
- let s = String.Map.find kind (Indmap.find ind !scheme_map) in
- s, Safe_typing.add_private
- (Safe_typing.private_con_of_scheme
- ~kind (Global.safe_env()) [ind, s])
- Safe_typing.empty_private_constants
-
-let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
- try find_scheme_on_env_too kind ind
- with Not_found ->
- match Hashtbl.find scheme_object_table kind with
- | s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f mode None ind
- | s,MutualSchemeFunction f ->
- let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
- ca.(i), eff
-
-let check_scheme kind ind =
- try let _ = find_scheme_on_env_too kind ind in true
- with Not_found -> false
diff --git a/vernac/ind_tables.mli b/vernac/ind_tables.mli
deleted file mode 100644
index 005555caa0..0000000000
--- a/vernac/ind_tables.mli
+++ /dev/null
@@ -1,51 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Term
-open Names
-open Declare
-
-(** This module provides support for registering inductive scheme builders,
- declaring schemes and generating schemes on demand *)
-
-(** A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *)
-
-type mutual
-type individual
-type 'a scheme_kind
-
-type mutual_scheme_object_function =
- internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
-type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
-
-(** Main functions to register a scheme builder *)
-
-val declare_mutual_scheme_object : string -> ?aux:string ->
- mutual_scheme_object_function -> mutual scheme_kind
-
-val declare_individual_scheme_object : string -> ?aux:string ->
- individual_scheme_object_function ->
- individual scheme_kind
-
-(** Force generation of a (mutually) scheme with possibly user-level names *)
-
-val define_individual_scheme : individual scheme_kind ->
- internal_flag (** internal *) ->
- Id.t option -> inductive -> constant * Safe_typing.private_constants
-
-val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
- (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
-
-(** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
-
-val check_scheme : 'a scheme_kind -> inductive -> bool
-
-
-val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6d93f0e410..3d97a767c8 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -383,9 +383,8 @@ let do_mutual_induction_scheme lnamedepindsort =
match inst with
| None ->
let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
- let ctxs = Univ.ContextSet.of_context ctx in
- let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in
- let u = Univ.UContext.instance ctx in
+ let u, ctx = Universes.fresh_instance_from ctx None in
+ let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in
evd, (ind,u), Some u
| Some ui -> evd, (ind, ui), inst
in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2eeaf4d5dc..645320c603 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -44,12 +44,15 @@ let call_hook fix_exn hook l c =
(* Support for mutually proved theorems *)
-let retrieve_first_recthm = function
+let retrieve_first_recthm uctx = function
| VarRef id ->
(NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
- (Global.body_of_constant_body cb, is_opaque cb)
+ let (_, uctx) = UState.universe_context uctx in
+ let inst = Univ.UContext.instance uctx in
+ let map (c, ctx) = Vars.subst_instance_constr inst c in
+ (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
| _ -> assert false
let adjust_guardness_conditions const = function
@@ -412,7 +415,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let other_thms_data =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
- let body,opaq = retrieve_first_recthm ref in
+ let body,opaq = retrieve_first_recthm ctx ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
let ctx = UState.context_set (*FIXME*) ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57d..10d3317f8d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -285,7 +285,7 @@ type obligation =
{ obl_name : Id.t;
obl_type : types;
obl_location : Evar_kinds.t Loc.located;
- obl_body : constant obligation_body option;
+ obl_body : pconstant obligation_body option;
obl_status : bool * Evar_kinds.obligation_definition_status;
obl_deps : Int.Set.t;
obl_tac : unit Proofview.tactic option;
@@ -350,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations
let _ =
declare_bool_option
- { optdepr = true;
+ { optdepr = true; (* remove in 8.8 *)
optname = "Shrinking of Program obligations";
optkey = ["Shrink";"Obligations"];
optread = get_shrink_obligations;
@@ -358,18 +358,8 @@ let _ =
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-let get_body obl =
- match obl.obl_body with
- | None -> None
- | Some (DefinedObl c) ->
- let u = Environ.constant_instance (Global.env ()) c in
- let pc = (c, u) in
- Some (DefinedObl pc)
- | Some (TermObl c) ->
- Some (TermObl c)
-
let get_obligation_body expand obl =
- match get_body obl with
+ match obl.obl_body with
| None -> None
| Some c ->
if expand && snd obl.obl_status == Evar_kinds.Expand then
@@ -664,7 +654,7 @@ let declare_obligation prg obl body ty uctx =
definition_message obl.obl_name;
true, { obl with obl_body =
if poly then
- Some (DefinedObl constant)
+ Some (DefinedObl (constant, Univ.UContext.instance uctx))
else
Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
@@ -892,20 +882,22 @@ let obligation_hook prg obl num auto ctx' _ gr =
if not transparent then err_not_transp ()
| _ -> ()
in
- let obl = { obl with obl_body = Some (DefinedObl cst) } in
- let () = if transparent then add_hint true prg cst in
- let obls = Array.copy obls in
- let _ = obls.(num) <- obl in
let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
- let ctx' =
+ let inst, ctx' =
if not (pi2 prg.prg_kind) (* Not polymorphic *) then
(* The universe context was declared globally, we continue
from the new global environment. *)
let evd = Evd.from_env (Global.env ()) in
let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
- Evd.evar_universe_context ctx'
- else ctx'
+ Univ.Instance.empty, Evd.evar_universe_context ctx'
+ else
+ let (_, uctx) = UState.universe_context ctx' in
+ Univ.UContext.instance uctx, ctx'
in
+ let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
+ let () = if transparent then add_hint true prg cst in
+ let obls = Array.copy obls in
+ let _ = obls.(num) <- obl in
let prg = { prg with prg_ctx = ctx' } in
let () =
try ignore (update_obls prg obls (pred rem))
@@ -1132,7 +1124,7 @@ let admit_prog prg =
(ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
- obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
+ obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
| Some _ -> ())
obls;
ignore(update_obls prg obls 0)
diff --git a/vernac/record.ml b/vernac/record.ml
index d61f44cac8..63ca227862 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,16 +265,10 @@ let warn_non_primitive_record =
let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
- let u = Declareops.inductive_polymorphic_instance mib in
- let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let poly = Declareops.inductive_is_polymorphic mib in
- let ctx =
- match mib.mind_universes with
- | Monomorphic_ind ctx -> ctx
- | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
- | Cumulative_ind cumi ->
- Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
- in
+ let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
+ let u = Univ.UContext.instance ctx in
+ let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -334,8 +328,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_polymorphic = poly;
- const_entry_universes =
- if poly then ctx else Univ.UContext.empty;
+ const_entry_universes = ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
@@ -431,6 +424,12 @@ let declare_structure finite univs id idbuild paramimpls params arity template
let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
+ let fields =
+ if poly then
+ let subst, _ = Univ.abstract_universes ctx in
+ Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
+ else fields
+ in
let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
let build = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
@@ -518,8 +517,18 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
| None -> None)
params, params
in
+ let univs, ctx_context, fields =
+ if poly then
+ let usubst, auctx = Univ.abstract_universes ctx in
+ let map c = Vars.subst_univs_level_constr usubst c in
+ let fields = Context.Rel.map map fields in
+ let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
+ auctx, ctx_context, fields
+ else Univ.AUContext.empty, ctx_context, fields
+ in
let k =
- { cl_impl = impl;
+ { cl_univs = univs;
+ cl_impl = impl;
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique;
cl_context = ctx_context;
@@ -530,10 +539,11 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
let add_constant_class cst =
- let ty = Universes.unsafe_type_of_global (ConstRef cst) in
+ let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in
let ctx, arity = decompose_prod_assum ty in
let tc =
- { cl_impl = ConstRef cst;
+ { cl_univs = univs;
+ cl_impl = ConstRef cst;
cl_context = (List.map (const None) ctx, ctx);
cl_props = [LocalAssum (Anonymous, arity)];
cl_projs = [];
@@ -547,12 +557,13 @@ let add_inductive_class ind =
let mind, oneind = Global.lookup_inductive ind in
let k =
let ctx = oneind.mind_arity_ctxt in
- let inst = Declareops.inductive_polymorphic_instance mind in
- let ty = Inductive.type_of_inductive
- (push_rel_context ctx (Global.env ()))
- ((mind,oneind),inst)
- in
- { cl_impl = IndRef ind;
+ let univs = Declareops.inductive_polymorphic_context mind in
+ let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in
+ let env = push_rel_context ctx env in
+ let inst = Univ.make_abstract_instance univs in
+ let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+ { cl_univs = univs;
+ cl_impl = IndRef ind;
cl_context = List.map (const None) ctx, ctx;
cl_props = [LocalAssum (Anonymous, ty)];
cl_projs = [];
diff --git a/vernac/search.ml b/vernac/search.ml
index 00536e52ec..0f56f81e74 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -78,14 +78,14 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
let gr = ConstRef cst in
- let typ = Global.type_of_global_unsafe gr in
+ let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
fn gr env typ
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in
let mib = Global.lookup_mind mind in
let iter_packet i mip =
let ind = (mind, i) in
- let u = Declareops.inductive_polymorphic_instance mib in
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let i = (ind, u) in
let typ = Inductiveops.type_of_inductive env i in
let () = fn (IndRef ind) env typ in
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index b3810f7d53..e7b14309d1 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -149,7 +149,7 @@ let gen_logger dbg warn ?pre_hdr level msg = match level with
(** Standard loggers *)
(* We provide a generic clear_log_backend callback for backends
- wanting to do clenaup after the print.
+ wanting to do cleanup after the print.
*)
let std_logger_cleanup = ref (fun () -> ())
@@ -207,6 +207,8 @@ let make_style_stack () =
italic = Some false;
underline = Some false;
negative = Some false;
+ prefix = None;
+ suffix = None;
})
in
let style_stack = ref [] in
@@ -235,20 +237,49 @@ let make_style_stack () =
let clear () = style_stack := [] in
push, pop, clear
-let init_color_output () =
+let make_printing_functions () =
+ let empty = Terminal.make () in
+ let print_prefix ft tag =
+ let style =
+ try CString.Map.find tag !tag_map
+ with | Not_found -> empty
+ in
+ match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> ()
+ in
+ let print_suffix ft tag =
+ let style =
+ try CString.Map.find tag !tag_map
+ with | Not_found -> empty
+ in
+ match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> ()
+ in
+ print_prefix, print_suffix
+
+let init_terminal_output ~color =
init_tag_map (default_tag_map ());
let push_tag, pop_tag, clear_tag = make_style_stack () in
- std_logger_cleanup := clear_tag;
- let tag_handler = {
+ let print_prefix, print_suffix = make_printing_functions () in
+ let tag_handler ft = {
Format.mark_open_tag = push_tag;
Format.mark_close_tag = pop_tag;
- Format.print_open_tag = ignore;
- Format.print_close_tag = ignore;
+ Format.print_open_tag = print_prefix ft;
+ Format.print_close_tag = print_suffix ft;
} in
- Format.pp_set_mark_tags !std_ft true;
- Format.pp_set_mark_tags !err_ft true;
- Format.pp_set_formatter_tag_functions !std_ft tag_handler;
- Format.pp_set_formatter_tag_functions !err_ft tag_handler
+ if color then
+ (* Use 0-length markers *)
+ begin
+ std_logger_cleanup := clear_tag;
+ Format.pp_set_mark_tags !std_ft true;
+ Format.pp_set_mark_tags !err_ft true
+ end
+ else
+ (* Use textual markers *)
+ begin
+ Format.pp_set_print_tags !std_ft true;
+ Format.pp_set_print_tags !err_ft true
+ end;
+ Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft);
+ Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft)
(* Rules for emacs:
- Debug/info: emacs_quote_info
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0e781bcc1b..6e006fc6c9 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -41,11 +41,13 @@ val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds ->
val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
(** Color output *)
-val init_color_output : unit -> unit
val clear_styles : unit -> unit
val parse_color_config : string -> unit
val dump_tags : unit -> (string * Terminal.style) list
+(** Initialization of interpretation of tags *)
+val init_terminal_output : color:bool -> unit
+
(** Error printing *)
(* To be deprecated when we can fully move to feedback-based error
printing. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bbec28afff..9650ea19d7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -986,7 +986,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let sr = smart_global reference in
let inf_names =
- let ty = Global.type_of_global_unsafe sr in
+ let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
Impargs.compute_implicits_names (Global.env ()) ty
in
let prev_names =
@@ -1811,9 +1811,9 @@ let vernac_end_subproof () =
Proof_global.simple_with_current_proof (fun _ p ->
Proof.unfocus subproof_kind p ())
-let vernac_bullet (bullet:Proof_global.Bullet.t) =
+let vernac_bullet (bullet : Proof_bullet.t) =
Proof_global.simple_with_current_proof (fun _ p ->
- Proof_global.Bullet.put p bullet)
+ Proof_bullet.put p bullet)
let vernac_show = let open Feedback in function
| ShowScript -> assert false (* Only the stm knows the script *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 15:57:40 +0000