diff options
Diffstat (limited to 'pretyping')
42 files changed, 151 insertions, 141 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ea33f1c0d6..d59102b6c7 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -10,6 +10,7 @@ open Names open Globnames open Term +open Constr open Environ open Util open Libobject @@ -103,7 +104,7 @@ let rename_type_of_constructor env cstruct = let rename_typing env c = let j = Typeops.infer env c in let j' = - match kind_of_term c with + match kind c with | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) } | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) } | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) } diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 804e38216c..b499da3ab7 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -9,7 +9,7 @@ open Names open Globnames open Environ -open Term +open Constr val rename_arguments : bool -> global_reference -> Name.t list -> unit diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aefa09dbe6..4f3669a2b9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -13,7 +13,7 @@ open CErrors open Util open Names open Nameops -open Term +open Constr open Termops open Environ open EConstr @@ -1014,7 +1014,7 @@ let adjust_impossible_cases pb pred tomatch submat = this means that the Evd.define below may redefine an already defined evar. See e.g. first definition of test for bug #3388. *) let pred = EConstr.Unsafe.to_constr pred in - begin match kind_of_term pred with + begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin let evd, default = use_unit_judge !(pb.evdref) in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index cbf5788e48..3a139b7b03 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Evd open Environ open EConstr @@ -124,7 +124,7 @@ val prepare_predicate : ?loc:Loc.t -> (types * tomatch_type) list -> (rel_context * rel_context) list -> constr option -> - glob_constr option -> (Evd.evar_map * Names.name list * constr) list + glob_constr option -> (Evd.evar_map * Name.t list * constr) list -val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> +val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t -> Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 19d61a64db..3a2eac7e79 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -8,7 +8,7 @@ open Util open Names -open Term +open Constr open Vars open CClosure open Esubst @@ -211,7 +211,7 @@ and reify_value = function (* reduction under binders *) t (* map_constr_with_binders subs_lift (cbv_norm_term) env t *) | LAM (n,ctxt,b,env) -> - List.fold_left (fun c (n,t) -> Term.mkLambda (n, t, c)) b ctxt + List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) b ctxt | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, @@ -240,7 +240,7 @@ and reify_value = function (* reduction under binders *) let rec norm_head info env t stack = (* no reduction under binders *) - match kind_of_term t with + match kind t with (* stack grows (remove casts) *) | App (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) @@ -294,7 +294,7 @@ let rec norm_head info env t stack = (* non-neutral cases *) | Lambda _ -> - let ctxt,b = decompose_lam t in + let ctxt,b = Term.decompose_lam t in (LAM(List.length ctxt, List.rev ctxt,b,env), stack) | Fix fix -> (FIXP(fix,env,[||]), stack) | CoFix cofix -> (COFIXP(cofix,env,[||]), stack) @@ -411,12 +411,12 @@ and cbv_norm_value info = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (apply_stack info (cbv_norm_value info v) stk) | CBN(t,env) -> - map_constr_with_binders subs_lift (cbv_norm_term info) env t + Constr.map_with_binders subs_lift (cbv_norm_term info) env t | LAM (n,ctxt,b,env) -> let nctxt = List.map_i (fun i (x,ty) -> (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in - compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) + Term.compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 3ee7bebf08..5f9609a5c5 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -24,7 +24,7 @@ val cbv_norm : cbv_infos -> constr -> constr (*********************************************************************** i This is for cbv debug *) -open Term +open Constr type cbv_value = | VAL of int * constr diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 260cd04446..c36630f5d3 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -10,12 +10,12 @@ open CErrors open Util open Pp open Names +open Constr open Libnames open Globnames open Nametab open Environ open Libobject -open Term open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -27,9 +27,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t type cl_info_typ = { cl_param : int @@ -43,7 +43,7 @@ type coe_info_typ = { coe_value : constr; coe_type : types; coe_local : bool; - coe_context : Univ.universe_context_set; + coe_context : Univ.ContextSet.t; coe_is_identity : bool; coe_is_projection : bool; coe_param : int } @@ -59,8 +59,8 @@ let coe_info_typ_equal c1 c2 = let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2 + | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2 | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 8707078b58..b41d0efac5 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -17,9 +17,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ddef1cee96..b7b76c8309 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -214,7 +214,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let convref ref c = match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.Id.equal id id' - | ConstRef c, Const (c',_) -> Names.eq_constant c c' + | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' | _, _ -> @@ -286,7 +286,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (c1,arg1), App (c2,arg2) -> (match c1, EConstr.kind sigma c2 with - | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) + | PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> @@ -303,7 +303,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels with Invalid_argument _ -> raise PatternMatchingFailure) | PApp (PRef (ConstRef c1), _), Proj (pr, c2) - when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> + when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 34c62043ef..780ccc23d1 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -9,7 +9,7 @@ (** This module implements pattern-matching on terms *) open Names -open Term +open Constr open EConstr open Environ open Pattern diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c02fc5aafd..0d1e401d98 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -554,7 +554,7 @@ and detype_r d flags avoid env sigma t = let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in id,l with Not_found -> - Id.of_string ("X" ^ string_of_int (Evar.repr evk)), + Id.of_string ("X" ^ string_of_int (Evar.repr evk)), (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (id, diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index f03bde68ec..cb1c0d8d4b 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Glob_term @@ -40,7 +39,7 @@ val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> const val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g -val detype_sort : evar_map -> sorts -> glob_sort +val detype_sort : evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0f1a508c8d..681eb17d3c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -10,6 +10,7 @@ open CErrors open Util open Names open Term +open Constr open Termops open Environ open EConstr @@ -49,7 +50,7 @@ let _ = Goptions.declare_bool_option { let impossible_default_case () = let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in let (_, u) = Term.destConst c in - Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) + Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) let coq_unit_judge = let open Environ in @@ -175,7 +176,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Sort s -> let s = ESorts.kind sigma s in lookup_canonical_conversion - (proji, Sort_cs (family_of_sort s)),[] + (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> let c2 = Globnames.ConstRef (Projection.constant p) in let c = Retyping.expand_projection env sigma p c [] in @@ -297,7 +298,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, @@ -341,7 +342,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ @@ -771,7 +772,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] (* Catch the p.c ~= p c' cases *) - | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> + | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' -> let res = try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None @@ -782,7 +783,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (appr2,csts2) | None -> UnifFailure (evd,NotSameHead)) - | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> + | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') -> let res = try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index c30d1d26bf..d793b06d3d 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -47,7 +47,7 @@ val check_problems_are_solved : env -> evar_map -> unit val check_conv_record : env -> evar_map -> state -> state -> - Univ.universe_context_set * (constr * constr) + Univ.ContextSet.t * (constr * constr) * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * constr * diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 5f12f360b3..18dbbea1bd 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -10,6 +10,7 @@ open Util open Pp open Names open Term +open Constr open Termops open EConstr open Vars @@ -82,7 +83,7 @@ let define_pure_evar_as_product evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort (ESorts.kind evd1 s) then + if Sorts.is_prop (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 5477c5c99d..869e3adbf9 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Evd open Environ @@ -39,7 +38,7 @@ val lift_tycon : int -> type_constraint -> type_constraint val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types -val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t (** {6 debug pretty-printer:} *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b906c3b597..fba1542912 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -10,6 +10,7 @@ open Util open CErrors open Names open Term +open Constr open Environ open Termops open Evd @@ -1391,7 +1392,7 @@ let occur_evar_upto_types sigma n c = let c = EConstr.Unsafe.to_constr c in let seen = ref Evar.Set.empty in (** FIXME: Is that supposed to be evar-insensitive? *) - let rec occur_rec c = match kind_of_term c with + let rec occur_rec c = match Constr.kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> if Evar.Set.mem sp !seen then diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 811b4dc18f..e5d288b5c3 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr open Evd open Environ diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index f27928662e..9dd7068cbc 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -64,7 +64,7 @@ val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_ here by its relevant components [m] and [c]. It is used to interpret Ltac-bound names both in pretyping and printing of terms. *) -val map_pattern_binders : (name -> name) -> +val map_pattern_binders : (Name.t -> Name.t) -> tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses) (** [map_pattern f m c] applies [f] to the return predicate and the @@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name +val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index aced42f839..48b33e708c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -18,6 +18,7 @@ open Libnames open Globnames open Nameops open Term +open Constr open Vars open Namegen open Declarations @@ -33,7 +34,7 @@ type dep_flag = bool (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive @@ -168,7 +169,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in - match kind_of_term p' with + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) @@ -186,13 +187,13 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | _ -> let t' = whd_all env sigma (EConstr.of_constr p) in let t' = EConstr.Unsafe.to_constr t' in - if Term.eq_constr p' t' then assert false + if Constr.equal p' t' then assert false else prec env i sign t' in prec env 0 [] in let rec process_constr env i c recargs nhyps li = - if nhyps > 0 then match kind_of_term c with + if nhyps > 0 then match kind c with | Prod (n,t,c_0) -> let (optionpos,rest) = match recargs with @@ -247,7 +248,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in - match kind_of_term p' with + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) @@ -261,7 +262,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | _ -> let t' = whd_all env sigma (EConstr.of_constr p) in let t' = EConstr.Unsafe.to_constr t' in - if Term.eq_constr t' p' then assert false + if Constr.equal t' p' then assert false else prec env i hyps t' in prec env 0 [] @@ -505,7 +506,7 @@ let build_case_analysis_scheme_default env sigma pity kind = [rec] by [s] *) let change_sort_arity sort = - let rec drec a = match kind_of_term a with + let rec drec a = match kind a with | Cast (c,_,_) -> drec c | Prod (n,t,c) -> let s, c' = drec c in s, mkProd (n, t, c') | LetIn (n,b,t,c) -> let s, c' = drec c in s, mkLetIn (n,b,t,c') @@ -519,7 +520,7 @@ let change_sort_arity sort = let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in let rec drec np elim = - match kind_of_term elim with + match kind elim with | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in @@ -566,7 +567,7 @@ let build_mutual_induction_scheme env sigma = function (List.map (function ((mind',u'),dep',s') -> let (sp',_) = mind' in - if eq_mind sp sp' then + if MutInd.equal sp sp' then let (mibi',mipi') = lookup_mind_specif env mind' in ((mind',u'),mibi',mipi',dep',s') else @@ -605,7 +606,7 @@ let lookup_eliminator ind_sp s = (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in + let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in let _ = Global.lookup_constant cst in ConstRef cst with Not_found -> diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 2825c4d83a..a9838cffe5 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -7,14 +7,14 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Evd (** Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive @@ -27,25 +27,25 @@ type dep_flag = bool (** Build a case analysis elimination scheme in some sort family *) val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * Constr.t + dep_flag -> Sorts.family -> evar_map * Constr.t (** Build a dependent case elimination predicate unless type is in Prop or is a recursive record with primitive projections. *) val build_case_analysis_scheme_default : env -> evar_map -> pinductive -> - sorts_family -> evar_map * Constr.t + Sorts.family -> evar_map * Constr.t (** Builds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop or a recursive record with primitive projections. *) val build_induction_scheme : env -> evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * constr + dep_flag -> Sorts.family -> evar_map * constr (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * sorts_family) list -> evar_map * constr list + env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) @@ -54,13 +54,13 @@ val build_mutual_induction_scheme : scheme quantified on sort [s]. [set] asks for [s] be declared equal to [i], otherwise just less or equal to [i]. *) -val weaken_sort_scheme : env -> evar_map -> bool -> sorts -> int -> constr -> types -> +val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> types -> evar_map * types * constr (** Recursor names utilities *) -val lookup_eliminator : inductive -> sorts_family -> Globnames.global_reference -val elimination_suffix : sorts_family -> string -val make_elimination_ident : Id.t -> sorts_family -> Id.t +val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference +val elimination_suffix : Sorts.family -> string +val make_elimination_ident : Id.t -> Sorts.family -> Id.t val case_suffix : string diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b31ee03d8c..34df7d3d72 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -11,6 +11,7 @@ open Util open Names open Univ open Term +open Constr open Vars open Termops open Declarations @@ -643,7 +644,7 @@ let type_of_projection_knowing_arg env sigma p c ty = syntactic conditions *) let control_only_guard env c = - let check_fix_cofix e c = match kind_of_term c with + let check_fix_cofix e c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> @@ -659,7 +660,7 @@ let control_only_guard env c = (* inference of subtyping condition for inductive types *) let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = let numchecked = ref 0 in let numparams = Context.Rel.nhyps params in let update_contexts (env, evd, csts) csts' = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index aa38d3b47d..febe99b0bc 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Declarations open Environ open Evd @@ -120,7 +120,7 @@ val constructor_nrealdecls_env : env -> constructor -> int val constructor_has_local_defs : constructor -> bool val inductive_has_local_defs : inductive -> bool -val allowed_sorts : env -> inductive -> sorts_family list +val allowed_sorts : env -> inductive -> Sorts.family list (** (Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination. *) @@ -147,17 +147,17 @@ val get_constructor : pinductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary val get_constructors : env -> inductive_family -> constructor_summary array -val get_projections : env -> inductive_family -> constant array option +val get_projections : env -> inductive_family -> Constant.t array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * Sorts.family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context -val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types +val make_arity : env -> evar_map -> bool -> inductive_family -> Sorts.t -> EConstr.types val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) @@ -172,7 +172,7 @@ val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr. (** Builds the case predicate arity (dependent or not) *) val arity_of_case_predicate : - env -> inductive_family -> bool -> sorts -> types + env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types @@ -203,8 +203,8 @@ val control_only_guard : env -> types -> unit (* inference of subtyping condition for inductive types *) (* for debugging purposes only to be removed *) val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> -(Term.constr -> Term.constr) -> -Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t +(constr -> constr) -> +types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index fe134f5126..dafe8cb269 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -7,6 +7,7 @@ (************************************************************************) open CErrors open Term +open Constr open Vars open Environ open Reduction @@ -98,7 +99,7 @@ let app_type env c = let find_rectype_a env c = let (t, l) = app_type env c in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -131,7 +132,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = let construct_of_constr const env tag typ = let t, l = app_type env typ in - match kind_of_term t with + match kind t with | Ind (ind,u) -> construct_of_constr_notnative const env tag ind u l | _ -> assert false @@ -360,7 +361,7 @@ and nf_atom_type env sigma atom = and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind_of_term pT with + match kind_of_value v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in let vb = f (mk_rel_accu k) in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index aaa9467068..ee79b54744 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -12,6 +12,7 @@ open Names open Globnames open Nameops open Term +open Constr open Vars open Glob_term open Pp @@ -75,8 +76,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) = and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Term.eq_constr c1 c2 && - Array.equal Term.eq_constr r1 r2 + Array.equal Constr.equal c1 c2 && + Array.equal Constr.equal r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -149,7 +150,7 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with let pattern_of_constr env sigma t = let rec pattern_of_constr env t = let open Context.Rel.Declaration in - match kind_of_term t with + match kind t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id @@ -165,7 +166,7 @@ let pattern_of_constr env sigma t = pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match - match kind_of_term f with + match kind f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id @@ -174,7 +175,7 @@ let pattern_of_constr env sigma t = with | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) - | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) + | Const (sp,u) -> PRef (ConstRef (Constant.make1 (Constant.canonical sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 54b477bed9..ce478ac202 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Type_errors diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 124fa6e06c..dab376ef07 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Type_errors @@ -99,8 +99,8 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> - pinductive -> sorts_family list -> constr -> - unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b + pinductive -> Sorts.family list -> constr -> + unsafe_judgment -> (Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 6537d1ecf7..eb2b435bf6 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,7 +12,7 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) -open Term +open Constr open Environ open Evd open EConstr diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e970a1db90..cb24ca804d 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,7 @@ open Pp open Names open Globnames open Nametab -open Term +open Constr open Libobject open Mod_subst open Reductionops @@ -37,7 +37,7 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } let structure_table = Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" @@ -48,7 +48,7 @@ let projection_table = is the inductive always (fst constructor) ? It seems so... *) type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in @@ -144,7 +144,7 @@ type obj_typ = { type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with @@ -172,7 +172,7 @@ let keep_true_projections projs kinds = List.map_filter filter (List.combine projs kinds) let cs_pattern_of_constr env t = - match kind_of_term t with + match kind t with App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs @@ -184,7 +184,7 @@ let cs_pattern_of_constr env t = let { Environ.uj_type = ty } = Typeops.infer env c in let _, params = Inductive.find_rectype env ty in Const_cs (ConstRef (Projection.constant p)), None, params @ [c] - | Sort s -> Sort_cs (family_of_sort s), None, [] + | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> begin try Const_cs (global_of_constr t) , None, [] @@ -213,7 +213,7 @@ let compute_canonical_projections warn (con,ind) = let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in let lt = List.rev_map snd sign in - let args = snd (decompose_app t) in + let args = snd (Term.decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = List.chop p args in @@ -286,7 +286,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let inCanonStruc : constant * inductive -> obj = +let inCanonStruc : Constant.t * inductive -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -311,10 +311,10 @@ let check_and_decompose_canonical_structure ref = | None -> error_not_structure ref in let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let body = EConstr.Unsafe.to_constr body in - let f,args = match kind_of_term body with + let f,args = match kind body with | App (f,args) -> f,args | _ -> error_not_structure ref in - let indsp = match kind_of_term f with + let indsp = match kind f with | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 8e2333b349..f15418577d 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Globnames (** Operations concerning records and canonical structures *) @@ -20,10 +20,10 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list val declare_structure : struc_tuple -> unit @@ -35,7 +35,7 @@ val lookup_structure : inductive -> struc_typ (** [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise it fails with [Not_found] *) -val lookup_projections : inductive -> constant option list +val lookup_projections : inductive -> Constant.t option list (** raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int @@ -52,7 +52,7 @@ val find_projection : global_reference -> struc_typ type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs type obj_typ = { diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2aa2f90131..04374c88b4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Termops open Univ open Evd @@ -339,7 +339,7 @@ struct type 'a member = | App of 'a app_node - | Case of Term.case_info * 'a * 'a array * Cst_stack.t + | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t @@ -358,7 +358,7 @@ struct ++ str ")" | Proj (n,m,p,cst) -> str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ - pr_comma () ++ pr_con (Projection.constant p) ++ str ")" + pr_comma () ++ Constant.print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -1314,7 +1314,9 @@ let pb_equal = function | Reduction.CONV -> Reduction.CONV let report_anomaly e = - let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in + let msg = Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) in + let e = UserError (None,msg) in let e = CErrors.push e in iraise e diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1828196fe4..db0c29aeff 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open EConstr open Univ open Evd @@ -258,7 +258,7 @@ val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixp val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) -val is_transparent : Environ.env -> constant tableKey -> bool +val is_transparent : Environ.env -> Constant.t tableKey -> bool (** {6 Conversion Functions (uses closures, lazy strategy) } *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 56f8b33e01..5dd6879d39 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -10,6 +10,7 @@ open Pp open CErrors open Util open Term +open Constr open Inductive open Inductiveops open Names @@ -146,7 +147,7 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> type1_sort + | Prop _ -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> @@ -167,7 +168,7 @@ let retype ?(polyprop=true) sigma = and sort_family_of env t = match EConstr.kind sigma t with - | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s) + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) | Sort _ -> InType | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in @@ -175,12 +176,12 @@ let retype ?(polyprop=true) sigma = s2 == InSet && sort_family_of env t == InType then InType else s2 | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in - family_of_sort (sort_of_atomic_type env sigma t args) + Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> - family_of_sort (decomp_sort env sigma (type_of env t)) + Sorts.family (decomp_sort env sigma (type_of env t)) and type_of_global_reference_knowing_parameters env c args = let argtyps = diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index ed3a9d0f96..af86df499c 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Evd open Environ open EConstr @@ -30,10 +29,10 @@ val get_type_of : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types val get_sort_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts + ?polyprop:bool -> env -> evar_map -> types -> Sorts.t val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts_family + ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment @@ -44,7 +43,7 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> val type_of_global_reference_knowing_conclusion : env -> evar_map -> constr -> types -> evar_map * types -val sorts_of_context : env -> evar_map -> rel_context -> sorts list +val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9451b0f868..85383ba398 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -75,13 +75,13 @@ let global_of_evaluable_reference = function | EvalVarRef id -> VarRef id type evaluable_reference = - | EvalConst of constant + | EvalConst of Constant.t | EvalVar of Id.t | EvalRel of int | EvalEvar of EConstr.existential let evaluable_reference_eq sigma r1 r2 = match r1, r2 with -| EvalConst c1, EvalConst c2 -> eq_constant c1 c2 +| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> @@ -240,7 +240,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - Some (EvalConst (con_with_label kn (Label.of_id id))) in + Some (EvalConst (Constant.change_label kn (Label.of_id id))) in match refi with | None -> None | Some ref -> @@ -521,7 +521,7 @@ let reduce_mind_case_use_function func env sigma mia = the block was indeed initially built as a global definition *) let (kn, u) = destConst sigma func in - let kn = con_with_label kn (Label.of_id id) in + let kn = Constant.change_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 @@ -944,7 +944,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | CoFix _ | Fix _ -> s' | Proj (p,t) when (match EConstr.kind sigma constr with - | Const (c', _) -> eq_constant (Projection.constant p) c' + | Const (c', _) -> Constant.equal (Projection.constant p) c' | _ -> false) -> let pb = Environ.lookup_projection p env in if List.length stack <= pb.Declarations.proj_npars then @@ -1050,7 +1050,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 + | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 375a8a983f..d55b286fb4 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,6 +11,7 @@ open Names open Globnames open Decl_kinds open Term +open Constr open Vars open Evd open Util @@ -71,7 +72,7 @@ type typeclass = { (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option - * constant option) list; + * Constant.t option) list; cl_strict : bool; diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 99cdbd3a36..062d5cf356 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -8,7 +8,7 @@ open Names open Globnames -open Term +open Constr open Evd open Environ @@ -36,7 +36,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1f35fa19aa..43066c8099 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -160,7 +160,7 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in - let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in + let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then @@ -195,11 +195,11 @@ let check_cofix env sigma pcofix = let judge_of_prop = { uj_val = EConstr.mkProp; - uj_type = EConstr.mkSort type1_sort } + uj_type = EConstr.mkSort Sorts.type1 } let judge_of_set = { uj_val = EConstr.mkSet; - uj_type = EConstr.mkSort type1_sort } + uj_type = EConstr.mkSort Sorts.type1 } let judge_of_prop_contents = function | Null -> judge_of_prop diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1e20788268..9f084ae8df 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Evd @@ -26,7 +26,7 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) -val e_sort_of : env -> evar_map ref -> types -> sorts +val e_sort_of : env -> evar_map ref -> types -> Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val e_check : env -> evar_map ref -> constr -> types -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 86ebc1f01f..5eb6b780ad 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -12,7 +12,7 @@ open CErrors open Pp open Util open Names -open Term +open Constr open Termops open Environ open EConstr @@ -68,10 +68,10 @@ let _ = Goptions.declare_bool_option { let unsafe_occur_meta_or_existential c = let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Evar _ -> raise Occur | Meta _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Occur -> true @@ -79,7 +79,7 @@ let occur_meta_or_undefined_evar evd c = (** This is performance-critical. Using the evar-insensitive API changes the resulting heuristic. *) let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Meta _ -> raise Occur | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with @@ -558,10 +558,10 @@ let oracle_order env cf1 cf2 = | Some k2 -> match k1, k2 with | IsProj (p, _), IsKey (ConstKey (p',_)) - when eq_constant (Projection.constant p) p' -> + when Constant.equal (Projection.constant p) p' -> Some (not (Projection.unfolded p)) | IsKey (ConstKey (p,_)), IsProj (p', _) - when eq_constant p (Projection.constant p') -> + when Constant.equal p (Projection.constant p') -> Some (Projection.unfolded p') | _ -> Some (Conv_oracle.oracle_order (fun x -> x) @@ -613,7 +613,7 @@ let subst_defined_metas_evars sigma (bl,el) c = (** This seems to be performance-critical, and using the evar-insensitive primitives blow up the time passed in this function. *) let c = EConstr.Unsafe.to_constr c in - let rec substrec c = match kind_of_term c with + let rec substrec c = match Constr.kind c with | Meta i -> let select (j,_,_) = Int.equal i j in substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl))) @@ -788,7 +788,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (** Fast path for projections. *) - | Proj (p1,c1), Proj (p2,c2) when eq_constant + | Proj (p1,c1), Proj (p2,c2) when Constant.equal (Projection.constant p1) (Projection.constant p2) -> (try unify_same_proj curenvnb cv_pb {opt with at_top = true} substn c1 c2 diff --git a/pretyping/unification.mli b/pretyping/unification.mli index fce17d5641..085e8c5b8b 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr open Environ open Evd diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 66cc42cb61..b5b8987e33 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -10,6 +10,7 @@ open Util open Names open Declarations open Term +open Constr open Vars open Environ open Inductive @@ -51,7 +52,7 @@ let invert_tag cst tag reloc_tbl = let find_rectype_a env c = let (t, l) = decompose_appvect (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> assert false @@ -262,7 +263,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind_of_term pT with + match whd_val v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in let vb = body_of_vfun k f in |