diff options
author | 2000-03-21 00:05:58 +0000 | |
---|---|---|
committer | 2000-03-21 00:05:58 +0000 | |
commit | f1684dd7722e42c9a2de12d14101098c3bf92036 (patch) | |
tree | 8e702c39682c292735484d6a0bba49ddaa686d4b /kernel/generic.ml | |
parent | 9fad5317634c476fdb073c7dfa3ea81b6607d41f (diff) |
Déplacement fonction du discharge dans Discharge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@341 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/generic.ml')
-rw-r--r-- | kernel/generic.ml | 52 |
1 files changed, 0 insertions, 52 deletions
diff --git a/kernel/generic.ml b/kernel/generic.ml index 0484a801d..329103fa1 100644 --- a/kernel/generic.ml +++ b/kernel/generic.ml @@ -502,58 +502,6 @@ let under_dlams f = apprec -(* utility for discharge *) -type modification_action = ABSTRACT | ERASE - -let interp_modif absfun oper (oper',modif) cl = - let rec interprec = function - | ([], cl) -> DOPN(oper',Array.of_list cl) - | (ERASE::tlm, c::cl) -> interprec (tlm,cl) - | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c - | _ -> assert false - in - interprec (modif,cl) - - -type 'a modification = - | NOT_OCCUR - | DO_ABSTRACT of 'a * modification_action list - | DO_REPLACE - -let modify_opers replfun absfun oper_alist = - let failure () = - anomalylabstrm "generic__modify_opers" - [< 'sTR"An oper which was never supposed to appear has just appeared" ; - 'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC; - 'sTR"report this error," ; 'sPC ; - 'sTR"Or you are using a user-written tactic which calls" ; 'sPC ; - 'sTR"generic__modify_opers, in which case the user-written code" ; - 'sPC ; 'sTR"is broken - this function is an internal system" ; - 'sPC ; 'sTR"for internal system use only" >] - in - let rec substrec = function - | DOPN(oper,cl) as c -> - let cl' = Array.map substrec cl in - (try - (match List.assoc oper oper_alist with - | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',modif) -> - if List.length modif > Array.length cl then - anomaly "found a reference with too few args" - else - interp_modif absfun oper (oper',modif) (Array.to_list cl') - | DO_REPLACE -> substrec (replfun (DOPN(oper,cl')))) - with - | Not_found -> DOPN(oper,cl')) - | DOP1(i,c) -> DOP1(i,substrec c) - | DOPL(oper,cl) -> DOPL(oper,List.map substrec cl) - | DOP2(oper,c1,c2) -> DOP2(oper,substrec c1,substrec c2) - | DLAM(na,c) -> DLAM(na,substrec c) - | DLAMV(na,v) -> DLAMV(na,Array.map substrec v) - | x -> x - in - if oper_alist = [] then fun x -> x else substrec - let put_DLAMSV lna lc = match lna with | [] -> anomaly "put_DLAM" |