aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a3983737d..9581db23d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -962,9 +962,10 @@ let simpl env sigma c = strong whd_simpl env sigma c
(* Reduction at specific subterms *)
let matches_head env sigma c t =
- match kind_of_term t with
+ let open EConstr in
+ match EConstr.kind sigma t with
| App (f,_) -> Constr_matching.matches env sigma c f
- | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p))
+ | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, Univ.Instance.empty))
| _ -> raise Constr_matching.PatternMatchingFailure
(** FIXME: Specific function to handle projections: it ignores what happens on the
@@ -999,8 +1000,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
else
try
let subst =
- if byhead then matches_head env sigma c t
- else Constr_matching.matches env sigma c t in
+ if byhead then matches_head env sigma c (EConstr.of_constr t)
+ else Constr_matching.matches env sigma c (EConstr.of_constr t) in
let ok =
if nowhere_except_in then Int.List.mem !pos locs
else not (Int.List.mem !pos locs) in