diff options
| author | Pierre-Marie Pédrot | 2018-04-13 12:49:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-04-13 12:49:54 +0200 |
| commit | f3b84cf63c242623bdcccd30c536e55983971da5 (patch) | |
| tree | 740984c577ed75c76edc2525b3de9bf744da3c21 /vernac/classes.ml | |
| parent | b68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff) | |
| parent | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (diff) | |
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contains evars
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 76d427add6..3c133f3175 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (* Check that the type is free of evars now. *) Pretyping.check_evars env Evd.empty sigma termtype; let termtype = to_constr sigma termtype in - let term = Option.map (to_constr sigma) term in + let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype |