summaryrefslogtreecommitdiff
path: root/plugins/funind/functional_principles_types.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
-rw-r--r--plugins/funind/functional_principles_types.ml68
1 files changed, 33 insertions, 35 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 45e5aaf5..c47602bd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -274,7 +274,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
let new_princ_name =
next_ident_away_in_goal (Id.of_string "___________princ_________") []
in
- let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in
+ let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
let hook = Lemmas.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
@@ -303,7 +303,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
try
let f = funs.(i) in
- let type_sort = Universes.new_sort_in_family InType in
+ let env = Global.env () in
+ let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -317,23 +318,23 @@ let generate_functional_principle (evd: Evd.evar_map ref)
id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
in
let names = ref [new_princ_name] in
- let evd' = !evd in
let hook =
fun new_principle_type _ _ ->
if Option.is_empty sorts
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
- let s = Universes.new_sort_in_family fam_sort in
+ let evd' = Evd.from_env (Global.env ()) in
+ let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
- let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in
+ let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in
+ let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
ignore(
Declare.declare_constant
name
- (Entries.DefinitionEntry ce,
+ (DefinitionEntry ce,
Decl_kinds.IsDefinition (Decl_kinds.Scheme))
);
Declare.definition_message name;
@@ -394,7 +395,7 @@ let get_funs_constant mp dp =
let body = Tacred.cbv_norm_flags
(Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
(Global.env ())
- (Evd.empty)
+ (Evd.from_env (Global.env ()))
body
in
body
@@ -446,7 +447,7 @@ let get_funs_constant mp dp =
exception No_graph_found
exception Found_type of int
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
@@ -478,16 +479,15 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
in
let _ = evd := sigma in
let l_schemes =
- List.map (Typing.type_of env sigma) schemes
+ List.map (Typing.unsafe_type_of env sigma) schemes
in
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x)
)
fas
in
- evd:=sigma;
(* We create the first priciple by tactic *)
let first_type,other_princ_types =
match l_schemes with
@@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
let sorts = Array.of_list sorts in
List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+ let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = destFix fix in
let other_result =
@@ -585,30 +585,29 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
in
{const with
- Entries.const_entry_body =
- (Future.from_val (Term_typing.mk_pure_proof princ_body));
- Entries.const_entry_type = Some scheme_type
+ const_entry_body =
+ (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+ const_entry_type = Some scheme_type
}
)
other_fun_princ_types
in
const::other_result
-
let build_scheme fas =
- Dumpglob.pause ();
- let evd = (ref Evd.empty) in
+ let evd = (ref (Evd.from_env (Global.env ()))) in
let pconstants = (List.map
(fun (_,f,sort) ->
let f_as_constant =
try
Smartlocate.global_with_alias f
with Not_found ->
- Errors.error ("Cannot find "^ Libnames.string_of_reference f)
+ errorlabstrm "FunInd.build_scheme"
+ (str "Cannot find " ++ Libnames.pr_reference f)
in
let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
- let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in
- let _ = evd := evd' in
+ let _ = evd := evd' in
+ let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in
(destConst f,sort)
)
fas
@@ -621,25 +620,24 @@ let build_scheme fas =
ignore
(Declare.declare_constant
princ_id
- (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+ (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
Declare.definition_message princ_id
)
fas
- bodies_types;
- Dumpglob.continue ()
-
-
+ bodies_types
let build_case_scheme fa =
let env = Global.env ()
- and sigma = Evd.empty in
+ and sigma = (Evd.from_env (Global.env ())) in
(* let id_to_constr id = *)
(* Constrintern.global_reference id *)
(* in *)
- let funs = (fun (_,f,_) ->
- try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
- with Not_found ->
- Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+ let funs =
+ let (_,f,_) = fa in
+ try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+ with Not_found ->
+ errorlabstrm "FunInd.build_case_scheme"
+ (str "Cannot find " ++ Libnames.pr_reference f) in
let first_fun,u = destConst funs in
let funs_mp,funs_dp,_ = Names.repr_con first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -656,7 +654,7 @@ let build_case_scheme fa =
in
let sigma, scheme =
(fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in
- let scheme_type = (Typing.type_of env sigma ) scheme in
+ let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in
let sorts =
(fun (_,_,x) ->
Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
@@ -670,14 +668,14 @@ let build_case_scheme fa =
);
*)
generate_functional_principle
- (ref Evd.empty)
+ (ref (Evd.from_env (Global.env ())))
false
scheme_type
(Some ([|sorts|]))
(Some princ_name)
this_block_funs
0
- (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|])
+ (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
in
()
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 18:03:19 +0000