diff options
| author | Pierre-Marie Pédrot | 2017-07-11 17:16:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-13 15:14:45 +0200 |
| commit | 603bfb392805fb8d1559d304bcf1b9c7b938bb6e (patch) | |
| tree | 37dde8996de9a02c03d518c69120b44827d4bc21 /pretyping/evarconv.ml | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
Getting rid of AUContext abstraction breakers in Recordops.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 87f29ba492..cb76df4e8a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let u, ctx' = Universes.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in let t' = EConstr.of_constr t' in |