diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /proofs | |
| 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')
| -rw-r--r-- | proofs/clenv.ml | 10 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 6 |
3 files changed, 8 insertions, 10 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ab301c450..0cd364b93 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 diff --git a/proofs/logic.ml b/proofs/logic.ml index a92276cc8..db9b7c110 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -157,7 +157,7 @@ let new_meta_variables = | IsCast (c,t) -> mkCast (newrec c, t) | IsAppL (f,cl) -> applist (newrec f, List.map newrec cl) | IsMutCase (ci,p,c,lf) -> - mkMutCaseA ci (newrec p) (newrec c) (Array.map newrec lf) + mkMutCase (ci, newrec p, newrec c, Array.map newrec lf) | _ -> x in newrec diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 28eaa7ad4..b96f17af5 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -765,8 +765,7 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = in idents := Some (function - Const sp -> List.mem sp idl - | Abst sp -> List.mem sp idl + | Const sp -> List.mem sp idl | _ -> false) else user_err_loc(loc,"flag_of_ast", [<'sTR "Cannot specify identifiers to unfold twice">]) @@ -781,8 +780,7 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = in idents := Some (function - Const sp -> not (List.mem sp idl) - | Abst sp -> not (List.mem sp idl) + | Const sp -> not (List.mem sp idl) | _ -> false) else user_err_loc(loc,"flag_of_ast", [<'sTR "Cannot specify identifiers to unfold twice">]) |