From 937b4a9ab459696fccd613e52601411c4f1dadef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Oct 2017 11:50:02 +0200
Subject: Fix relative meaning of Pattern vs. Context in match goal.

---
 src/tac2core.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

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
-- 
cgit v1.2.3