diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 10 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 9 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/structures.ml | 2 |
5 files changed, 15 insertions, 10 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 5eb8a88698..d6ba84d0bf 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -232,7 +232,17 @@ let occur_rigidly flags env evd (evk,_) t = let check_conv_record env sigma (t1,sk1) (t2,sk2) = let open ValuePattern in let (proji, u), arg = Termops.global_app_of_constr sigma t1 in + let t2, sk2' = decompose_app_vect sigma (shrink_eta env t2) in + let sk2 = Stack.append_app sk2' sk2 in let (sigma, solution), sk2_effective = + let t2 = + let rec remove_lambda t2 = + match EConstr.kind sigma t2 with + | Lambda (_,_,t2) -> remove_lambda t2 + | Cast (t2,_,_) -> remove_lambda t2 + | App (t2,_) -> t2 + | _ -> t2 in + if Stack.is_empty sk2 then remove_lambda t2 else t2 in try match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 86d2cc78e0..5a8ac32ffa 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -104,9 +104,8 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with let cast_type_eq eq t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> eq t1 t2 | CastVM t1, CastVM t2 -> eq t1 t2 - | CastCoerce, CastCoerce -> true | CastNative t1, CastNative t2 -> eq t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + | (CastConv _ | CastVM _ | CastNative _), _ -> false let matching_var_kind_eq k1 k2 = match k1, k2 with | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 @@ -188,14 +187,12 @@ let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce | CastNative a -> CastNative (f a) let smartmap_cast_type f c = match c with | CastConv a -> let a' = f a in if a' == a then c else CastConv a' | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce | CastNative a -> let a' = f a in if a' == a then c else CastNative a' let map_glob_constr_left_to_right f = DAst.map (function @@ -275,7 +272,7 @@ let fold_glob_constr f acc = DAst.with_val (function Array.fold_left f (Array.fold_left f acc tyl) bv | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f acc t in f acc c | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc @@ -318,7 +315,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function Array.fold_left_i f' acc idl | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f v acc t in f v acc c | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 9f93e5e6c1..d480c12834 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -57,7 +57,6 @@ and glob_fix_kind = type 'a cast_type = | CastConv of 'a | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) | CastNative of 'a (** The kind of patterns that occurs in "match ... with ... end" diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 21b2137f09..4c2fc26b45 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1166,9 +1166,6 @@ struct let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = match k with - | CastCoerce -> - let sigma, cj = pretype empty_tycon env sigma c in - Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in diff --git a/pretyping/structures.ml b/pretyping/structures.ml index 3ef6e98373..145663d3b9 100644 --- a/pretyping/structures.ml +++ b/pretyping/structures.ml @@ -161,6 +161,7 @@ let rec of_constr env t = let patt, n, args = of_constr env f in patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] + | Lambda (_, _, b) -> let patt, _, _ = of_constr env b in patt, None, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] @@ -222,6 +223,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let lpj = keep_true_projections lpj in let nenv = Termops.push_rels_assum sign env in List.fold_left2 (fun acc (spopt, canonical) t -> + let t = EConstr.Unsafe.to_constr (shrink_eta env (EConstr.of_constr t)) in if canonical then Option.cata (fun proji_sp -> |