diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/generic.ml | 52 | ||||
| -rw-r--r-- | kernel/generic.mli | 10 |
2 files changed, 0 insertions, 62 deletions
diff --git a/kernel/generic.ml b/kernel/generic.ml index 0484a801d5..329103fa14 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" diff --git a/kernel/generic.mli b/kernel/generic.mli index cad600a50c..61686e9702 100644 --- a/kernel/generic.mli +++ b/kernel/generic.mli @@ -105,16 +105,6 @@ val sAPPViList : int -> 'a term -> 'a term list -> 'a term val under_dlams : ('a term -> 'a term) -> 'a term -> 'a term val eq_term : 'a term -> 'a term -> bool -type modification_action = ABSTRACT | ERASE - -type 'a modification = - | NOT_OCCUR - | DO_ABSTRACT of 'a * modification_action list - | DO_REPLACE - -val modify_opers : ('a term -> 'a term) -> ('a term -> 'a term -> 'a term) - -> ('a * 'a modification) list -> 'a term -> 'a term - val put_DLAMSV : name list -> 'a term array -> 'a term val decomp_DLAMV : int -> 'a term -> 'a term array val decomp_DLAMV_name : int -> 'a term -> name list * 'a term array |