diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 0a82a945a..e04bebe33 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -383,7 +383,7 @@ let make_conclusion_flexible evdref ty poly = | Type u -> (match Univ.universe_level u with | Some u -> - evdref := Evd.make_flexible_variable !evdref true u + evdref := Evd.make_flexible_variable !evdref ~algebraic:true u | None -> ()) | _ -> () else () diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index ae662d74b..567fc57fa 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1164,11 +1164,11 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in + let onlyprint = nobj.notobj_onlyprint in + let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in let active = is_active_compat nobj.notobj_compat in if Int.equal i 1 && fresh && active then begin (* Declare the interpretation *) - let onlyprint = nobj.notobj_onlyprint in let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in (* Declare the uninterpretation *) if not nobj.notobj_onlyparse then diff --git a/vernac/record.ml b/vernac/record.ml index 218cf7a0a..d61f44cac 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let s' = EConstr.ESorts.kind !evars s' in (if poly then match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true l; + | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; s, s', true | None -> s, s', false else s, s', false) |