diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-06 19:59:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:26:34 +0100 |
| commit | 258c8502eafd3e078a5c7478a452432b5c046f71 (patch) | |
| tree | d4ce21b23a67056242410fbd78362213700af099 /pretyping/tacred.ml | |
| parent | 77e638121b6683047be915da9d0499a58fcb6e52 (diff) | |
Constr_matching API using EConstr.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 9 |
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 |