diff options
| author | Matthieu Sozeau | 2016-09-12 13:37:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-12 13:37:08 +0200 |
| commit | 7a3ef81f20e159bcf4d40227d36c54abbe69c3e9 (patch) | |
| tree | 1527039fb27481b1ce82e2d3cff8fa82ce834ce3 /pretyping/evarconv.ml | |
| parent | 12cedcbf4dcfe4fd43ab9f4b648314cac26b82db (diff) | |
| parent | 43869b4e05824244e666c60e0b740a80e8b09d0c (diff) | |
Merge remote-tracking branch 'github-coq/pr/249' into v8.6
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0fea2ba223..b033f5a395 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -314,7 +314,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = if Reductionops.Stack.compare_shape sk1 sk2 then ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) - + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -432,7 +432,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else quick_fail i and delta i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) - (whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM (vM,skM)) + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i cstsM (vM,skM)) in let default i = ise_try i [f1; consume apprF apprM; delta] in @@ -449,7 +450,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = - whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (termM',skM) + whd_betaiota_deltazeta_for_iota_state + (fst ts) env evd cstsM (termM',skM) in let delta' i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') |