diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 16:53:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 16:53:20 +0200 |
| commit | 332f092e3a30f8428b28f12c85c0a90e3f6d7171 (patch) | |
| tree | 87db578ae9f16c5d976069c19016f3890966ba73 /pretyping/evarconv.ml | |
| parent | 2ac8e0edebe0d9a6bde4d997327dbd2ffcde08b6 (diff) | |
Fix canonical structure resolution (makes test-suite files go through again).
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 86bd36a30..5265a875b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -125,7 +125,8 @@ let check_conv_record (t1,sk1) (t2,sk2) = let c2 = global_of_constr t2 in lookup_canonical_conversion (proji, Const_cs c2),sk2 with Not_found -> - lookup_canonical_conversion (proji,Default_cs),[] + let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in + (t2,cs),[] in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in @@ -148,7 +149,7 @@ let check_conv_record (t1,sk1) (t2,sk2) = let t' = subst_univs_level_constr subst t' in let bs' = List.map (subst_univs_level_constr subst) bs in let f, _ = decompose_app_vect t' in - ctx',(t2,f),c',bs',(Stack.append_app_list params Stack.empty,params1), + ctx',(t2, f),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n,Stack.zip(t2,sk2)) @@ -697,7 +698,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), us2 us); (fun i -> evar_conv_x trs env i CONV c1 app); (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1); - (fun i -> evar_conv_x trs env i CONV h h')] + (fun i -> evar_conv_x trs env i CONV h (substl ks h'))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = |