From f1684dd7722e42c9a2de12d14101098c3bf92036 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 00:05:58 +0000
Subject: 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
---
 kernel/generic.mli | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'kernel/generic.mli')

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
-- 
cgit v1.2.3