diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
| commit | dfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (patch) | |
| tree | c6e4c772dae91a047c488f20fb3b03afd384300a /vernac/classes.ml | |
| parent | 6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (diff) | |
| parent | 467d4f28802bf07bb0cdb748c78f0936219ceb8d (diff) | |
Merge PR #11027: Cleanup post #10647 (expose comind universe handling)
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 0333b73ffe..c9b5144299 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env = (* Beware of this step, it is required as to minimize universes. *) let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) - Pretyping.check_evars env (Evd.from_env env) sigma termtype; + Pretyping.check_evars env sigma termtype; termtype, sigma let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = |