diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-15 11:24:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-15 11:26:44 +0100 |
| commit | cab5e98780deb1bb65dbeef5d558376f8e34bccc (patch) | |
| tree | 10e2cd1c272d676feea6dabd00669228372f3172 /pretyping/evarconv.ml | |
| parent | b270ad686075e5579dc3826fafdc324ea339785c (diff) | |
Fix #5368: Canonical structure unification fails.
Universe instances were lost during constructions of the canonical instance.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cb8844623..f7a3789a2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -218,6 +218,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = EConstr.of_constr t' in let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in + let params = List.map (fun c -> subst_univs_level_constr subst c) params in + let us = List.map (fun c -> subst_univs_level_constr subst c) us in let h, _ = decompose_app_vect sigma t' in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, |