Fix relative meaning of Pattern vs. Context in match goal.

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