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 /plugins/ltac | |
| parent | 6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (diff) | |
| parent | 467d4f28802bf07bb0cdb748c78f0936219ceb8d (diff) | |
Merge PR #11027: Cleanup post #10647 (expose comind universe handling)
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index ca5c8b30c2..98d14f3d33 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1930,7 +1930,7 @@ let build_morphism_signature env sigma m = let evd = solve_constraints env !evd in let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in - Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m); + Pretyping.check_evars env evd (EConstr.of_constr m); Evd.evar_universe_context evd, m let default_morphism sign m = |