aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_types.ml20
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml95
-rw-r--r--plugins/funind/indfun.ml34
-rw-r--r--plugins/funind/indfun_common.ml7
-rw-r--r--plugins/funind/invfun.ml6
-rw-r--r--plugins/funind/recdef.ml7
7 files changed, 94 insertions, 77 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3edc590cc..64284c6fe 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -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,14 +318,14 @@ 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.type_of ~refresh:true (Global.env ()) evd' value) in
@@ -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
@@ -483,11 +484,10 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
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
@@ -597,7 +597,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
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 =
@@ -633,7 +633,7 @@ let build_scheme fas =
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 *)
@@ -673,14 +673,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
()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 61f03d6f2..bc7e6f8b0 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -388,7 +388,7 @@ let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
| Some id ->
let idref = const_of_id id in
(* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *)
- let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in
+ let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in
(fun u -> constr_head_match u idconstr) (* select only id *)
| None -> (fun u -> isApp u) in (* select calls to any function *)
let info_list = find_fapp test g in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 07efaae27..9d3c0b4b4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,20 +333,20 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in
- let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in
+ let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
+ let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
Environ.push_named (id,value,typ) env
let add_pat_variables pat typ env : Environ.env =
let rec add_pat_variables env pat typ : Environ.env =
- observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty);
+ observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
match pat with
| PatVar(_,na) -> Environ.push_rel (na,None,typ) env
| PatCstr(_,c,patl,na) ->
let Inductiveops.IndType(indf,indargs) =
- try Inductiveops.find_rectype env Evd.empty typ
+ try Inductiveops.find_rectype env (Evd.from_env env) typ
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
@@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env =
~init:(env,[])
)
in
- observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty);
+ observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
res
@@ -393,7 +393,7 @@ let rec pattern_to_term_and_type env typ = function
constr
in
let Inductiveops.IndType(indf,indargs) =
- try Inductiveops.find_rectype env Evd.empty typ
+ try Inductiveops.find_rectype env (Evd.from_env env) typ
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
@@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function
Array.to_list
(Array.init
(cst_narg - List.length patternl)
- (fun i -> Detyping.detype false [] env Evd.empty csta.(i))
+ (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
)
in
let patl_as_term =
@@ -486,9 +486,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
- let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
- let rt_typ = Typing.unsafe_type_of env Evd.empty rt_as_constr in
- let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
+ let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
+ let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+ let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res::args_res.to_avoid in
let res_rt = mkGVar res in
@@ -594,8 +594,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
and combine the two result
*)
let v_res = build_entry_lc env funnames avoid v in
- let v_as_constr,ctx = Pretyping.understand env Evd.empty v in
- let v_type = Typing.unsafe_type_of env Evd.empty v_as_constr in
+ let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
+ let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
let new_env =
match n with
Anonymous -> env
@@ -610,10 +610,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let make_discr = make_discr_match brl in
build_entry_lc_from_case env funnames make_discr el brl avoid
| GIf(_,b,(na,e_option),lhs,rhs) ->
- let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
- let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in
+ let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
- try Inductiveops.find_inductive env Evd.empty b_typ
+ try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
errorlabstrm "" (str "Cannot find the inductive associated to " ++
Printer.pr_glob_constr b ++ str " in " ++
@@ -642,10 +642,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
)
nal
in
- let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
- let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in
+ let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
- try Inductiveops.find_inductive env Evd.empty b_typ
+ try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
errorlabstrm "" (str "Cannot find the inductive associated to " ++
Printer.pr_glob_constr b ++ str " in " ++
@@ -689,8 +689,8 @@ and build_entry_lc_from_case env funname make_discr
in
let types =
List.map (fun (case_arg,_) ->
- let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in
- Typing.unsafe_type_of env Evd.empty case_arg_as_constr
+ let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
+ Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr
) el
in
(****** The next works only if the match is not dependent ****)
@@ -737,11 +737,11 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
List.fold_right
(fun id acc ->
let typ_of_id =
- Typing.unsafe_type_of env_with_pat_ids Evd.empty (mkVar id)
+ Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id)
in
let raw_typ_of_id =
Detyping.detype false []
- env_with_pat_ids Evd.empty typ_of_id
+ env_with_pat_ids (Evd.from_env env) typ_of_id
in
mkGProd (Name id,raw_typ_of_id,acc))
pat_ids
@@ -785,15 +785,15 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
List.map3
(fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
- let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in
+ let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
let pat_as_term = pattern_to_term pat in
List.fold_right
(fun id acc ->
if Id.Set.mem id this_pat_ids
then (Prod (Name id),
- let typ_of_id = Typing.unsafe_type_of new_env Evd.empty (mkVar id) in
+ let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in
let raw_typ_of_id =
- Detyping.detype false [] new_env Evd.empty typ_of_id
+ Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
in
raw_typ_of_id
)::acc
@@ -894,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let new_t =
mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
in
- let t',ctx = Pretyping.understand env Evd.empty new_t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -914,7 +914,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
try
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
- try fst (Pretyping.understand env Evd.empty t)(*FIXME*)
+ try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
with e when Errors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
@@ -937,7 +937,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
with Continue ->
let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
- let ty',ctx = Pretyping.understand env Evd.empty ty in
+ let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
let ind,args' = Inductive.find_inductive env ty' in
let mib,_ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
@@ -949,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
- env Evd.empty
+ env (Evd.from_env env)
p) params)@(Array.to_list
(Array.make
(List.length args' - nparam)
@@ -959,7 +959,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
in
observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
- let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in
+ let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
match kind_of_term eq'_as_constr with
@@ -978,12 +978,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| Name id' ->
(id',Detyping.detype false []
env
- Evd.empty
+ (Evd.from_env env)
arg)::acc
else if isVar var_as_constr
then (destVar var_as_constr,Detyping.detype false []
env
- Evd.empty
+ (Evd.from_env env)
arg)::acc
else acc
)
@@ -1009,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
if is_in_b then b else replace_var_by_term id rt b
in
let new_env =
- let t',ctx = Pretyping.understand env Evd.empty eq' in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
Environ.push_rel (n,None,t') env
in
let new_b,id_to_exclude =
@@ -1047,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
else raise Continue
with Continue ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t',ctx = Pretyping.understand env Evd.empty t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1063,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
end
| _ ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t',ctx = Pretyping.understand env Evd.empty t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1082,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
- let t',ctx = Pretyping.understand env Evd.empty t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
match n with
| Name id ->
let new_env = Environ.push_rel (n,None,t') env in
@@ -1104,8 +1104,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| GLetIn(_,n,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
- let t',ctx = Pretyping.understand env Evd.empty t in
- let type_t' = Typing.unsafe_type_of env Evd.empty t' in
+ let evd = (Evd.from_env env) in
+ let t',ctx = Pretyping.understand env evd t in
+ let evd = Evd.from_env ~ctx env in
+ let type_t' = Typing.unsafe_type_of env evd t' in
let new_env = Environ.push_rel (n,Some t',type_t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1129,7 +1131,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
args (crossed_types)
depth t
in
- let t',ctx = Pretyping.understand env Evd.empty new_t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
let new_env = Environ.push_rel (na,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1297,7 +1299,7 @@ let do_build_inductive
let rel_arities = Array.mapi rel_arity funsargs in
Util.Array.fold_left2 (fun env rel_name rel_ar ->
Environ.push_named (rel_name,None,
- fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities
+ fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
@@ -1460,8 +1462,17 @@ let do_build_inductive
let build_inductive evd funconstants funsargs returned_types rtl =
+ let pu = !Detyping.print_universes in
+ let cu = !Constrextern.print_universes in
try
- do_build_inductive evd funconstants funsargs returned_types rtl
- with e when Errors.noncritical e -> raise (Building_graph e)
+ Detyping.print_universes := true;
+ Constrextern.print_universes := true;
+ do_build_inductive evd funconstants funsargs returned_types rtl;
+ Detyping.print_universes := pu;
+ Constrextern.print_universes := cu
+ with e when Errors.noncritical e ->
+ Detyping.print_universes := pu;
+ Constrextern.print_universes := cu;
+ raise (Building_graph e)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d9d059f8f..65dc51a84 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -145,15 +145,14 @@ let interp_casted_constr_with_implicits env sigma impls c =
let build_newrecursive
lnameargsardef =
- let env0 = Global.env()
- and sigma = Evd.empty
- in
+ let env0 = Global.env() in
+ let sigma = Evd.from_env env0 in
let (rec_sign,rec_impls) =
List.fold_left
(fun (env,impls) (((_,recname),_),bl,arityc,_) ->
let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
+ let evdref = ref (Evd.from_env env0) in
let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
(Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
@@ -228,7 +227,7 @@ let process_vernac_interp_error e =
let derive_inversion fix_names =
try
- let evd' = Evd.empty in
+ let evd' = Evd.from_env (Global.env ()) in
(* we first transform the fix_names identifier into their corresponding constant *)
let evd',fix_names_as_constant =
List.fold_right
@@ -355,9 +354,11 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
List.map_i
(fun i x ->
let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
- let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in
+ let env = Global.env () in
+ let evd = ref (Evd.from_env env) in
+ let evd',uprinc = Evd.fresh_global env !evd princ in
let _ = evd := evd' in
- let princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd uprinc in
+ let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
Functional_principles_types.generate_functional_principle
evd
interactive_proof
@@ -394,7 +395,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
evd,((destConst c)::l)
)
- (Evd.empty,[])
+ (Evd.from_env (Global.env ()),[])
fixpoint_exprl
in
evd,List.rev rev_pconstants
@@ -408,7 +409,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
evd,((destConst c)::l)
)
- (Evd.empty,[])
+ (Evd.from_env (Global.env ()),[])
fixpoint_exprl
in
evd,List.rev rev_pconstants
@@ -594,9 +595,9 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
+ let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in
let constr_expr_typel =
- with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in
+ with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_env ~ctx (Global.env ())))) typel in
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
@@ -625,7 +626,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let using_lemmas = [] in
let pre_hook pconstants =
generate_principle
- (ref (Evd.empty))
+ (ref (Evd.from_env (Global.env ())))
pconstants
on_error
true
@@ -649,7 +650,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
let pre_hook pconstants =
generate_principle
- (ref Evd.empty)
+ (ref (Evd.from_env (Global.env ())))
pconstants
on_error
true
@@ -680,7 +681,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let evd,pconstants =
if register_built
then register_struct is_rec fixpoint_exprl
- else (Evd.empty,pconstants)
+ else (Evd.from_env (Global.env ()),pconstants)
in
let evd = ref evd in
generate_principle
@@ -835,10 +836,11 @@ let make_graph (f_ref:global_reference) =
| None -> error "Cannot build a graph over an axiom !"
| Some body ->
let env = Global.env () in
+ let sigma = Evd.from_env env in
let extern_body,extern_type =
with_full_print (fun () ->
- (Constrextern.extern_constr false env Evd.empty body,
- Constrextern.extern_type false env Evd.empty
+ (Constrextern.extern_constr false env sigma body,
+ Constrextern.extern_type false env sigma
((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
)
)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1c409500e..35bd1c36d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -180,9 +180,10 @@ let get_proof_clean do_reduce =
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
- and old_contextual_implicit_args = Impargs.is_contextual_implicit_args ()
- in
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
let old_rawprint = !Flags.raw_print in
+ let old_printuniverses = !Constrextern.print_universes in
+ Constrextern.print_universes := true;
Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
@@ -195,6 +196,7 @@ let with_full_print f a =
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
+ Constrextern.print_universes := old_printuniverses;
Dumpglob.continue ();
res
with
@@ -203,6 +205,7 @@ let with_full_print f a =
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
+ Constrextern.print_universes := old_printuniverses;
Dumpglob.continue ();
raise reraise
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 89ceb751a..d97940142 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let funs_constr = Array.map mkConstU funs in
States.with_state_protection_on_exception
(fun () ->
- let evd = ref Evd.empty in
+ let env = Global.env () in
+ let evd = ref (Evd.from_env env) in
let graphs_constr = Array.map mkInd graphs in
let lemmas_types_infos =
Util.Array.map2_i
@@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
)
funs;
- (* let evd = ref Evd.empty in *)
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
@@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
i*)
let lem_id = mk_complete_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd
+ (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
(fst lemmas_types_infos.(i))
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9de15e407..ca0b9c5fe 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) =
Anonymous)],
GVar(d0,v_id)])
in
- let body = fst (understand env Evd.empty glob_body)(*FIXME*) in
+ let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -1293,8 +1293,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
ref_ := Some lemma ;
let lid = ref [] in
let h_num = ref (-1) in
+ let env = Global.env () in
Proof_global.discard_all ();
- build_proof Evd.empty
+ build_proof (Evd.from_env env)
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
observe_tclTHENLIST (str "")
@@ -1513,7 +1514,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let relation =
fst (*FIXME*)(interp_constr
env_with_pre_rec_args
- Evd.empty
+ (Evd.from_env env_with_pre_rec_args)
r)
in
let tcc_lemma_name = add_suffix function_name "_tcc" in
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 02:10:59 +0000