aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli4
-rw-r--r--library/global.ml5
-rw-r--r--library/global.mli4
-rw-r--r--library/heads.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--printing/prettyp.ml5
-rw-r--r--stm/stm.ml3
-rw-r--r--vernac/assumptions.ml4
-rw-r--r--vernac/lemmas.ml3
11 files changed, 20 insertions, 18 deletions
diff --git a/API/API.mli b/API/API.mli
index a661b34c5..48fd3a682 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2716,8 +2716,8 @@ sig
val type_of_global_unsafe : Globnames.global_reference -> Term.types
val current_dirpath : unit -> Names.DirPath.t
- val body_of_constant_body : Declarations.constant_body -> Term.constr option
- val body_of_constant : Names.Constant.t -> Term.constr option
+ val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
+ val body_of_constant : Names.Constant.t -> (Term.constr * Univ.AUContext.t) option
val add_constraints : Univ.Constraint.t -> unit
end
diff --git a/library/global.ml b/library/global.ml
index cb6334c74..3a74f535d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -126,9 +126,8 @@ let opaque_tables () = Environ.opaque_tables (env ())
let instantiate cb c =
let open Declarations in
match cb.const_universes with
- | Monomorphic_const _ -> c
- | Polymorphic_const ctx ->
- Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
+ | Monomorphic_const _ -> c, Univ.AUContext.empty
+ | Polymorphic_const ctx -> c, ctx
let body_of_constant_body cb =
let open Declarations in
diff --git a/library/global.mli b/library/global.mli
index d9190736f..d6d2f1f85 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -89,8 +89,8 @@ val constant_of_delta_kn : kernel_name -> constant
val mind_of_delta_kn : kernel_name -> mutual_inductive
val opaque_tables : unit -> Opaqueproof.opaquetab
-val body_of_constant : constant -> Term.constr option
-val body_of_constant_body : Declarations.constant_body -> Term.constr option
+val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option
+val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
(** Global universe name <-> level mapping *)
type universe_names =
diff --git a/library/heads.ml b/library/heads.ml
index a1cb81242..c12fa9479 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -132,7 +132,7 @@ let compute_head = function
in
(match body with
| None -> RigidHead (RigidParameter cst)
- | Some c -> kind_of_head env c)
+ | Some (c, _) -> kind_of_head env c)
| EvalVarRef id ->
(match Global.lookup_named id with
| LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ba46f78aa..dc43ea7c4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -957,7 +957,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst evd f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let f_body = Option.get (Global.body_of_constant_body f_def) in
+ let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
let f_body = EConstr.of_constr f_body in
let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1091,7 +1091,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let get_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8ffd15f9f..8c9b514e6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -407,7 +407,7 @@ let get_funs_constant mp dp =
function const ->
let find_constant_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
let body = Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2c5dae1cd..ff7667e99 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -851,7 +851,7 @@ let make_graph (f_ref:global_reference) =
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
- | Some body ->
+ | Some (body, _) ->
let env = Global.env () in
let sigma = Evd.from_env env in
let extern_body,extern_type =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ff12737f6..d1e51c9f3 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -557,9 +557,10 @@ let print_constant with_values sep sp =
print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
Printer.pr_universe_ctx sigma univs
- | _ ->
+ | Some (c, ctx) ->
+ let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
- (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
Printer.pr_universe_ctx sigma univs)
let gallina_print_constant_with_infos sp =
diff --git a/stm/stm.ml b/stm/stm.ml
index fd3d418c1..d38491fec 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1576,8 +1576,9 @@ end = struct (* {{{ *)
let uc =
Option.get
(Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+ let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
let pr =
- Future.from_val (Option.get (Global.body_of_constant_body c)) in
+ Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
let uc =
Future.chain
~pure:true uc Univ.hcons_universe_context_set in
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index db07bbd06..86bbf46a3 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/lemmas.ml b/vernac/lemmas.ml
index 2eeaf4d5d..cfd489dde 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,8 @@ let retrieve_first_recthm = function
(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 map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
+ (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
| _ -> assert false
let adjust_guardness_conditions const = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 18:02:13 +0000