diff options
-rw-r--r-- | kernel/fast_typeops.ml | 284 | ||||
-rw-r--r-- | kernel/fast_typeops.mli | 106 | ||||
-rw-r--r-- | kernel/typeops.mli | 10 | ||||
-rw-r--r-- | plugins/cc/ccalgo.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 8 |
6 files changed, 323 insertions, 89 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index dce4e9307..7d9a2aac0 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -37,19 +37,14 @@ let check_constraints cst env = else error_unsatisfied_constraints env cst (* This should be a type (a priori without intention to be an assumption) *) -let type_judgment env c t = - match kind_of_term(whd_all env t) with - | Sort s -> {utj_val = c; utj_type = s } - | _ -> error_not_type env (make_judge c t) - let check_type env c t = match kind_of_term(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env t ty = +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = try let _ = check_type env t ty in t with TypeError _ -> error_assumption env (make_judge t ty) @@ -62,26 +57,24 @@ let assumption_of_judgment env t ty = (* Prop and Set *) -let judge_of_prop = mkSort type1_sort - -let judge_of_prop_contents _ = judge_of_prop +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = +let type_of_variable env id = try named_type id env with Not_found -> error_unbound_var env id @@ -89,17 +82,24 @@ let judge_of_variable env id = (* Management of context of variables. *) (* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) + variables of the current env. + Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env f c sign = Context.Named.fold_outside - (fun decl () -> - let id = NamedDecl.get_id decl in - let ty1 = NamedDecl.get_type decl in + (fun d1 () -> + let open Context.Named.Declaration in + let id = NamedDecl.get_id d1 in try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> + let d2 = lookup_named id env in + conv env (get_type d2) (get_type d1); + (match d2,d1 with + | LocalAssum _, LocalAssum _ -> () + | LocalAssum _, LocalDef _ -> + (* This is wrong, because we don't know if the body is + needed or not for typechecking: *) () + | LocalDef _, LocalAssum _ -> raise NotConvertible + | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); + with Not_found | NotConvertible | Option.Heterogeneous -> error_reference_variables env id (f c)) sign ~init:() @@ -111,7 +111,7 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant_knowing_parameters_arity env t paramtyps = +let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t | TemplateArity (sign,ar) -> @@ -119,19 +119,28 @@ let type_of_constant_knowing_parameters_arity env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_knowing_parameters_arity env ty paramtyps, cu - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = +let type_of_constant_knowing_parameters env (kn,u as cst) args = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant_knowing_parameters env cst args in + let ty, cu = constant_type env cst in + let ty = type_of_constant_type_knowing_parameters env ty args in let () = check_constraints cu env in ty -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let ty = constant_type_in env cst in + type_of_constant_type_knowing_parameters env ty args + +let type_of_constant env cst = + type_of_constant_knowing_parameters env cst [||] + +let type_of_constant_in env cst = + type_of_constant_knowing_parameters_in env cst [||] + +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -145,7 +154,7 @@ let judge_of_constant env cst = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var ty = +let type_of_abstraction env name var ty = mkProd (name, var, ty) (* Type of an application. *) @@ -153,7 +162,7 @@ let judge_of_abstraction env name var ty = let make_judgev c t = Array.map2 make_judge c t -let judge_of_apply env func funt argsv argstv = +let type_of_apply env func funt argsv argstv = let len = Array.length argsv in let rec apply_rec i typ = if Int.equal i len then typ @@ -207,7 +216,7 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name s1 s2 = +let type_of_product env name s1 s2 = let s = sort_of_product env s1 s2 in mkSort s @@ -220,7 +229,7 @@ let judge_of_product env name s1 s2 = env |- c:typ2 *) -let judge_of_cast env c ct k expected_type = +let check_cast env c ct k expected_type = try match k with | VMcast -> @@ -249,33 +258,34 @@ let judge_of_cast env c ct k expected_type = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = +let type_of_inductive env (ind,u as indu) = let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let _ = +let type_of_constructor env (c,u as cu) = + let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu mib.mind_hyps + in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in let () = check_constraints cst env in - t + t (* Case. *) @@ -287,25 +297,25 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci p pt c ct lf lft = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - let _ = check_case_info env pind ci in + let () = check_case_info env pind ci in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in - rslty + rslty -let judge_of_projection env p c ct = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty (* Fixpoints. *) @@ -313,7 +323,7 @@ let judge_of_projection env p c ct = (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdef vdeft = +let check_fixpoint env lna lar vdef vdeft = let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try @@ -333,23 +343,23 @@ let rec execute env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> let ct = execute env c in - judge_of_projection env p c ct + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> @@ -359,56 +369,56 @@ let rec execute env cstr = | Ind ind when Environ.template_polymorphic_pind ind env -> (* Template sort-polymorphism of inductive types *) let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args + type_of_inductive_knowing_parameters env ind args | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Template sort-polymorphism of constants *) let args = Array.map (fun t -> lazy t) argst in - judge_of_constant_knowing_parameters env cst args + type_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) execute env f in - judge_of_apply env f ft args argst + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (LocalAssum (name,c1)) env in let c2t = execute env1 c2 in - judge_of_abstraction env name c1 c2t + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> let vars = execute_is_type env c1 in let env1 = push_rel (LocalAssum (name,c1)) env in let vars' = execute_is_type env1 c2 in - judge_of_product env name vars vars' + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> let c1t = execute env c1 in let _c2s = execute_is_type env c2 in - let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in + let () = check_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (LocalDef (name,c1,c2)) env in let c3t = execute env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> let ct = execute env c in - let _ts = execute_type env t in - let _ = judge_of_cast env c ct k t in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> let ct = execute env c in let pt = execute env p in let lft = execute_array env lf in - judge_of_case env ci p pt c ct lf lft + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in @@ -431,16 +441,12 @@ and execute_is_type env constr = let t = execute env constr in check_type env constr t -and execute_type env constr = - let t = execute env constr in - type_judgment env constr t - and execute_recdef env (names,lar,vdef) i = let lart = execute_array env lar in - let lara = Array.map2 (assumption_of_judgment env) lar lart in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in let vdeft = execute_array env1 vdef in - let () = type_fixpoint env1 names lara vdef vdeft in + let () = check_fixpoint env1 names lara vdef vdeft in (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) @@ -456,9 +462,133 @@ let infer = Profile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t + +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } + let infer_type env constr = - execute_type env constr + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in make_judgev cv jv + +(* Typing of several terms. *) + +let infer_local_decl env id = function + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) + +let infer_local_decls env decls = + let rec inferec env = function + | (id, d) :: l -> + let (env, l) = inferec env l in + let d = infer_local_decl env id d in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in + inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +let judge_of_case env ci pj cj lfj = + let lf, lft = dest_judgev lfj in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) + (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +let type_of_projection_constant env (p,u) = + let cst = Projection.constant p in + let cb = lookup_constant cst env in + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] l + +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = + let params, ccl = dest_prod_assum env t in + match kind_of_term ccl with + | Sort (Type u) -> + let ind, l = decompose_app (whd_all env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t + | _ -> + RegularArity t diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 41cff607e..73c63db68 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names +open Univ open Term open Environ +open Entries open Declarations (** {6 Typing functions (not yet tagged as safe) } - - They return unsafe judgments that are "in context" of a set of + + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -22,3 +25,102 @@ open Declarations val infer : env -> constr -> unsafe_judgment val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment + +val infer_local_decls : + env -> (Id.t * local_entry) list -> (env * Context.Rel.t) + +(** {6 Basic operations of the typing machine. } *) + +(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j] + returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *) + +val assumption_of_judgment : env -> unsafe_judgment -> types +val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment + +(** {6 Type of sorts. } *) +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment +val judge_of_prop_contents : contents -> unsafe_judgment +val judge_of_type : universe -> unsafe_judgment + +(** {6 Type of a bound variable. } *) +val judge_of_relative : env -> int -> unsafe_judgment + +(** {6 Type of variables } *) +val judge_of_variable : env -> variable -> unsafe_judgment + +(** {6 type of a constant } *) + +val judge_of_constant : env -> pconstant -> unsafe_judgment + +val judge_of_constant_knowing_parameters : + env -> pconstant -> types Lazy.t array -> unsafe_judgment + +(** {6 type of an applied projection } *) + +val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment + +(** {6 Type of application. } *) +val judge_of_apply : + env -> unsafe_judgment -> unsafe_judgment array + -> unsafe_judgment + +(** {6 Type of an abstraction. } *) +val judge_of_abstraction : + env -> Name.t -> unsafe_type_judgment -> unsafe_judgment + -> unsafe_judgment + +val sort_of_product : env -> sorts -> sorts -> sorts + +(** {6 Type of a product. } *) +val judge_of_product : + env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment + -> unsafe_judgment + +(** s Type of a let in. *) +val judge_of_letin : + env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment + -> unsafe_judgment + +(** {6 Type of a cast. } *) +val judge_of_cast : + env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment -> + unsafe_judgment + +(** {6 Inductive types. } *) + +val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment + +(* val judge_of_inductive_knowing_parameters : *) +(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) + +val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment + +(** {6 Type of Cases. } *) +val judge_of_case : env -> case_info + -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array + -> unsafe_judgment + +(* val type_of_constant : env -> pconstant -> types constrained *) + +val type_of_constant_type : env -> constant_type -> types + +val type_of_projection_constant : env -> Names.projection puniverses -> types + +val type_of_constant_in : env -> pconstant -> types + +val type_of_constant_type_knowing_parameters : + env -> constant_type -> types Lazy.t array -> types + +(* val type_of_constant_knowing_parameters : *) +(* env -> pconstant -> types Lazy.t array -> types constrained *) + +val type_of_constant_knowing_parameters_in : + env -> pconstant -> types Lazy.t array -> types + +(** Make a type polymorphic if an arity *) +val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> + constant_type + +(** Check that hyps are included in env and fails with error otherwise *) +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 81fd1427d..cfc82c158 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -102,10 +102,10 @@ val judge_of_case : env -> case_info -> unsafe_judgment (** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit +(* val type_fixpoint : env -> Name.t array -> types array *) +(* -> unsafe_judgment array -> unit *) -val type_of_constant : env -> pconstant -> types constrained +(* val type_of_constant : env -> pconstant -> types constrained *) val type_of_constant_type : env -> constant_type -> types @@ -116,8 +116,8 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained +(* val type_of_constant_knowing_parameters : *) +(* env -> pconstant -> types Lazy.t array -> types constrained *) val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc53b113d..7347c3c2c 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -444,7 +444,7 @@ and applist_projection c l = let p = Projection.make (fst c) false in (match l with | [] -> (* Expand the projection *) - let ty,_ = Typeops.type_of_constant (Global.env ()) c in + let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a980a43f5..33fab74e1 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -258,7 +258,7 @@ let rec extract_type env db j c args = | Const (kn,u as c) -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ,_ = Typeops.type_of_constant env c in + let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *) (match flag_of_type env typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 54066edfb..e00fa528a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -78,8 +78,10 @@ let def_of_const t = let type_of_const t = match (kind_of_term t) with - Const sp -> Typeops.type_of_constant (Global.env()) sp - |_ -> assert false + | Const sp -> + (* FIXME discarding universe constraints *) + Typeops.type_of_constant_in (Global.env()) sp + |_ -> assert false let constr_of_global x = fst (Universes.unsafe_constr_of_global x) @@ -1422,7 +1424,7 @@ let start_equation (f:global_reference) (term_f:global_reference) (cont_tactic:Id.t list -> tactic) g = let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in - let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in + let nargs = nb_prod (type_of_const terminate_constr) in let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; |