diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e86a8a28c9..21b2137f09 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -35,6 +35,7 @@ open Environ open EConstr open Vars open Reductionops +open Structures open Type_errors open Typing open Evarutil @@ -653,12 +654,8 @@ struct sigma, { uj_val; uj_type } | Some arg -> - let sigma, ty = - match tycon with - | Some ty -> sigma, ty - | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in - let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in - sigma, { uj_val = c; uj_type = ty } + let j, sigma = GlobEnv.interp_glob_genarg ?loc ~poly env sigma tycon arg in + sigma, j let pretype_rec self (fixkind, names, bl, lar, vdef) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -805,8 +802,8 @@ struct in let app_f = match EConstr.kind sigma fj.uj_val with - | Const (p, u) when Recordops.is_primitive_projection p -> - let p = Option.get @@ Recordops.find_primitive_projection p in + | Const (p, u) when PrimitiveProjections.mem p -> + let p = Option.get @@ PrimitiveProjections.find_opt p in let p = Projection.make p false in let npars = Projection.npars p in fun n -> @@ -1398,7 +1395,7 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let path_convertible env sigma i p q = +let path_convertible env sigma cl p q = let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in @@ -1423,7 +1420,7 @@ let path_convertible env sigma i p q = p' | [] -> (* identity function for the class [i]. *) - let cl,params = class_info_from_index i in + let params = class_nparams cl in let clty = match cl with | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false}) @@ -1434,8 +1431,7 @@ let path_convertible env sigma i p q = | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p)) in let names = - List.init params.cl_param - (fun n -> Id.of_string ("x" ^ string_of_int n)) + List.init params (fun n -> Id.of_string ("x" ^ string_of_int n)) in List.fold_right (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ |