aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r--interp/notation_ops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5066e2e22..f6afbe48a 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -473,7 +473,7 @@ let rec subst_notation_constr subst bound raw =
| _ -> knd
in
let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in
- if nsolve == solve && nknd = knd then raw
+ if nsolve == solve && nknd == knd then raw
else NHole (nknd, nsolve)
| NCast (r1,k) ->