diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 20 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 95 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 34 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 7 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 6 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 7 |
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 |