diff options
| author | Pierre-Marie Pédrot | 2017-10-27 14:48:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-27 14:48:34 +0200 |
| commit | bd462a21974caca5928ae172a7740a1f96ae0ae4 (patch) | |
| tree | c3a930af934bead6a62c7f59a77e228fb080fd66 /src | |
| parent | 937b4a9ab459696fccd613e52601411c4f1dadef (diff) | |
Fix goal_matching quotation.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2quote.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |