diff options
| author | Maxime Dénès | 2017-12-18 19:01:47 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 19:01:47 +0100 |
| commit | 80158e796b6df8eb36117f349c312127c5729a8c (patch) | |
| tree | bc38b9ea21b210464979ad62a6fdc816508a8c19 /pretyping | |
| parent | 62133e7aa410d6120279c10954d585a61301a2ea (diff) | |
| parent | cab5e98780deb1bb65dbeef5d558376f8e34bccc (diff) | |
Merge PR #6436: Fix #5368: Canonical structure unification fails.
Diffstat (limited to 'pretyping')
| -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 cb88446236..f7a3789a21 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, |