diff options
| author | Théo Zimmermann | 2017-11-15 17:50:51 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-12-08 16:51:10 +0100 |
| commit | 3c2b1b7f99a1e06ad86a3c5dbf8369d773928e85 (patch) | |
| tree | 0bd8648bd40e3f881107a5e5f1d210e4289499ae /src | |
| parent | 2bd31e5fffbd6722f20016c3962088ab2008e2c0 (diff) | |
Adapt to removal of match_appsubterm.
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 -> |