From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/funind/functional_principles_types.ml | 207 ++++++++++++++------------ 1 file changed, 112 insertions(+), 95 deletions(-) (limited to 'plugins/funind/functional_principles_types.ml') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5e72b867..804548ce 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,9 @@ open Printer open CErrors -open Util open Term +open Sorts +open Util +open Constr open Vars open Namegen open Names @@ -11,8 +13,8 @@ open Tactics open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs -open Misctypes -open Sigma.Notations + +module RelDecl = Context.Rel.Declaration exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -21,25 +23,28 @@ let observe s = if do_observe () then Feedback.msg_debug s +let pop t = Vars.lift (-1) t + (* Transform an inductive induction principle into a functional one *) let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = - let princ_type_info = compute_elim_sig princ_type in + let princ_type = EConstr.of_constr princ_type in + let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in let env = Global.env () in - let env_with_params = Environ.push_rel_context princ_type_info.params env in + let env_with_params = EConstr.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = + let rec change_predicates_names (avoid:Id.t list) (predicates:EConstr.rel_context) : EConstr.rel_context = match predicates with | [] -> [] | decl :: predicates -> (match Context.Rel.Declaration.get_name decl with | Name x -> - let id = Namegen.next_ident_away x avoid in + let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in Hashtbl.add tbl id x; - set_name (Name id) decl :: change_predicates_names (id::avoid) predicates - | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) + RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -51,14 +56,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (get_type decl) in + let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in let real_args = if princ_type_info.indarg_in_concl then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl), - compose_prod real_args (mkSort new_sort)) + Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), + Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = List.map_i @@ -70,18 +75,19 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let rel_as_kn = fst (match princ_type_info.indref with | Some (Globnames.IndRef ind) -> ind - | _ -> error "Not a valid predicate" + | _ -> user_err Pp.(str "Not a valid predicate") ) in let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in let is_pte = let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> - match kind_of_term t with + match Constr.kind t with | Var id -> Id.Set.mem id set | _ -> false in let pre_princ = + let open EConstr in it_mkProd_or_LetIn (it_mkProd_or_LetIn (Option.fold_right @@ -93,28 +99,31 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = ) princ_type_info.branches in + let pre_princ = EConstr.Unsafe.to_constr pre_princ in let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = - match kind_of_term c with + match Constr.kind c with | Ind((u,_),_) -> MutInd.equal u rel_as_kn | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn | _ -> false in let get_fun_num c = - match kind_of_term c with + match Constr.kind c with | Ind((_,num),_) -> num | Construct(((_,num),_),_) -> num | _ -> assert false in let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = - let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in - observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); + let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in + observe (str "replacing " ++ + pr_lconstr_env env Evd.empty c ++ str " by " ++ + pr_lconstr_env env Evd.empty res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = let (new_princ_type,_) as res = - match kind_of_term pre_princ with + match Constr.kind pre_princ with | Rel n -> begin try match Environ.lookup_rel n env with @@ -143,13 +152,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = ([],[]) in let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - applist(new_f, new_args), - list_union_eq eq_constr binders_to_remove_from_f binders_to_remove + applistc new_f new_args, + list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove | LetIn(x,v,t,b) -> compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in -(* let _ = match kind_of_term pre_princ with *) +(* let _ = match Constr.kind pre_princ with *) (* | Prod _ -> *) (* observe(str "compute_new_princ_type for "++ *) (* pr_lconstr_env env pre_princ ++ *) @@ -165,26 +174,26 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( bind_fun(new_x,new_t,new_b), list_union_eq - eq_constr + Constr.equal binders_to_remove_from_t - (List.map Termops.pop binders_to_remove_from_b) + (List.map pop binders_to_remove_from_b) ) with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map Termops.pop binders_to_remove_from_b + new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b) + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin @@ -194,31 +203,31 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( mkLetIn(new_x,new_v,new_t,new_b), list_union_eq - eq_constr - (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) - (List.map Termops.pop binders_to_remove_from_b) + Constr.equal + (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) + (List.map pop binders_to_remove_from_b) ) with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map Termops.pop binders_to_remove_from_b + new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b) + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = let new_e,to_remove_from_e = compute_new_princ_type remove env e in - new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc + new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc in (* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *) let pre_res,_ = @@ -235,20 +244,21 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b)) new_predicates) ) - princ_type_info.params + (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params) let change_property_sort evd toSort princ princName = let open Context.Rel.Declaration in - let princ_info = compute_elim_sig princ in + let princ = EConstr.of_constr princ in + let princ_info = compute_elim_sig evd princ in let change_sort_in_predicate decl = LocalAssum (get_name decl, - let args,ty = decompose_prod (get_type decl) in + let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in let s = destSort ty in Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty); - compose_prod args (mkSort toSort) + Term.compose_prod args (mkSort toSort) ) in let evd,princName_as_constr = @@ -264,11 +274,11 @@ let change_property_sort evd toSort princ princName = (it_mkLambda_or_LetIn init (List.map change_sort_in_predicate princ_info.predicates) ) - princ_info.params + (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.params) let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) - let mutr_nparams = (compute_elim_sig old_princ_type).nparams in + let mutr_nparams = (compute_elim_sig !evd (EConstr.of_constr old_princ_type)).nparams in (* let time1 = System.get_time () in *) let new_principle_type = compute_new_princ_type_from_rel @@ -279,20 +289,21 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let time2 = System.get_time () in *) (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) let new_princ_name = - next_ident_away_in_goal (Id.of_string "___________princ_________") [] + next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof new_princ_name (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd - new_principle_type + (EConstr.of_constr new_principle_type) hook ; (* let _tim1 = System.get_time () in *) - ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConstU funs) mutr_nparams))); + let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in + ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams))); (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) @@ -321,8 +332,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = Label.to_id (con_label (fst f)) in - id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + let id_of_f = Label.to_id (Constant.label (fst f)) in + id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort) in let names = ref [new_princ_name] in let hook = @@ -331,13 +342,17 @@ let generate_functional_principle (evd: Evd.evar_map ref) then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = - 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 - (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value 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' (EConstr.of_constr value)) in + (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let univs = + let poly = Flags.is_universe_polymorphism () in + Evd.const_univ_entry ~poly evd' + in + let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant name @@ -362,12 +377,12 @@ let generate_functional_principle (evd: Evd.evar_map ref) begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () @@ -380,17 +395,17 @@ let generate_functional_principle (evd: Evd.evar_map ref) exception Not_Rec let get_funs_constant mp dp = - let get_funs_constant const e : (Names.constant*int) array = - match kind_of_term ((strip_lam e)) with + let get_funs_constant const e : (Names.Constant.t*int) array = + match Constr.kind ((strip_lam e)) with | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> match na with | Name id -> - let const = make_con mp dp (Label.of_id id) in + let const = Constant.make3 mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly (Pp.str "Anonymous fix") + anomaly (Pp.str "Anonymous fix.") ) na | _ -> [|const,0|] @@ -398,15 +413,16 @@ 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 ()) (Evd.from_env (Global.env ())) - body + (EConstr.of_constr body) in + let body = EConstr.Unsafe.to_constr body in body - | None -> error ( "Cannot define a principle over an axiom ") + | None -> user_err Pp.(str ( "Cannot define a principle over an axiom ")) in let f = find_constant_body const in let l_const = get_funs_constant const f in @@ -421,8 +437,8 @@ let get_funs_constant mp dp = let first_params = List.hd l_params in List.iter (fun params -> - if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params) - then error "Not a mutal recursive block" + if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params) + then user_err Pp.(str "Not a mutal recursive block") ) l_params in @@ -430,21 +446,21 @@ let get_funs_constant mp dp = let _check_bodies = try let extract_info is_first body = - match kind_of_term body with + match Constr.kind body with | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) | _ -> if is_first && Int.equal (List.length l_bodies) 1 then raise Not_Rec - else error "Not a mutal recursive block" + else user_err Pp.(str "Not a mutal recursive block") in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 && - Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2 + Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) - then error "Not a mutal recursive block" + then user_err Pp.(str "Not a mutal recursive block") in List.iter check l_bodies with Not_Rec -> () @@ -454,7 +470,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) : Safe_typing.private_constants definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) 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 @@ -486,12 +502,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con in let _ = evd := sigma in let l_schemes = - List.map (Typing.unsafe_type_of env sigma) schemes + List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes in let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x) + Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x ) fas in @@ -514,12 +530,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () @@ -555,7 +571,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; - observe (Printer.pr_lconstr scheme_type); + observe (Printer.pr_lconstr_env env sigma scheme_type); let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in @@ -565,10 +581,10 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con let t = (strip_prod_assum t) in let applied_g = List.hd (List.rev (snd (decompose_app t))) in let g = fst (decompose_app applied_g) in - if eq_constr f g + if Constr.equal f g then raise (Found_type j); - observe (Printer.pr_lconstr f ++ str " <> " ++ - Printer.pr_lconstr g) + observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ + Printer.pr_lconstr_env env sigma g) ) ta; @@ -609,19 +625,22 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - errorlabstrm "FunInd.build_scheme" + user_err ~hdr:"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',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in - (destConst f,sort) + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in + if isConst f + then (destConst f,sort) + else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") ) fas ) in let bodies_types = make_scheme evd pconstants in + List.iter2 (fun (princ_id,_,_) def_entry -> ignore @@ -641,12 +660,12 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> - errorlabstrm "FunInd.build_case_scheme" + user_err ~hdr:"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 funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in @@ -659,15 +678,13 @@ let build_case_scheme fa = let ind = first_fun_kn,funs_indexes in (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (scheme, sigma, _) = + let (sigma, scheme) = Indrec.build_case_analysis_scheme_default env sigma ind sf in - let sigma = Sigma.to_evar_map sigma in - let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in + let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) + Universes.new_sort_in_family x ) fa in -- cgit v1.2.3