diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 4 | ||||
| -rw-r--r-- | src/tac2match.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 48cec86540..d21c1998da 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -561,7 +561,7 @@ let () = define2 "pattern_matches_subterm" pattern constr begin fun pat c -> Proofview.tclOR (return ans) (fun _ -> of_ans s) in pf_apply begin fun env sigma -> - let ans = Constr_matching.match_appsubterm env sigma pat c in + let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in of_ans ans end end @@ -593,7 +593,7 @@ let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c - Proofview.tclOR (return ans) (fun _ -> of_ans s) in pf_apply begin fun env sigma -> - let ans = Constr_matching.match_appsubterm env sigma pat c in + let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in of_ans ans end end diff --git a/src/tac2match.ml b/src/tac2match.ml index fef5647725..5035c9dba6 100644 --- a/src/tac2match.ml +++ b/src/tac2match.ml @@ -173,7 +173,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k (Some m_ctx) nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_appsubterm E.env E.sigma p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma (Id.Set.empty,p) term) imatching_error let hyp_match_type pat hyps = pick hyps >>= fun decl -> |