diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7a525f84a5..b41160f758 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw = match raw with | NRef ref -> let ref',t = subst_global subst ref in - if ref' == ref then raw else - fst (notation_constr_of_constr bound t) + if ref' == ref then raw else (match t with + | None -> NRef ref' + | Some t -> + fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value)) | NVar _ -> raw |