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

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