diff options
| author | barras | 2001-03-01 10:09:34 +0000 |
|---|---|---|
| committer | barras | 2001-03-01 10:09:34 +0000 |
| commit | bb7d7482724489521dde94a5b70af7864acfa802 (patch) | |
| tree | 821dfa6baa108de2b2af016e842164f01a39101f /pretyping/evarconv.ml | |
| parent | 05b756a9a5079e91c5015239bb801918d4903c08 (diff) | |
nouvelle implantation de la reduction
suppression de IsXtra du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8dab704414..82746d287e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -257,8 +257,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | (IsMeta _ | IsXtra _ | IsLambda _), _ -> false - | _, (IsMeta _ | IsXtra _ | IsLambda _) -> false + | (IsMeta _ | IsLambda _), _ -> false + | _, (IsMeta _ | IsLambda _) -> false | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false |