From bd462a21974caca5928ae172a7740a1f96ae0ae4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Oct 2017 14:48:34 +0200
Subject: Fix goal_matching quotation.

---
 src/tac2quote.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 9728c3af93..1275c939c5 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -419,10 +419,10 @@ let of_goal_matching (loc, gm) =
   in
   let map (loc, (pat, tac)) =
     let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in
-    let tac = abstract_vars loc hyps tac in
-    let tac = abstract_vars loc hctx tac in
+    let tac = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar cctx, None], tac) in
     let tac = abstract_vars loc subst tac in
-    let tac = abstract_vars loc [cctx] tac in
+    let tac = abstract_vars loc hctx tac in
+    let tac = abstract_vars loc hyps tac in
     of_tuple ?loc [pat; tac]
   in
   of_list ?loc map gm
-- 
cgit v1.2.3