diff options
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r-- | pretyping/recordops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4f4e49d82..cb24ca804 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 @@ -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 @@ -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 |