diff options
| author | Pierre-Marie Pédrot | 2020-11-12 13:33:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-12 13:33:21 +0100 |
| commit | c53abd9bf4517ba66c732034fb5f9aedef6d0930 (patch) | |
| tree | b31f4b01a1e30edc1045c118c1f285b57583ea5e /vernac/classes.ml | |
| parent | 0245aa233e671372e9d3fb34f3b34706fd9f4bf7 (diff) | |
| parent | e7b39c73f48279980f8ea2238632bfbf6e3d4178 (diff) | |
Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in naming
Ack-by: gares
Reviewed-by: ppedrot
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 a100352145..054addc542 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 |