diff options
| author | Hugo Herbelin | 2020-10-31 14:06:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 16:56:49 +0100 |
| commit | 78e600ac5f8aa9609cac4347c7a694428ae9d7cc (patch) | |
| tree | 54ddd0faba729e23d3cfc06c8d6457bb420a2d72 /vernac/classes.ml | |
| parent | 404a041fce68b4f7072de0b91b4e136f04250482 (diff) | |
Moving interpretation of user-level universes in constrintern.ml.
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 d5509e2697..3b69273570 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -503,7 +503,7 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype let interp_instance_context ~program_mode env ctx ~generalize pl tclass = - let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in + let sigma, decl = interp_univ_decl_opt env pl in let tclass = if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass |