From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- engine/eConstr.ml | 35 ++++++++++++++++--------- engine/eConstr.mli | 33 +++++++++++++++++------- engine/termops.ml | 14 ++++++---- engine/termops.mli | 4 +-- plugins/cc/cctac.ml | 6 ++++- plugins/firstorder/formula.ml | 6 ++++- plugins/funind/functional_principles_types.ml | 3 ++- plugins/funind/glob_term_to_relation.ml | 5 ++-- plugins/funind/indfun.ml | 11 +++++--- plugins/funind/invfun.ml | 5 ++-- plugins/funind/merge.ml | 7 ++--- plugins/funind/recdef.ml | 5 ++-- plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/taccoerce.ml | 2 +- plugins/quote/quote.ml | 5 ++-- pretyping/cases.ml | 5 ++-- pretyping/classops.ml | 9 ++++--- pretyping/classops.mli | 2 +- pretyping/detyping.ml | 2 ++ pretyping/evarconv.ml | 4 +-- pretyping/inductiveops.ml | 4 ++- pretyping/inductiveops.mli | 10 ++++---- pretyping/reductionops.ml | 17 +++++++----- pretyping/reductionops.mli | 2 +- pretyping/retyping.ml | 30 ++++++++++++---------- pretyping/tacred.ml | 37 +++++++++++++++------------ pretyping/tacred.mli | 6 ++--- pretyping/typeclasses.ml | 1 + pretyping/typeclasses.mli | 4 +-- pretyping/typing.ml | 33 ++++++++++++++---------- pretyping/unification.ml | 1 + proofs/logic.ml | 3 ++- proofs/tacmach.mli | 6 ++--- tactics/eauto.ml | 5 ++-- tactics/equality.ml | 9 ++++--- tactics/hipattern.ml | 17 ++++++------ tactics/hipattern.mli | 8 +++--- tactics/tacticals.ml | 11 +++++--- tactics/tacticals.mli | 6 ++--- tactics/tactics.ml | 22 +++++++++------- vernac/auto_ind_decl.ml | 20 ++++++++------- vernac/classes.ml | 5 ++-- 42 files changed, 257 insertions(+), 165 deletions(-) diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 166340b41..28e9ffdb2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -23,12 +23,21 @@ val make : Sorts.t -> t val kind : Evd.evar_map -> t -> Sorts.t val unsafe_to_sorts : t -> Sorts.t end +module EInstance : +sig +type t +val make : Univ.Instance.t -> t +val kind : Evd.evar_map -> t -> Univ.Instance.t +val empty : t +val is_empty : t -> bool +val unsafe_to_instance : t -> Univ.Instance.t +end type t -val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type val whd_evar : Evd.evar_map -> t -> t -val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t val of_constr : Constr.t -> t val to_constr : evar_map -> t -> Constr.t val unsafe_to_constr : t -> Constr.t @@ -50,6 +59,16 @@ struct let unsafe_to_sorts s = s end +module EInstance = +struct + type t = Univ.Instance.t + let make i = i + let kind sigma i = Evd.normalize_universe_instance sigma i + let empty = Univ.Instance.empty + let is_empty = Univ.Instance.is_empty + let unsafe_to_instance t = t +end + type t = Constr.t let safe_evar_value sigma ev = @@ -63,15 +82,6 @@ let rec whd_evar sigma c = | Some c -> whd_evar sigma c | None -> c end - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') | App (f, args) when isEvar f -> (** Enforce smart constructor invariant on applications *) let ev = destEvar f in @@ -137,7 +147,7 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt type named_context = (constr, types) Context.Named.pt type rel_context = (constr, types) Context.Rel.pt -let in_punivs a = (a, Univ.Instance.empty) +let in_punivs a = (a, EInstance.empty) let mkProp = of_kind (Sort (ESorts.make Sorts.prop)) let mkSet = of_kind (Sort (ESorts.make Sorts.set)) @@ -762,6 +772,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference = module Unsafe = struct let to_sorts = ESorts.unsafe_to_sorts +let to_instance = EInstance.unsafe_to_instance let to_constr = unsafe_to_constr let to_rel_decl = unsafe_to_rel_decl let to_named_decl = unsafe_to_named_decl diff --git a/engine/eConstr.mli b/engine/eConstr.mli index db10fbf42..3a9469e55 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -45,9 +45,21 @@ sig end +module EInstance : +sig + type t + (** Type of universe instances up-to universe unification. Similar to + {ESorts.t} for {Univ.Instance.t}. *) + + val make : Univ.Instance.t -> t + val kind : Evd.evar_map -> t -> Univ.Instance.t + val empty : t + val is_empty : t -> bool +end + (** {5 Destructors} *) -val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) @@ -60,7 +72,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) -val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t (** Construct a term from a view. *) val of_constr : Constr.t -> t @@ -89,13 +101,13 @@ val mkLambda : Name.t * t * t -> t val mkLetIn : Name.t * t * t * t -> t val mkApp : t * t array -> t val mkConst : constant -> t -val mkConstU : pconstant -> t +val mkConstU : constant * EInstance.t -> t val mkProj : (projection * t) -> t val mkInd : inductive -> t -val mkIndU : pinductive -> t +val mkIndU : inductive * EInstance.t -> t val mkConstruct : constructor -> t -val mkConstructU : pconstructor -> t -val mkConstructUi : pinductive * int -> t +val mkConstructU : constructor * EInstance.t -> t +val mkConstructUi : (inductive * EInstance.t) * int -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t @@ -146,10 +158,10 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types val destLambda : Evd.evar_map -> t -> Name.t * types * t val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t val destApp : Evd.evar_map -> t -> t * t array -val destConst : Evd.evar_map -> t -> constant puniverses +val destConst : Evd.evar_map -> t -> constant * EInstance.t val destEvar : Evd.evar_map -> t -> t pexistential -val destInd : Evd.evar_map -> t -> inductive puniverses -val destConstruct : Evd.evar_map -> t -> constructor puniverses +val destInd : Evd.evar_map -> t -> inductive * EInstance.t +val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t val destCase : Evd.evar_map -> t -> case_info * t * t * t array val destProj : Evd.evar_map -> t -> projection * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint @@ -262,6 +274,9 @@ sig val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) + val to_instance : EInstance.t -> Univ.Instance.t + (** Physical identity. Does not care for normalization. *) + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end diff --git a/engine/termops.ml b/engine/termops.ml index a67916345..64f4c6dc5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1150,7 +1150,7 @@ let global_of_constr sigma c = | Const (c, u) -> ConstRef c, u | Ind (i, u) -> IndRef i, u | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Univ.Instance.empty + | Var id -> VarRef id, EConstr.EInstance.empty | _ -> raise Not_found let is_global sigma c t = @@ -1169,8 +1169,12 @@ let isGlobalRef sigma c = let is_template_polymorphic env sigma f = match EConstr.kind sigma f with - | Ind ind -> Environ.template_polymorphic_pind ind env - | Const c -> Environ.template_polymorphic_pconstant c env + | Ind (ind, u) -> + if not (EConstr.EInstance.is_empty u) then false + else Environ.template_polymorphic_ind ind env + | Const (cst, u) -> + if not (EConstr.EInstance.is_empty u) then false + else Environ.template_polymorphic_constant cst env | _ -> false let base_sort_cmp pb s0 s1 = @@ -1453,8 +1457,8 @@ let global_app_of_constr sigma c = | Const (c, u) -> (ConstRef c, u), None | Ind (i, u) -> (IndRef i, u), None | Construct (c, u) -> (ConstructRef c, u), None - | Var id -> (VarRef id, Instance.empty), None - | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c + | Var id -> (VarRef id, EConstr.EInstance.empty), None + | Proj (p, c) -> (ConstRef (Projection.constant p), EConstr.EInstance.empty), Some c | _ -> raise Not_found let prod_applist sigma c l = diff --git a/engine/termops.mli b/engine/termops.mli index 0dd5d96fb..fe6dfb0ce 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -250,7 +250,7 @@ val clear_named_body : Id.t -> env -> env val global_vars : env -> Evd.evar_map -> constr -> Id.t list val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option +val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -259,7 +259,7 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses +val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c9c904e35..2d9dec095 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -66,6 +66,7 @@ let rec decompose_term env sigma t= decompose_term env sigma b) | Construct c -> let (((mind,i_ind),i_con),u)= c in + let u = EInstance.kind sigma u in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in @@ -75,9 +76,11 @@ let rec decompose_term env sigma t= ci_nhyps=nargs-oib.mind_nparams} | Ind c -> let (mind,i_ind),u = c in + let u = EInstance.kind sigma u in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> + let u = EInstance.kind sigma u in let canon_const = constant_of_kn (canonical_con c) in (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> @@ -408,7 +411,8 @@ let build_term_to_complete uf meta pac = let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in let dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in - applist (mkConstructU cinfo.ci_constr, all_args) + let (kn, u) = cinfo.ci_constr in + applist (mkConstructU (kn, EInstance.make u), all_args) let cc_tactic depth additionnal_terms = Proofview.Goal.enter { enter = begin fun gl -> diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 87bac2fe3..7773f6a2f 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -91,6 +91,7 @@ let kind_of_formula gl term = Some (i,l,n)-> let l = List.map EConstr.Unsafe.to_constr l in let ind,u=EConstr.destInd (project gl) i in + let u = EConstr.EInstance.kind (project gl) u in let (mib,mip) = Global.lookup_inductive ind in let nconstr=Array.length mip.mind_consnames in if Int.equal nconstr 0 then @@ -112,7 +113,10 @@ let kind_of_formula gl term = Or((ind,u),l,is_trivial) | _ -> match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with - Some (i,l)-> Exists((EConstr.destInd (project gl) i),List.map EConstr.Unsafe.to_constr l) + Some (i,l)-> + let (ind, u) = EConstr.destInd (project gl) i in + let u = EConstr.EInstance.kind (project gl) u in + Exists((ind, u), List.map EConstr.Unsafe.to_constr l) |_-> Atom (normalize cciterm) type atoms = {positive:constr list;negative:constr list} diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e845db3bc..529b91c4c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -300,7 +300,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin hook ; (* let _tim1 = System.get_time () in *) - ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map EConstr.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 *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 63bd3848f..8aab3b742 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1275,8 +1275,9 @@ let do_build_inductive let open Context.Named.Declaration in let evd,env = Array.fold_right2 - (fun id c (evd,env) -> - let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in + (fun id (c, u) (evd,env) -> + let u = EConstr.EInstance.make u in + let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a7489fb7b..2852152e1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -249,7 +249,8 @@ let derive_inversion fix_names = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in let c = EConstr.of_constr c in - evd, destConst evd c::l + let (cst, u) = destConst evd c in + evd, (cst, EInstance.kind evd u) :: l ) fix_names (evd',[]) @@ -412,7 +413,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in let c = EConstr.of_constr c in - evd,((destConst evd c)::l) + let (cst, u) = destConst evd c in + let u = EInstance.kind evd u in + evd,((cst, u) :: l) ) (Evd.from_env (Global.env ()),[]) fixpoint_exprl @@ -427,7 +430,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in let c = EConstr.of_constr c in - evd,((destConst evd c)::l) + let (cst, u) = destConst evd c in + let u = EInstance.kind evd u in + evd,((cst, u) :: l) ) (Evd.from_env (Global.env ()),[]) fixpoint_exprl diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2c2cd919b..94ec0a898 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -783,7 +783,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( assert (funs <> []); assert (graphs <> []); let funs = Array.of_list funs and graphs = Array.of_list graphs in - let funs_constr = Array.map mkConstU funs in + let map (c, u) = mkConstU (c, EInstance.make u) in + let funs_constr = Array.map map funs in States.with_state_protection_on_exception (fun () -> let env = Global.env () in @@ -882,7 +883,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( (Indrec.build_mutual_induction_scheme (Global.env ()) !evd (Array.to_list (Array.mapi - (fun i _ -> ((kn,i),u(* Univ.Instance.empty *)),true,InType) + (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType) mib.Declarations.mind_packets ) ) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 44aacaf45..c0298d06c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -136,13 +136,14 @@ let prNamedRLDecl s lc = let showind (id:Id.t) = let cstrid = Constrintern.global_reference id in - let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in - let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in + let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in + let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in + let u = EConstr.Unsafe.to_instance u in List.iter (fun decl -> print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); prconstr (RelDecl.get_type decl); print_string "\n") ib1.mind_arity_ctxt; - Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); + Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u)); Array.iteri (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) ib1.mind_user_lc diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0a288c76e..5460d6fb7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -86,9 +86,10 @@ let def_of_const t = let type_of_const sigma t = match (EConstr.kind sigma t) with - | Const sp -> + | Const (sp, u) -> + let u = EInstance.kind sigma u in (* FIXME discarding universe constraints *) - Typeops.type_of_constant_in (Global.env()) sp + Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false let constr_of_global x = diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 55108631b..b34afd51b 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1073,7 +1073,7 @@ let decompose l c = Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let to_ind c = - if isInd sigma c then Univ.out_punivs (destInd sigma c) + if isInd sigma c then fst (destInd sigma c) else error "not an inductive type" in let l = List.map to_ind l in diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 95620b374..b76009c99 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -255,7 +255,7 @@ let coerce_to_evaluable_ref env sigma v = | IndRef _ | ConstructRef _ -> fail () else match Value.to_constr v with - | Some c when isConst sigma c -> EvalConstRef (Univ.out_punivs (destConst sigma c)) + | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c)) | Some c when isVar sigma c -> EvalVarRef (destVar sigma c) | _ -> fail () in if Tacred.is_evaluable env ev then ev else fail () diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 23069a9ab..fc9d70ae7 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -225,8 +225,9 @@ let compute_rhs env sigma bodyi index_of_f = let compute_ivs f cs gl = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let cst = try destConst sigma f with DestKO -> i_can't_do_that () in - let body = Environ.constant_value_in (Global.env()) cst in + let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in + let u = EInstance.kind sigma u in + let body = Environ.constant_value_in (Global.env()) (cst, u) in let body = EConstr.of_constr body in match decomp_term sigma body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 38c105666..c5cf74ccf 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -279,6 +279,7 @@ let rec find_row_ind = function let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in let arsign = inductive_alldecls_env env indu in + let indu = on_snd EInstance.make indu in let hole_source i = match tmloc with | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in @@ -1314,7 +1315,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let cur_alias = lift const_info.cs_nargs current in let ind = mkApp ( - applist (mkIndU (inductive_of_constructor (fst const_info.cs_cstr), snd const_info.cs_cstr), + applist (mkIndU (inductive_of_constructor (fst const_info.cs_cstr), EInstance.make (snd const_info.cs_cstr)), List.map (EConstr.of_constr %> lift const_info.cs_nargs) const_info.cs_params), Array.map EConstr.of_constr const_info.cs_concl_realargs) in Alias (initial,(aliasname,cur_alias,(ci,ind))) in @@ -2104,7 +2105,7 @@ let constr_of_pat env evdref arsign pat avoid = let args = List.rev args in let patargs = List.rev patargs in let pat' = PatCstr (l, cstr, patargs, alias) in - let cstr = mkConstructU ci.cs_cstr in + let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in let apptype = Retyping.get_type_of env ( !evdref) app in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 13310c44d..632ba0d9c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -193,15 +193,16 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) let find_class_type sigma t = + let open EConstr in let t', args = Reductionops.whd_betaiotazeta_stack sigma t in match EConstr.kind sigma t' with - | Var id -> CL_SECVAR id, Univ.Instance.empty, args + | Var id -> CL_SECVAR id, EInstance.empty, args | Const (sp,u) -> CL_CONST sp, u, args | Proj (p, c) when not (Projection.unfolded p) -> - CL_PROJ (Projection.constant p), Univ.Instance.empty, (c :: args) + CL_PROJ (Projection.constant p), EInstance.empty, (c :: args) | Ind (ind_sp,u) -> CL_IND ind_sp, u, args - | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] - | Sort _ -> CL_SORT, Univ.Instance.empty, [] + | Prod (_,_,_) -> CL_FUN, EInstance.empty, [] + | Sort _ -> CL_SORT, EInstance.empty, [] | _ -> raise Not_found diff --git a/pretyping/classops.mli b/pretyping/classops.mli index a1d030f12..0d741a5a5 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -60,7 +60,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list +val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 84022f57f..e4d7ab38d 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -438,6 +438,7 @@ let detype_level sigma l = GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) let detype_instance sigma l = + let l = EInstance.kind sigma l in if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) @@ -507,6 +508,7 @@ let rec detype flags avoid env sigma t = let ty = Retyping.get_type_of (snd env) sigma c in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let body' = strip_lam_assum body in + let u = EInstance.kind sigma u in let body' = CVars.subst_instance_constr u body' in let body' = EConstr.of_constr body' in substl (c :: List.rev args) body' diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b6fa25769..9c9350ab1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -51,9 +51,9 @@ let unfold_projection env evd ts p c = let eval_flexible_term ts env evd c = match EConstr.kind evd c with - | Const (c,u as cu) -> + | Const (c, u) -> if is_transparent_constant ts c - then Option.map EConstr.of_constr (constant_opt_value_in env cu) + then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) else None | Rel n -> (try match lookup_rel n env with diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 88c492f03..5b42add28 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -74,6 +74,7 @@ let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n) let mkAppliedInd (IndType ((ind,params), realargs)) = let open EConstr in + let ind = on_snd EInstance.make ind in applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs) (* Does not consider imbricated or mutually recursive types *) @@ -471,11 +472,12 @@ let find_rectype env sigma c = let open EConstr in let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with - | Ind (ind,u as indu) -> + | Ind (ind,u) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in if mib.mind_nparams > List.length l then raise Not_found; let l = List.map EConstr.Unsafe.to_constr l in let (par,rargs) = List.chop mib.mind_nparams l in + let indu = (ind, EInstance.kind sigma u) in IndType((indu, par),List.map EConstr.of_constr rargs) | _ -> raise Not_found diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index ab470a540..bdb6f996b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -161,12 +161,12 @@ val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list -val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list -val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array +val extract_mrectype : evar_map -> EConstr.t -> (inductive * EConstr.EInstance.t) * EConstr.constr list +val find_mrectype : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr array val find_rectype : env -> evar_map -> EConstr.types -> inductive_type -val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list -val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list +val find_inductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list +val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list (********************) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8be3b8328..270320538 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -550,7 +550,7 @@ struct let constr_of_cst_member f sk = match f with - | Cst_const (c, u) -> mkConstU (c,u), sk + | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk | Cst_proj p -> match decomp sk with | Some (hd, sk) -> mkProj (p, hd), sk @@ -703,7 +703,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function csts Univ.LMap.empty in let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - mkConstU (cst,inst) + mkConstU (cst, EInstance.make inst) | None -> bd end with @@ -856,7 +856,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some body -> whrec cst_l (EConstr.of_constr body, stack) | None -> fold ()) | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> - (match constant_opt_value_in env const with + let u' = EInstance.kind sigma u in + (match constant_opt_value_in env (fst const, u') with | None -> fold () | Some body -> let body = EConstr.of_constr body in @@ -895,7 +896,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | None -> fold () | Some (bef,arg,s') -> whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s') + (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') ) | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in @@ -998,6 +999,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (match constant_opt_value_in env const with | None -> fold () | Some body -> + let const = (fst const, EInstance.make (snd const)) in let body = EConstr.of_constr body in whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) @@ -1657,12 +1659,13 @@ let meta_reducible_instance evd b = let head_unfold_under_prod ts env sigma c = - let unfold (cst,u as cstu) = + let unfold (cst,u) = + let cstu = (cst, EInstance.kind sigma u) in if Cpred.mem cst (snd ts) then match constant_opt_value_in env cstu with | Some c -> EConstr.of_constr c - | None -> mkConstU cstu - else mkConstU cstu in + | None -> mkConstU (cst, u) + else mkConstU (cst, u) in let rec aux c = match EConstr.kind sigma c with | Prod (n,t,c) -> mkProd (n,aux t, aux c) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 01707b47a..752c30a8a 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -232,7 +232,7 @@ type 'a miota_args = { val reducible_mind_case : evar_map -> constr -> bool val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, Univ.Instance.t) kind_of_term +val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 9c9751af8..496c706ec 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -102,10 +102,10 @@ let retype ?(polyprop=true) sigma = let ty = RelDecl.get_type (lookup_rel n env) in lift n ty | Var id -> type_of_var env id - | Const cst -> EConstr.of_constr (rename_type_of_constant env cst) + | Const (cst, u) -> EConstr.of_constr (rename_type_of_constant env (cst, EInstance.kind sigma u)) | Evar ev -> existential_type sigma ev - | Ind ind -> EConstr.of_constr (rename_type_of_inductive env ind) - | Construct cstr -> EConstr.of_constr (rename_type_of_constructor env cstr) + | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u)) + | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u)) | Case (_,p,c,lf) -> let Inductiveops.IndType(indf,realargs) = let t = type_of env c in @@ -186,16 +186,20 @@ let retype ?(polyprop=true) sigma = let argtyps = Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in match EConstr.kind sigma c with - | Ind ind -> - let mip = lookup_mind_specif env (fst ind) in + | Ind (ind, u) -> + let u = EInstance.kind sigma u in + let mip = lookup_mind_specif env ind in EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters - ~polyprop env (mip,snd ind) argtyps + ~polyprop env (mip, u) argtyps with Reduction.NotArity -> retype_error NotAnArity) - | Const cst -> - EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps + | Const (cst, u) -> + let u = EInstance.kind sigma u in + EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id - | Construct cstr -> EConstr.of_constr (type_of_constructor env cstr) + | Construct (cstr, u) -> + let u = EInstance.kind sigma u in + EConstr.of_constr (type_of_constructor env (cstr, u)) | _ -> assert false in type_of, sort_of, sort_family_of, @@ -212,13 +216,13 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with | Ind (ind,u) -> let spec = Inductive.lookup_mind_specif env ind in - type_of_inductive_knowing_conclusion env sigma (spec,u) conclty - | Const cst -> - let t = constant_type_in env cst in + type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty + | Const (cst, u) -> + let t = constant_type_in env (cst, EInstance.kind sigma u) in (* TODO *) sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||]) | Var id -> sigma, type_of_var env id - | Construct cstr -> sigma, EConstr.of_constr (type_of_constructor env cstr) + | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false (* Profiling *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ef9f39d77..67221046b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -60,6 +60,7 @@ let is_evaluable env = function let value_of_evaluable_ref env evref u = match evref with | EvalConstRef con -> + let u = Unsafe.to_instance u in EConstr.of_constr (try constant_value_in env (con,u) with NotEvaluableConst IsProj -> raise (Invalid_argument "value_of_evaluable_ref")) @@ -103,9 +104,9 @@ let isEvalRef env sigma c = match EConstr.kind sigma c with let destEvalRefU sigma c = match EConstr.kind sigma c with | Const (cst,u) -> EvalConst cst, u - | Var id -> (EvalVar id, Univ.Instance.empty) - | Rel n -> (EvalRel n, Univ.Instance.empty) - | Evar ev -> (EvalEvar ev, Univ.Instance.empty) + | Var id -> (EvalVar id, EInstance.empty) + | Rel n -> (EvalRel n, EInstance.empty) + | Evar ev -> (EvalEvar ev, EInstance.empty) | _ -> anomaly (Pp.str "Not an unfoldable reference") let unsafe_reference_opt_value env sigma eval = @@ -125,7 +126,9 @@ let unsafe_reference_opt_value env sigma eval = let reference_opt_value env sigma eval u = match eval with - | EvalConst cst -> Option.map EConstr.of_constr (constant_opt_value_in env (cst,u)) + | EvalConst cst -> + let u = EInstance.kind sigma u in + Option.map EConstr.of_constr (constant_opt_value_in env (cst,u)) | EvalVar id -> env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> @@ -519,13 +522,13 @@ let reduce_mind_case_use_function func env sigma mia = mutual inductive, try to reuse the global name if the block was indeed initially built as a global definition *) - let kn = map_puniverses (fun x -> con_with_label x (Label.of_id id)) - (destConst sigma func) - in - try match constant_opt_value_in env kn with + let (kn, u) = destConst sigma func in + let kn = con_with_label kn (Label.of_id id) in + let cst = (kn, EInstance.kind sigma u) in + try match constant_opt_value_in env cst with | None -> None (* TODO: check kn is correct *) - | Some _ -> Some (minargs,mkConstU kn) + | Some _ -> Some (minargs,mkConstU (kn, u)) with Not_found -> None else fun _ -> None in @@ -539,14 +542,15 @@ let match_eval_ref env sigma constr = match EConstr.kind sigma constr with | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> Some (EvalConst sp, u) - | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, Univ.Instance.empty) - | Rel i -> Some (EvalRel i, Univ.Instance.empty) - | Evar ev -> Some (EvalEvar ev, Univ.Instance.empty) + | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty) + | Rel i -> Some (EvalRel i, EInstance.empty) + | Evar ev -> Some (EvalEvar ev, EInstance.empty) | _ -> None let match_eval_ref_value env sigma constr = match EConstr.kind sigma constr with | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> + let u = EInstance.kind sigma u in Some (EConstr.of_constr (constant_value_in env (sp, u))) | Var id when is_evaluable env (EvalVarRef id) -> env |> lookup_named id |> NamedDecl.get_value @@ -628,8 +632,9 @@ let whd_nothing_for_iota env sigma s = | Meta ev -> (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack) with Not_found -> s) - | Const const when is_transparent_constant full_transparent_state (fst const) -> - (match constant_opt_value_in env const with + | Const (const, u) when is_transparent_constant full_transparent_state const -> + let u = EInstance.kind sigma u in + (match constant_opt_value_in env (const, u) with | Some body -> whrec (EConstr.of_constr body, stack) | None -> s) | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack @@ -955,7 +960,7 @@ let simpl env sigma c = strong whd_simpl env sigma c let matches_head env sigma c t = match EConstr.kind sigma t with | App (f,_) -> Constr_matching.matches env sigma c f - | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, Univ.Instance.empty)) + | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, EInstance.empty)) | _ -> raise Constr_matching.PatternMatchingFailure (** FIXME: Specific function to handle projections: it ignores what happens on the @@ -1039,7 +1044,7 @@ let contextually byhead occs f env sigma t = let match_constr_evaluable_ref sigma c evref = match EConstr.kind sigma c, evref with | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u - | Var id, EvalVarRef id' when id_eq id id' -> Some Univ.Instance.empty + | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty | _, _ -> None let substlin env sigma evalref n (nowhere_except_in,locs) c = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index a4499015d..76d0bc241 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -76,12 +76,12 @@ val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) -val reduce_to_atomic_ind : env -> evar_map -> types -> pinductive * types +val reduce_to_atomic_ind : env -> evar_map -> types -> (inductive * EInstance.t) * types (** [reduce_to_quantified_ind env sigma t] puts [t] in the form [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) -val reduce_to_quantified_ind : env -> evar_map -> types -> pinductive * types +val reduce_to_quantified_ind : env -> evar_map -> types -> (inductive * EInstance.t) * types (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) @@ -92,7 +92,7 @@ val reduce_to_atomic_ref : env -> evar_map -> global_reference -> types -> types val find_hnf_rectype : - env -> evar_map -> types -> pinductive * constr list + env -> evar_map -> types -> (inductive * EInstance.t) * constr list val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 478499d91..93c71e6ea 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -303,6 +303,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = | Some (Forward, info) -> let proj = Option.get proj in let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in + let u = EConstr.EInstance.kind sigma u in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in if check && check_instance env sigma (EConstr.of_constr body) then None else diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 7990b12cd..8d1c0b94c 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -61,13 +61,13 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c (** These raise a UserError if not a class. Caution: the typeclass structures is not instantiated w.r.t. the universe instance. This is done separately by typeclass_univ_instance. *) -val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * constr list +val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option +val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option val instance_impl : instance -> global_reference diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d9d64e7eb..c2a030bcd 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -35,11 +35,13 @@ let meta_type evd mv = let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty -let constant_type_knowing_parameters env sigma cst jl = +let constant_type_knowing_parameters env sigma (cst, u) jl = + let u = Unsafe.to_instance u in let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in - EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp) + EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp) let inductive_type_knowing_parameters env sigma (ind,u) jl = + let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp) @@ -140,9 +142,10 @@ let e_type_case_branches env evdref (ind,largs) pj c = (lc, ty) let e_judge_of_case env evdref ci pj cj lfj = - let indspec = + let ((ind, u), spec) = try find_mrectype env !evdref cj.uj_type with Not_found -> error_case_not_inductive env !evdref cj in + let indspec = ((ind, EInstance.kind !evdref u), spec) in let _ = check_case_info env (fst indspec) ci in let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in e_check_branch_types env evdref (fst indspec) cj (lfj,bty); @@ -224,6 +227,7 @@ let judge_of_projection env sigma p cj = try find_mrectype env sigma cj.uj_type with Not_found -> error_case_not_inductive env sigma cj in + let u = EInstance.kind sigma u in let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in let ty = substl (cj.uj_val :: List.rev args) ty in {uj_val = EConstr.mkProj (p,cj.uj_val); @@ -262,14 +266,17 @@ let rec execute env evdref cstr = | Var id -> judge_of_variable env id - | Const c -> - make_judge cstr (EConstr.of_constr (rename_type_of_constant env c)) + | Const (c, u) -> + let u = EInstance.kind !evdref u in + make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) - | Ind ind -> - make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind)) + | Ind (ind, u) -> + let u = EInstance.kind !evdref u in + make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) - | Construct cstruct -> - make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct)) + | Construct (cstruct, u) -> + let u = EInstance.kind !evdref u in + make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) | Case (ci,p,c,lf) -> let cj = execute env evdref c in @@ -305,14 +312,14 @@ let rec execute env evdref cstr = let jl = execute_array env evdref args in let j = match EConstr.kind !evdref f with - | Ind ind when Environ.template_polymorphic_pind ind env -> + | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> (* Sort-polymorphism of inductive types *) make_judge f - (inductive_type_knowing_parameters env !evdref ind jl) - | Const cst when Environ.template_polymorphic_pconstant cst env -> + (inductive_type_knowing_parameters env !evdref (ind, u) jl) + | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env -> (* Sort-polymorphism of inductive types *) make_judge f - (constant_type_knowing_parameters env !evdref cst jl) + (constant_type_knowing_parameters env !evdref (cst, u) jl) | _ -> execute env evdref f in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 035b0c223..91781a076 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -535,6 +535,7 @@ let key_of env sigma b flags f = | Const (cst, u) when is_transparent env (ConstKey cst) && (Cpred.mem cst (snd flags.modulo_delta) || Environ.is_projection cst env) -> + let u = EInstance.kind sigma u in Some (IsKey (ConstKey (cst, u))) | Var id when is_transparent env (VarKey id) && Id.Pred.mem id (fst flags.modulo_delta) -> diff --git a/proofs/logic.ml b/proofs/logic.ml index b38a901c2..e6024785d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -505,9 +505,10 @@ and mk_casegoals sigma goal goalacc p c = let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in let ct = EConstr.of_constr ct in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in - let indspec = + let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals") in + let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 1b05bc7d6..627a8e0e7 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -68,8 +68,8 @@ val pf_whd_all : goal sigma -> constr -> constr val pf_hnf_constr : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types +val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types +val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr @@ -131,7 +131,7 @@ module New : sig val pf_last_hyp : ('a, 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types diff --git a/tactics/eauto.ml b/tactics/eauto.ml index e0dff3739..8d1e0e507 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -472,8 +472,9 @@ let unfold_head env sigma (ids, csts) c = (match Environ.named_body id env with | Some b -> true, EConstr.of_constr b | None -> false, c) - | Const (cst,u as c) when Cset.mem cst csts -> - true, EConstr.of_constr (Environ.constant_value_in env c) + | Const (cst, u) when Cset.mem cst csts -> + let u = EInstance.kind sigma u in + true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) | App (f, args) -> (match aux f with | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) diff --git a/tactics/equality.ml b/tactics/equality.ml index 53b468bff..7ae7446c8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -746,6 +746,7 @@ let find_positions env sigma t1 t2 = let _,rargs2 = List.chop nparams args2 in let (mib,mip) = lookup_mind_specif env ind1 in let params1 = List.map EConstr.Unsafe.to_constr params1 in + let u1 = EInstance.kind sigma u1 in let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in List.flatten @@ -1324,19 +1325,19 @@ let inject_if_homogenous_dependent_pair ty = hd2,ar2 = decompose_app_vect sigma t2 in if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit; if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit; - let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in + let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in (* check if the user has declared the dec principle *) (* and compare the fst arguments of the dep pair *) (* Note: should work even if not an inductive type, but the table only *) (* knows inductive types *) - if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && + if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let inj2 = EConstr.of_constr inj2 in - let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in + let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) tclTHENLIST [Proofview.tclEFFECTS eff; @@ -1783,6 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in + let u = EInstance.kind sigma u in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with @@ -1834,6 +1836,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let test (_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let u = EInstance.kind sigma u in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; (* J.F.: added to prevent failure on goal containing x=x as an hyp *) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 8e4654c02..851554b83 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -144,6 +144,7 @@ let match_with_tuple sigma t = let t = match_with_one_constructor sigma None false true t in Option.map (fun (hd,l) -> let ind = destInd sigma hd in + let ind = on_snd (fun u -> EInstance.kind sigma u) ind in let (mib,mip) = Global.lookup_pinductive ind in let isrec = mis_is_recursive (fst ind,mib,mip) in (hd,l,isrec)) t @@ -200,8 +201,8 @@ let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t = let match_with_empty_type sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with - | Ind ind -> - let (mib,mip) = Global.lookup_pinductive ind in + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 0 then Some hdapp else None | _ -> None @@ -214,8 +215,8 @@ let is_empty_type sigma t = op2bool (match_with_empty_type sigma t) let match_with_unit_or_eq_type sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with - | Ind ind -> - let (mib,mip) = Global.lookup_pinductive ind in + | Ind (ind , _) -> + let (mib,mip) = Global.lookup_inductive ind in let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in @@ -369,8 +370,8 @@ let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) let match_with_nodep_ind sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with - | Ind ind -> - let (mib,mip) = Global.lookup_pinductive ind in + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in if Array.length (mib.mind_packets)>1 then None else let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in if Array.for_all nodep_constr mip.mind_nf_lc then @@ -387,8 +388,8 @@ let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) let match_with_sigma_type sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with - | Ind ind -> - let (mib,mip) = Global.lookup_pinductive ind in + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in if Int.equal (Array.length (mib.mind_packets)) 1 && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) && diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index c46817f50..dd09c3a4d 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -122,19 +122,19 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr -> - coq_eq_data * Univ.universe_instance * (types * constr * constr) + coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr -> - coq_eq_data * Univ.universe_instance * (types * constr * constr) + coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) -val find_eq_data : evar_map -> constr -> coq_eq_data * Univ.universe_instance * equation_kind +val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_kind (** Match a term of the form [(existT A P t p)] Returns associated lemmas and [A,P,t,p] *) val find_sigma_data_decompose : evar_map -> constr -> - coq_sigma_data * (Univ.universe_instance * constr * constr * constr * constr) + coq_sigma_data * (EInstance.t * constr * constr * constr * constr) (** Match a term of the form [{x:A|P}], returns [A] and [P] *) val match_sigma : evar_map -> constr -> constr * constr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index a1cd51047..90b7d6581 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -606,6 +606,7 @@ module New = struct isrec allnames tac predicate ind (c, t) = Proofview.Goal.enter { enter = begin fun gl -> let sigma, elim = (mk_elim ind).enter gl in + let ind = on_snd (fun u -> EInstance.kind sigma u) ind in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Proofview.Goal.enter { enter = begin fun gl -> let indclause = mk_clenv_from gl (c, t) in @@ -680,17 +681,19 @@ module New = struct (sigma, EConstr.of_constr c) end } - let gl_make_case_dep ind = { enter = begin fun gl -> + let gl_make_case_dep (ind, u) = { enter = begin fun gl -> let sigma = Sigma.Unsafe.of_evar_map (project gl) in - let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true + let u = EInstance.kind (project gl) u in + let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true (elimination_sort_of_goal gl) in (Sigma.to_evar_map sigma, EConstr.of_constr r) end } - let gl_make_case_nodep ind = { enter = begin fun gl -> + let gl_make_case_nodep (ind, u) = { enter = begin fun gl -> let sigma = Sigma.Unsafe.of_evar_map (project gl) in - let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false + let u = EInstance.kind (project gl) u in + let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false (elimination_sort_of_goal gl) in (Sigma.to_evar_map sigma, EConstr.of_constr r) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 5839666a7..3b90ec514 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -124,7 +124,7 @@ val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr -val compute_constructor_signatures : rec_flag -> pinductive -> bool list array +val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array (** Useful for [as intro_pattern] modifier *) val compute_induction_names : @@ -256,11 +256,11 @@ module New : sig val case_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> constr * types -> unit Proofview.tactic + constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic val case_nodep_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> constr * types -> unit Proofview.tactic + constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 55d6df659..8306ac174 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1445,6 +1445,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in + let mind = on_snd (fun u -> EInstance.kind (Sigma.to_evar_map sigma) u) mind in let Sigma (elim, sigma, p) = if occur_term (Sigma.to_evar_map sigma) c concl then build_case_analysis_scheme env sigma mind true sort @@ -1647,6 +1648,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let elim = try DefinedRecord (Recordops.lookup_projections ind) with Not_found -> + let u = EInstance.kind sigma u in let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in let elim = EConstr.of_constr elim in @@ -2214,9 +2216,9 @@ let constructor_tac with_evars expctdnumopt i lbind = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; - let Sigma (cons, sigma, p) = Sigma.fresh_constructor_instance + let Sigma ((cons, u), sigma, p) = Sigma.fresh_constructor_instance (Proofview.Goal.env gl) sigma (fst mind, i) in - let cons = mkConstructU cons in + let cons = mkConstructU (cons, EInstance.make u) in let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in let tac = @@ -4033,24 +4035,25 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info = let guess_elim isrec dep s hyp0 gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in - let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in + let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in let evd, elimc = - if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl + if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl else let env = Tacmach.New.pf_env gl in let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in + let u = EInstance.kind (Tacmach.New.project gl) u in if use_dependent_propositions_elimination () && dep then - let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma mind true s in + let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in (Sigma.to_evar_map sigma, ind) else - let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in + let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma (mind, u) s in let ind = EConstr.of_constr ind in (Sigma.to_evar_map sigma, ind) in let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - evd, ((elimc, NoBindings), elimt), mkIndU mind + evd, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in @@ -4637,9 +4640,10 @@ let case_type t = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Tacmach.New.pf_env gl in - let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in + let ((ind, u), t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in + let u = EInstance.kind (Sigma.to_evar_map sigma) u in let s = Tacticals.New.elimination_sort_of_goal gl in - let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma ind s in + let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma (ind, u) s in let elimc = EConstr.of_constr elimc in Sigma (elim_scheme_type elimc t, evd, p) end } diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 10ac7135b..b9c4c6cc5 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -179,9 +179,10 @@ let build_beq_scheme mode kn = *) let compute_A_equality rel_list nlist eqA ndx t = let lifti = ndx in + let sigma = Evd.empty (** FIXME *) in let rec aux c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in - match EConstr.kind Evd.empty (** FIXME *) c with + match EConstr.kind sigma c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants | Var x -> let eid = id_of_string ("eq_"^(string_of_id x)) in @@ -215,9 +216,10 @@ let build_beq_scheme mode kn = | Prod _ -> raise InductiveWithProduct | Lambda _-> raise (EqUnknown "abstraction") | LetIn _ -> raise (EqUnknown "let-in") - | Const kn -> - (match Environ.constant_opt_value_in env kn with - | None -> raise (ParameterWithoutEquality (ConstRef (fst kn))) + | Const (kn, u) -> + let u = EConstr.EInstance.kind sigma u in + (match Environ.constant_opt_value_in env (kn, u) with + | None -> raise (ParameterWithoutEquality (ConstRef kn)) | Some c -> aux (EConstr.applist (EConstr.of_constr c,a))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") @@ -373,7 +375,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = let u,v = destruct_ind sigma type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -445,7 +447,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = else ( let bl_t1, eff = try - let c, eff = find_scheme bl_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in mkConst c, eff with Not_found -> (* spiwack: the format of this error message should probably @@ -485,13 +487,13 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = begin try Proofview.tclUNIT (destApp sigma rgt) with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind2,ca2) -> - begin try Proofview.tclUNIT (out_punivs (destInd sigma ind1)) + begin try Proofview.tclUNIT (fst (destInd sigma ind1)) with DestKO -> begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind1))) with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp1,i1) -> - begin try Proofview.tclUNIT (out_punivs (destInd sigma ind2)) + begin try Proofview.tclUNIT (fst (destInd sigma ind2)) with DestKO -> begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind2))) with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") @@ -664,7 +666,7 @@ let make_bl_scheme mode mind = let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal - (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff diff --git a/vernac/classes.ml b/vernac/classes.ml index 415b98f2d..c3300a361 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -166,8 +166,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum c' in let ctx'' = ctx' @ ctx in - let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in - let cl, u = Typeclasses.typeclass_univ_instance k in + let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in + let u = EConstr.EInstance.kind !evars u in + let cl, u = Typeclasses.typeclass_univ_instance (k, u) in let _, args = List.fold_right (fun decl (args, args') -> match decl with -- cgit v1.2.3