aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/unification.ml8
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1caa629ff..f9a22b065 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1504,8 +1504,7 @@ let indirectly_dependent sigma c d decls =
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
- let sigma, subst = nf_univ_variables sigma in
- (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
+ (sigma, nf_evar sigma c)
let default_matching_core_flags sigma =
let ts = Names.full_transparent_state in {
@@ -1593,9 +1592,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
(fun test -> match test.testing_state with
| None -> None
| Some (sigma,_,l) ->
- let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
- let univs, subst = nf_univ_variables sigma in
- Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
+ let c = applist (local_strong whd_meta sigma c, l) in
+ Some (sigma, c))
let make_eq_test env evd c =
let out cstr =