diff options
| -rw-r--r-- | src/tac2core.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index c4502f8eae..1cfb34c249 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -604,7 +604,7 @@ let () = define3 "pattern_matches_goal" bool (list (pair bool pattern)) (pair bo let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in - let mk_pattern (b, pat) = if b then Tac2match.MatchContext pat else Tac2match.MatchPattern pat in + let mk_pattern (b, pat) = if b then Tac2match.MatchPattern pat else Tac2match.MatchContext pat in let r = (List.map mk_pattern hp, mk_pattern cp) in Tac2match.match_goal env sigma concl ~rev r >>= fun (hyps, ctx, subst) -> let of_ctxopt ctx = Value.of_constr (Option.default empty_context ctx) in |