diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-30 15:43:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 19:13:51 +0200 |
| commit | fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c (patch) | |
| tree | 2216811759d98065347041e5dbb19d1caaffd37e | |
| parent | d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962 (diff) | |
Cosmetic changes in evarconv.ml: hopefully more regular names and form
of arguments of eta_constructor.
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d3e18953a..b73ff2bc5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -469,7 +469,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let eta evd = match kind_of_term termR with | Lambda _ -> eta env evd false apprR apprF - | Construct u -> eta_constructor ts env evd skR u skF termF + | Construct u -> eta_constructor ts env evd (u,skR) apprF | _ -> UnifFailure (evd,NotSameHead) in let postpone tR lF evd = @@ -755,10 +755,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty rigids env evd sk1 term1 sk2 term2 | Construct u, _ -> - eta_constructor ts env evd sk1 u sk2 term2 + eta_constructor ts env evd (u,sk1) appr2 | _, Construct u -> - eta_constructor ts env evd sk2 u sk1 term1 + eta_constructor ts env evd (u,sk2) appr1 | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fst (decompose_app_vect (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> |