aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/invfun.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-17 15:06:26 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-24 23:58:23 +0200
commitbf13037e9ca39da28fb648e5488ce56ef8a1f1e2 (patch)
treee981dabe208b339db88188b7a5e89c53d77745a1 /plugins/funind/invfun.ml
parenta9d151a31937724543d5269e72b0262c8764c46e (diff)
[location] Use located in misctypes.
Diffstat (limited to 'plugins/funind/invfun.ml')
-rw-r--r--plugins/funind/invfun.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898..8da4f9233 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -31,8 +31,8 @@ module RelDecl = Context.Rel.Declaration
let pr_binding prc =
function
- | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
- | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
let pr_bindings prc prlc = function
| ImplicitBindings l ->