diff options
| author | herbelin | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /pretyping/evarconv.ml | |
| parent | 583992b6ce38655855f6625a26046ce84c53cdc1 (diff) | |
Suppression de Abst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e4e2e48c59..f9a3fe69b0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -210,32 +210,6 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f3; f4] - | IsAbst (_,_), IsAbst (_,_) -> - let f1 () = - (term1=term2) & - (List.length(l1) = List.length(l2)) & - (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) - and f2 () = - if evaluable_abst env term2 then - evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 (abst_value env term2)) - else - evaluable_abst env term1 - & evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 (abst_value env term1)) appr2 - in - ise_try isevars [f1; f2] - - | IsAbst (_,_), _ -> - (evaluable_abst env term1) - & evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 (abst_value env term1)) appr2 - - | _, IsAbst (_,_) -> - (evaluable_abst env term2) - & evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 (abst_value env term2)) - | IsRel n, IsRel m -> n=m & (List.length(l1) = List.length(l2)) |