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 /proofs/clenv.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 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ab301c4506..0cd364b93e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -429,10 +429,10 @@ let clenv_instance_term clenv c = let clenv_cast_meta clenv = let rec crec u = - match splay_constr u with - | (OpAppL | OpMutCase _), _ -> crec_hd u - | OpCast , [|c;_|] when isMeta c -> u - | op, cl -> gather_constr (op, Array.map crec cl) + match kind_of_term u with + | IsAppL _ | IsMutCase _ -> crec_hd u + | IsCast (c,_) when isMeta c -> u + | _ -> map_constr crec u and crec_hd u = match kind_of_term (strip_outer_cast u) with @@ -447,7 +447,7 @@ let clenv_cast_meta clenv = u) | IsAppL(f,args) -> mkAppList (crec_hd f) (List.map crec args) | IsMutCase(ci,p,c,br) -> - mkMutCaseA ci (crec_hd p) (crec_hd c) (Array.map crec br) + mkMutCase (ci, crec_hd p, crec_hd c, Array.map crec br) | _ -> u in crec |