Enlevé les trucs commités au mauvais endroit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 0 insertions, 1435 deletions

diff --git a/lib/biassoc.ml b/lib/biassoc.ml
deleted file mode 100644
index 2c8fc32167..0000000000
--- a/lib/biassoc.ml
+++ /dev/null
@@ -1,74 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: biassoc.ml aspiwack $ *)
-
-(* This modules implements a bidirectional association table,
-   that is a table where both values can be seen as the key for
-   the association.
-   For soundness reason, when adding an association [(a,b)] both
-   [a] and [b] must be unique.
-
-   Map is a reasonably efficient datastructure, which compares rather
-   well (in average) to the more imperative Hashtables. In that respect
-   and since persistent datastructures are used in the kernel, I write
-   this in the functional style.
-
-   This module have been originally written for being used both in the
-   retroknowledge for its internal representation (thus in the kernel)
-   and in the interactive proof system for associating dependent goals
-   to an evar. *)
-
-(* The internal representation is a straightforward pair of Maps
-   (one from a type 'a to a type 'b, and the other from the 
-   type 'b to the type 'a). Both are updated synchronously to 
-   provide fast access in both directions. *)
-
-
-
-
-type ('a,'b) biassoc = { left:('a,'b) Gmap.t ; right:('b,'a) Gmap.t }
-    
-let empty = { left=Gmap.empty ; right=Gmap.empty }
-let is_empty bm = (Gmap.is_empty bm.left)&&(Gmap.is_empty bm.right)
-  
-let find_with_left lt bm = Gmap.find lt bm.left
-let find_with_right rt bm = Gmap.find rt bm.right
-  
-let mem_with_left lt bm = Gmap.mem lt bm.left
-let mem_with_right rt bm = Gmap.mem rt bm.right
-  
-(* remove functions are not a direct lifting of the 
-   functions from either components, since you have to 
-   remove the corresponding binding in the second Map *)
-let remove_with_left lt bm = 
-  try 
-    let rt = find_with_left lt bm in
-      { left = Gmap.remove lt bm.left ;
-        right = Gmap.remove rt bm.right }
-  with Not_found ->
-    (* if there is no (lt, ?) in the left Map, then there
-       is no (?,lt) in the Right table. Thus bm is already
-       free of any reference to lt *)
-    bm
-      
-let remove_with_right rt bm = (* see remove_with_left *)
-  try 
-    let lt = find_with_right rt bm in
-      { left = Gmap.remove lt bm.left ;
-        right = Gmap.remove rt bm.right }
-  with Not_found ->
-    bm
-      
-let add lt rt bm = 
-  if not (mem_with_left lt bm) && not (mem_with_right rt bm) then
-    { left = Gmap.add lt rt bm.left ;
-      right = Gmap.add rt lt bm.right }
-  else
-    raise (Invalid_argument "Biassoc: non unique values")
-
diff --git a/lib/biassoc.mli b/lib/biassoc.mli
deleted file mode 100644
index 45426d1bc3..0000000000
--- a/lib/biassoc.mli
+++ /dev/null
@@ -1,61 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: biassoc.ml aspiwack $ *)
-
-(* This modules implements a bidirectional association table,
-   that is a table where both values can be seen as the key for
-   the association.
-   For soundness reason, when adding an association [(a,b)] both
-   [a] and [b] must be unique.
-
-   Map is a reasonably efficient datastructure, which compares rather
-   well (in average) to the more imperative Hashtables. In that respect
-   and since persistent datastructures are used in the kernel, I write
-   this in the functional style.
-
-   This module have been originally written for being used both in the
-   retroknowledge for its internal representation (thus in the kernel)
-   and in the interactive proof system for associating dependent goals
-   to an evar. *)
-
-
-
-type ('a,'b) biassoc
-(** the type of bidirectional association table between
-    ['a] and ['b] *)
-    
-val empty : ('a,'b) biassoc
-(** the empty bidirectional association table *)
-val is_empty : ('a,'b) biassoc -> bool
-(** tests the emptyness of a bidirectional association table *)
-val add : 'a -> 'b -> ('a,'b) biassoc -> ('a,'b) biassoc
-(** [add lt rt bm] return a bidirectional association table identical 
-    to [bm] except that there is an additional association between
-    [lt] and [rt].
-    If [lt] or [rt] are already present in an association in [bm]
-    then it raises [Invalid_argument "Biassoc: non unique values"] 
-    instead *)
-val find_with_left : 'a  -> ('a,'b) biassoc -> 'b
-(** [find_with_left lt bm] returns the value associated to [lt] it 
-    there is one. It raises [Not_found] otherwise. *)
-val find_with_right : 'b -> ('a,'b) biassoc -> 'a
-(** [find_with_right] works as [find_with_left] except that
-    it implements the other direction of the association. *)
-val remove_with_left : 'a -> ('a,'b) biassoc -> ('a,'b) biassoc
-(** [remove_with_left lt bm] returns a stack identical to [bm]
-    except that any association with [lt] has been removed. *)
-val remove_with_right : 'b -> ('a,'b) biassoc -> ('a,'b) biassoc
-(** [remove_with_right] works as [remove_with_left] except that
-    the key is from the right side of the associations. *)
-val mem_with_left : 'a -> ('a,'b) biassoc -> bool
-(** [mem_with_left lt bm] returns [true] if there is a value
-    associated to [lt] in [bm]. It returns [false] otherwise. *)
-val mem_with_right : 'b -> ('a,'b) biassoc -> bool
-(** [mem_with_right] works as [mem_with_left] except that it
-    implements the other direction. *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
deleted file mode 100644
index 2172373170..0000000000
--- a/proofs/goal.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: goal.ml aspiwack $ *)
-
-(* This module implements the abstract interface to goals *)
-
-
-type goal = Evd.evar_info
diff --git a/proofs/goal.mli b/proofs/goal.mli
deleted file mode 100644
index 829f4f23cb..0000000000
--- a/proofs/goal.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: goal.mli aspiwack $ *)
-
-(* This module implements the abstract interface to goals *)
-
-
-type goal
diff --git a/proofs/permutation.ml b/proofs/permutation.ml
deleted file mode 100644
index 8477f14960..0000000000
--- a/proofs/permutation.ml
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: permutation.ml aspiwack $ *)
-
-(* This module implements the permutations of arrays (it can probably
-   be extended to lists). *)
-
-(* This is not a module which is specific to the proof system, but it
-   is currently used only by it, thus it is held in the directory
-   proofs/. *)
-
-type permutation = int array
-
-(* Function checking if an array is of the form [| 0 1 ... (n-1) |] *)
-let check_correct =
-  let locally_correct ix elt =
-    if ix = elt then
-      ()
-    else
-      raise Not_found
-  in
-  fun arr ->
-    try
-      Array.iteri locally_correct arr ;
-      true
-    with Not_found ->
-      false
- 
-
-(* Function checking if an array is a permutation of [| 0 1 ... (n-1) |] *)
-let check_permutation arr =
-  let new_arr = Array.copy arr in
-  Array.fast_sort compare new_arr;
-  check_correct new_arr
-
-(* Function to build a permutation from an array. 
-   Raises Invalid_argument "Permutation.of_array: ill formed permutation"
-   if the array is not a permutation of [| 0 1 ... (n-1) |] *)
-let of_array arr =
-  if check_permutation arr then
-    Array.copy arr
-  else
-    invalid_arg "Permutation.of_array: ill formed permutation"
-
-(* Produces an occurence of the identity of size n *)
-let identity n =
-  Array.init n (fun i -> i)
-
-(* For an [n > Array.length perm], it extends the permutation with the
-   identity *)
-let extend perm n =
-  let ext = identity n in
-  Array.blit perm 0 ext 0 (Array.length perm);
-  ext
-
-(* Function to permute an array.
-   Raises Invalid_argument "Permutation.permute: array and permutation size do not match"
-   if the size of the array is smaller than that of the permutation.
-   If the size of the array is bigger than the permutation, then the permutation   is extended *)
-let permute =
-  (* permutes [arr] according to [per] both must be of length [len] *)
-  let unsafe_permute perm arr len =
-    Array.init len (fun i-> arr.(perm.(i)))
-  in
-  fun perm arr ->
-    let plen = Array.length perm in
-    let alen = Array.length arr in
-    if alen > plen then
-      unsafe_permute (extend perm alen) arr alen
-    else if alen = plen then
-      unsafe_permute perm arr alen
-    else
-      invalid_arg "Permutation.permute: array and permutation size do not match"
diff --git a/proofs/permutation.mli b/proofs/permutation.mli
deleted file mode 100644
index 9063f58159..0000000000
--- a/proofs/permutation.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: permutation.mli aspiwack $ *)
-
-(* This module implements the permutations of arrays (it can probably
-   be extended to lists). *)
-
-(* This is not a module which is specific to the proof system, but it
-   is currently used only by it, thus it is held in the directory
-   proofs/. *)
-
-type permutation
-
-(* Function to build a permutation from an array. 
-   Raises Invalid_arg "Permutation.of_array: ill formed permutation"
-   if the array is not a permutation of [| 0 1 ... (n-1) |] *)
-val of_array : int array -> permutation
-
-(* Function to permute an array.
-   Raises Invalid_argument "Permutation.permute: array and permutation size do not match"
-   if the size of the array is smaller than that of the permutation.
-   If the size of the array is bigger than the permutation, then the permutation   is extended *)
-val permute : permutation -> 'a array -> 'a array
diff --git a/proofs/proof.ml b/proofs/proof.ml
deleted file mode 100644
index c0bfc6f755..0000000000
--- a/proofs/proof.ml
+++ /dev/null
@@ -1,259 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: proof.ml aspiwack $ *)
-
-(* This module implements the actual proof datatype. It enforces strong
-   invariants, and it is the only module that should access the module
-   Subproof.
-   Actually from outside the proofs/ subdirectory, this is the only module
-   that should be used directly. *)
-
-(* arnaud: rajouter le blabla sur la  théorie du module ici *)
-
-(* arnaud: penser à garder une liste des positions qui seraient valide ? *)
-
-open Term
-
-type ('a,'b) subproof = ('a,'b) Subproof.subproof 
-     (* rather than opening Subproof *)
-
-open Transactional_stack
-
-
-
-type evar = unit (* arnaud: à compléter en temps utile aussi *)
-
-type 'a proof = { (* The root of the proof *)
-		  mutable root : ('a,[ `Subproof | `Resolved ]) Subproof.pointer;
-		  (* The list of focusings to be able to backtrack.
-		     The current focusing is the head of the list.
-		     The empty list means that the root is focused *)
-                  mutable focus : (constr,[ `Subproof | `Resolved | `Open ]) 
-		                                            Subproof.pointer list;
-		  (* The undo stack *)
-		  undo_stack : 'a undo_action transactional_stack;
-		  (* The dependent goal heap *)
-		  mutable dependent_goals : 
-		          ((constr,[ `Subproof | `Resolved | `Open ]) Subproof.pointer, evar) Biassoc.biassoc
-		}
-and 'a undo_action =  (* arnaud: à compléter et nettoyer en temps utile *)
-(*    | MutateBack of (constr,[ `Subproof | `Resolved | `Open ])  Subproof.pointer 
- * (constr,[ `Subproof | `Resolved | `Open ]) subproof *)
-    | MutateBack of packed_mutation
-    | Unfocus of 'a proof
-    | Focus of 'a proof * (constr,[`Subproof|`Resolved|`Open]) Subproof.pointer
-(*    | MutateRootBack of ('a,[ `Subproof | `Resolved ]) Subproof.pointer 
- * ('a,[ `Subproof | `Resolved ]) subproof *)
-
-(* Encoding the type
-     exists 'b 'c.{ sp : ('b,'c) subproof ; pt : ('b,'c) Subproof.pointer }
-   trick from Benjaming Pierce and Daniel Bünzli (cf: http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.en.html ) *)
-
-and ('b,'c) mutation = { sp : ('b,'c) subproof ; pt : ('b,'c) Subproof.pointer }
-and 't mutation_scope = { bind_mutation:'b 'c.('b,'c) mutation -> 't }
-and packed_mutation = { open_mutation : 't. 't mutation_scope -> 't }
-
-
-
-(* makes a packed_mutation out of mutation *)
-let pack_mutation mutn =
-  { open_mutation = fun scope -> scope.bind_mutation mutn }
-
-(* uses a scoped function on a packed mutation *)
-let unpack_mutation pck scp =
-  pck.open_mutation scp
-
-
-
-(* Gives the type of a proof action *)
-type 'a action = 'a proof -> 'a undo_action transaction -> unit
-
-(* arnaud: déplacer les séquences en externe, utiliser 
-  ('a proof -> 'a undo_action transaction) sequence pour les actions.
-   Et fournir l'algèbre correspondante. *)
-type 'b sequence = | Atom of 'b | Compound of 'b sequence*'b sequence
-
-
-(*** The following functions give more abstract methods to access
-     the data of a proof ***)
-
-(* This function gives the position of the focus if the proof is
-   focused, [None] otherwise *)
-let get_focus pr =
-  match pr.focus with
-  | [] -> None
-  | pos::_ -> Some pos
-
-(* The following function gives the content of the root *)
-let get_root pr =
-  pr.root
-
-(*** The following functions are somewhat unsafe, they are meant to 
-     be used by other functions later. They shouldn't be declared in
-     the .mli ***)
-
-
-(* This function performs a focusing on a given position
-   with no safety check nor caring of undos *)
-let unsafe_focus pr pos =
-  pr.focus <- pos::pr.focus
-
-(* This function unfocuses the proof [pr] with no safety
-   check nor caring of undos *)
-let unsafe_unfocus pr =
-  pr.focus <- List.tl pr.focus
-
-
-
-
-
-(*** The following functions define the basic safety mechanism of the
-     proof system, they may be unsafe if not used carefully. There is
-     currently no reason to export them in the .mli ***)
-
-let do_packed_mutation =
-  let scoped_mutate = 
-    { bind_mutation = fun mtn -> Subproof.mutate mtn.pt mtn.sp }
-  in
-  fun pck ->
-    unpack_mutation pck scoped_mutate
-
-
-(* This function interpetes (and execute) a single [undo_action] *)
-let execute_undo_action = function
-(*  | MutateBack(pt, sp) -> Subproof.mutate pt sp *)
-  | MutateBack pck -> do_packed_mutation pck
-  | Unfocus pr -> unsafe_unfocus pr
-  | Focus(pr, pt) -> unsafe_focus pr pt
-(*  | MutateRootBack(pt, sp) -> Subproof.mutate pt sp *)
-				
-
-(* This function interpetes a list of undo action, starting with
-   the one on the head. *)
-let execute_undo_sequence l =
-  List.iter execute_undo_action l
-
-(* This function gives the rollback procedure on unsuccessful commands .
-   tr is the current transaction. *)
-let rollback tr =
-  Transactional_stack.rollback execute_undo_sequence tr
-
-
-
-
-
-(* exception which represent a failure in a command *)
-exception Failure of Pp.std_ppcmds
-
-(* function to raise a failure less verbosely *)
-let fail msg = raise (Failure msg)
-
-
-
-(*** The functions that come below are meant to be used as 
-     atomic transformations, they raise [Failure] when they fail
-     and they push an [undo_action] to revert themselves.
-     They are still internal actions. *)
-
-(* This function performs sound mutation at a given position.
-   That is a mutation which stores an undo_action into the 
-   transaction [tr] *)
-let mutate pt sp tr =
-  push (MutateBack (pack_mutation {sp=sp;pt=pt})) tr;
-  Subproof.mutate pt sp
-
-(* arnaud:
-let mutate_root pt sp tr = 
-  push (MutateRootBack ( pt , Subproof.get pt)) tr;
-  Subproof.mutate pt sp *)
-
-(* This function focuses the proof [pr] at position [pt] and 
-   pushes an [undo_action] into the transaction [tr]. *)
-let focus pt pr tr =
-  push (Unfocus pr) tr;
-  unsafe_focus pr pt
-
-(* This function unfocuses the proof [pr], fails if 
-   [pr] is not focused (i.e. it shows its root). It
-   pushed an [undo_action] into the transaction [tr] *)
-let unfocus pr tr =
-  match pr.focus with
-  | [] -> fail (Pp.str "This proof is not focused")
-  | pt::_ -> push (Focus (pr,pt)) tr; unsafe_unfocus pr
-
-
-(*** The following function are composed transformations ***)
-
-(* This pair of functions tries percolate the resolved subgoal as much
-   as possible. It unfocuses the proof as much as needed so that it
-   is not focused on a resolved proof *)
-(* only [resolve] is meant to be used later on *)
-(* [deep_resolve] takes care of the non-root cases *)
-(* arnaud: rajouter les instanciations de métavariables *)
-let resolve =
-  (* This function unfocuses a proof until it is totally unfocused or
-     is focused on a non-resolved subproof *)
-  let rec unfocus_until_sound pr tr = 
-    match get_focus pr with
-    | None -> ()
-    | Some pt -> if Subproof.is_resolved (Subproof.get pt) then
-	           (unfocus pr tr;
-                    unfocus_until_sound pr tr)
-                 else 
-                   ()  
-  in
-  let resolve_iterator_fun tr pt =
-    try 
-      let res = Subproof.resolve (Subproof.get pt) in
-      mutate pt res tr
-    with Subproof.Unresolved ->
-      ()
-  in
-  let resolve_iterator tr = 
-    { Subproof.iterator = fun pt -> resolve_iterator_fun tr pt }
-  in
-  fun pr tr ->
-    Subproof.percolate (resolve_iterator tr) (get_root pr);
-    unfocus_until_sound pr tr
-
-
-(*** mechanism functions for sequences ***)
-let rec iter f seq =
-  match seq with
-  | Atom a -> f a
-  | Compound (lft,rgt) -> (iter f lft);(iter f rgt)
-
-(*** The following function takes a transformation and make it into 
-     a command ***)
-
-let do_command actions pr = 
-  let tr = start_transaction pr.undo_stack in
-  try 
-   iter (fun action -> action pr tr; resolve pr tr) actions;
-   commit tr
-  with e -> (* traitement particulier de Failure ? *)
-    rollback tr;
-    raise e
-  
-
-(*** The functions below are actually commands that can be used,
-     They cannot be used as a part of a compound transformation ***)
-
-(* This function gives the semantics of the "undo" command.
-   [pr] is the current proof *)
-let undo pr = 
-  Transactional_stack.pop execute_undo_sequence (pr.undo_stack)
-
-
-(*** The following functions define the tactic machinery. They 
-     transform a tactical expression into a sequence of actions. ***)
-(* apply_one *)
-(* apply_all *)
-(* apply_array *)
-(* apply_extend *)
diff --git a/proofs/proof.mli b/proofs/proof.mli
deleted file mode 100644
index 4e30d8dafa..0000000000
--- a/proofs/proof.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: proof.mli aspiwack $ *)
-
-(* This module implements the actual proof datatype. It enforces strong
-   invariants, and it is the only module that should access the module
-   Subproof.
-   Actually from outside the proofs/ subdirectory, this is the only module
-   that should be used directly. *)
-
-open Term
-
-(* Type of a proof *)
-type 'a proof
-
-(* Type of the proof transformations *)
-type 'a transformation
-
-(* exception which represent a failure in a command.
-   Opposed to anomalies and uncaught exceptions. *)
-exception Failure of Pp.std_ppcmds
-
-(* function to raise a failure less verbosely *)
-val fail : Pp.std_ppcmds -> 'a
-
-val do_command : 'a transformation -> 'a proof -> unit
-
-
diff --git a/proofs/subproof.ml b/proofs/subproof.ml
deleted file mode 100644
index 66c87ae298..0000000000
--- a/proofs/subproof.ml
+++ /dev/null
@@ -1,503 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: subproof.ml aspiwack $ *)
-
-(* arnaud: repasser sur cette description *)
-(* This module implements the primitive data type of the interactive
-   proof system : subproofs. A subproof is essentially a forest of 
-   subgoals. The subgoal on the leaves are said open (they are visible
-   by the user), the subgoal on the nodes are either partially resolved
-   (some of their children are leaves) or resolved (no more of their 
-   children are leaves). The node with no children are not considered 
-   leaves (they are the simplest form of resolved nodes).
-
-   Very little invariants are actually enforced in this module
-   only the basic functions for use in the more complete proof sytem
-   which starts in proof.ml . *)
-(* arnaud: rajouter quelque chose sur le fait qu'il y a peu de fonctions
-   mutables <= from .mli.
-           rechecker un peu la doc des fonctions 
-           rajouter les histoires de return value dans le .mli *)
-
-open Term
-open Goal
-
-
-(* We give a type ('a,+'b) pointer 'a is the type of the "return value"
-   of the proof 'b is a phantom argument stating the shape of the root
-   it can be any subtype of [< `Open | `Resolved | `Subproof ]
-   `Open is a single open goal, `Resolved is a node of the subproof
-   which knows its value `Subproof is a node which has partial information
-   on its value and opens a subproof *)
-
-(* The internal reprentation of the pointer type is 'a _pointer.
-   It is actually a type giving a way to access and mutate a subproof.
-   That is either a reference or a position in an array.
-   The reference is used to carry the mutable behavior down to the root *)
-type 'a _subproof =
-    (* An open goal *)
-    | Open of goal
-    (* A subproof whose content is resolved, holds its "return value" *)
-    | Resolved of 'a
-    (* A partially resolved subproof *)
-    | Subproof of 'a partially_resolved_subproof
-    (* A proof whose open goals have been permuted *)
-    | Permutation of constr _pointer array * 'a _subproof
-    (* A subproof which is routed because there has been a permutation *)
-    | Route of 'a _pointer
-
-(* A partially_resolved_subproof is that data of an array of subsubproofs
-   and a resolver function to close the subproof when every subproof above is
-   resolved *)
-(* In essence a partially resolved subproof could be an existential type:
-   {exists b. subproof b _subproof array; resolver : 'b array -> 'a}. There
-   is two main obstactle to this design choice :
-   1/ There is no existential type in OCaml
-   2/ There is sometimes need to know that internal subproofs
-      actually are constr _subproof, since tactics create such new goals.
-   The 1/ could be avoided by additional boxings and a bit of extra
-   verbosity, though it will probably impair a bit the legibility of
-   the code. The 2/ seems more of a problem thus the actual design 
-   choice is probably definite *)
-and  'a partially_resolved_subproof = 
-    { node : constr _subproof array;
-      resolver : constr array -> 'a 
-    }
-and 'a _pointer = 
-    | Root of 'a _subproof ref
-    | Node of 'a _subproof array*int
-
-type ('a,+'b) pointer = 'a _pointer
-
-(* This type gives *)
-type ('a,+'b) subproof = 'a _subproof
-
-(* Internal function which gives the subproof contained by the pointer *)
-let get = function
-  | Root r_sp -> !r_sp
-  | Node(sp_array,ix) -> sp_array.(ix)
-
-(* Internal function which gives the "real" subproof represented by a subproof.
-   it goes through the Route-s and Permutation-s to give the useful content
-   of the proof *)
-let rec simplify = function
-  | (Open _ as sp) 
-  | (Resolved _ as sp)
-  | (Subproof _ as sp)
-  | Permutation(_,sp) -> sp
-  | Route pt -> simplify (get pt)
-
-(* composition of the above two functions *)
-let get_simplify sp = simplify (get sp)
-
-let mutate pt sp =
-  match pt with
-  | Root r_nd -> r_nd := sp
-  | Node(sp_array,ix) -> sp_array.(ix) <- sp
-
-(* Type of the iterators (used with the iteration function) *)
-(* The need to define a new type is due the universal quantification
-   since not all the nodes have the same type case *)
-type iterator = { iterator : 'a.'a _pointer -> unit }
-
-(* The percolation function applies a function to all node pointer in the
-   subproof. It is guaranteed that an ancestor node will have the function
-   applied after all its descendants. *)
-(* This function may be a little ad hoc, it has been design mostly solely
-   for the interaction with [resolve] and [mutate] and being able to add 
-   undo information around the resolution. *)
-(* The extra seemingly unnecessary functions are here for typing issue,
-   the idea is that traverse_deep (: iterator -> constr _subproof -> unit) 
-   doesn't have the same type as traverse 
-   (: iterator -> 'a -> _subproof -> unit) *)
-let percolate =
-  let rec percolate_body traverse it pt =
-     match get pt with
-     | Resolved _ -> ()
-     | Open _ -> it.iterator pt
-     | Subproof prs 
-     | Permutation(_, Subproof prs) -> traverse it prs ; it.iterator pt
-     | Permutation(_, _) -> it.iterator pt
-     | Route pt -> percolate_body traverse it pt
-  in
-  let traverse_body traverse_deep it prs =
-    Array.iteri (fun i _ -> percolate_body traverse_deep it (Node(prs.node,i)))
-                                prs.node
-  in
-  let rec traverse_deep it prs = 
-    traverse_body traverse_deep it prs
-  in
-  let rec traverse it prs =
-    traverse_body traverse_deep it prs
-  in
-  fun it pt -> percolate_body traverse it pt
-
-
-(* This function is meant to turn a subproof that is actually
-   resolved into a Resolved Goal.
-   It can fail by raising the exception Unresolved when the current goal is
-   open or when not all it's immediate children are Resolved.
-   It is meant to be use later as the main tile of building a general
-   recursive resolve function which will take care of the additional
-   bureaucracy (such as the undo and such) *)
-exception Unresolved
-
-let rec resolve = 
-  let atomic_convert sp = (*converts a Resolved _ into a constr *)
-    match simplify sp with
-    | Resolved constr -> constr
-    | _ -> raise Unresolved
-  in 
-  let convert arr =
-    Array.map atomic_convert arr
-  in
-  fun sp ->
-    match simplify sp with
-    | Open _ -> raise Unresolved
-    | Resolved _ as sp -> sp
-    | Subproof psr -> let sub_constr = convert psr.node in
-	              Resolved (psr.resolver sub_constr)
-    | _ -> Util.anomaly "Subproof.resolve: failure of simplify"
-
-(* This function returns [true] if it's argument is resolved, and
-   [false] otherwise] *)
-let is_resolved sp =
-  match simplify sp with
-  | Resolved _ -> true
-  | _ -> false
-
-(* This function returns the array containing pointers to all the open 
-   subgoals of a given subproof pointer *)
-(* extra functions due to typing issue *)
-let opengoals =
-  let list_opengoals_node_body loga next cont pt = 
-      match get pt with
-      (* by construction a pointer containing an Open goal are
-	 always constr _pointer. If we omit the magic, then we
-         cannot express opengoals in all generality *)
-      | Open _ -> [(Obj.magic pt:constr _pointer)]
-      | Resolved _ -> next cont
-      | Subproof psr -> loga next cont psr.node 0
-      (* For the semantics to be correct here we need all the
-         open goals to be contained in subproofs from the permuted 
-         array all such open goal to be actually linked to the subproof. 
-         This invariant is not enforced by typing (unfortunately), but
-         should be kept correct as long as one does not do absurd things
-         with proofs *)
-      | Permutation (arr,_) ->let sp_arr = Array.map get arr in
-                              loga next cont sp_arr ((Array.length arr) - 1)
-      | Route _ -> Util.anomaly "Subproof.opengoals: abnormal Route node"
-  in
-  let rec list_opengoals_array return cont sp_arr ix =
-    if ix < 0 then
-      return cont
-    else
-      let next new_cont = list_opengoals_array return new_cont sp_arr ix in
-      list_opengoals_node_body list_opengoals_array next cont (Node(sp_arr,ix))
-  in
-  let list_opengoals_node pt =
-    list_opengoals_node_body list_opengoals_array (fun cont -> cont) [] pt
-  in
-  fun pt ->
-    Array.of_list (list_opengoals_node pt)
-
-(* This function returns the result of a resolved subproof *)
-let get_result sp = 
-  match simplify sp with
-  | Resolved res -> res
-  | _ -> Util.anomaly "Subproof.get_result: failure of simplify"
-
-(* This function returns the actual goal represented by an open 
-   goal subproof *)
-let get_goal sp =
-  match simplify sp with
-  | Open gl -> gl
-  | _ -> Util.anomaly "Subproof.get_goal: failure of simplify"
-
-(* Reorders the open goals of the given pointer, according to the 
-   permutation *)
-let reorder =
-  let copy pt = (* creates a new pointer towards the same content *)
-    Root (ref (get pt))
-  in
-  let route pt_route pt_content =  (* mutates [pt_route] into a route to *)
-                                   (* [pt_content] *)
-    mutate pt_route (Route (pt_content))
-  in
-  fun perm pt ->
-    let og = opengoals pt in
-    let copied_og = Array.map copy og in
-    Array.iteri (fun i pt -> route pt copied_og.(i)) og;
-    let reordered_og = Permutation.permute perm copied_og in
-    mutate pt (Permutation(reordered_og, get pt))
-
-
-(* The following function creates a new subproof *)
-let open_subproof ?(subgoals=[||]) ~resolver =
-   Subproof { node = Array.map (fun g -> Open g) subgoals;
-              resolver = resolver }
-
-(* The following function creates a new pointer with a new subproof in it *)
-let start_subproof ?(subgoals=[||]) ~resolver =
-  Root (ref (open_subproof ~subgoals:subgoals ~resolver:resolver))
-
-
-
-(*arnaud:
-  let list_opengoals_body log_deep traverse return cont sp_arr ix =
-    let next cont = traverse cont sp_arr (ix-1) in
-    if ix < 0 then
-      return cont
-    else
-      match get sp_arr.(ix) with
-      | Open _ -> [Node(sp_arr,ix)]
-      | Resolved _ -> next cont
-      | Subproof psr -> log_deep next cont psr.node 0
-      (* For the semantics to be correct here we need all the
-         open goals to be contained in subproofs from the permuted 
-         array all such open goal to be actually linked to the subproof. 
-         This invariant is not enforced by typing (unfortunately), but
-         should be kept correct as long as one does not do absurd things
-         with proofs *)
-      | Permutation (arr,_) -> log_deep next cont arr ((Array.length arr) - 1)
-      | Route (_, _) -> anomaly "Subproof.opengoals: abnormal Route node"
-  in
-  let rec deep_list_opengoals return cont sp_arr ix =
-    list_opengoals_body deep_list_opengoals (deep_list_opengoals return)
-  in
-  let rec list_opengoals cont sp_arr ix =
-    list_opengoals_body deep_list_opengoals 
-                        traverse 
-                        (fun cont -> cont)
-  in
-  function 
-  | Root r_sp -> match !sp with
-                 | Subproof
-  | Node(sp_arr, ix) -> Array.of_list (list_opengoals [] sp ix) *)
-
-
-
-(* arnaud:
-
-(* The type 'a subproof represents the type of subproofs "returning"
-   an object of type 'a. *)
-(* In essence the type 'a proof_node should be an existential type
-   of the shape 'a proof_node = exists 'b.{ node : 'b subproof array;
-                                            fallback : 'b array -> 'a}
-   However, this extra layer of abstraction is hardly needed in practice
-   and since existential types are not primitive in OCaml (though 
-   somewhat encodable through some additional boxing) it wasn't worth
-   the extra complication.
-   The type of nodes is specialized (in constr subproof) to allow clearer
-   and more efficient code *)
-(* arnaud: rather old style
-type 'a proof_node = 
-    { node : constr subproof array;
-      callback : constr array -> 'a
-    }
-and 'a subproof = 
-    [ `Open of goal
-    | `Resolved of 'a
-    | `Subproof of 'a proof_node ] *)
-
-(* arnaud: old style
-    | OpenGoal of goal
-    | PartiallyResolvedGoal of 'a proof_node
-    | ResolvedGoal of 'a *)
-
-(* This type replaces an existential typing *)
-type 'a deep_node = 
-    | Root of 'a proof_node
-    | Node of constr proof_node
-
-(* The type to identify a specific node or leaf of a subproof *)
-type 'a position = { handle:'a deep_node;
-		     index:int}
-
-(* This function is meant to turn a `Subproof that is actually
-   resolved into a Resolved Goal.
-   It can fail by raising the exception Unresolved when the current goal is
-   open or when not all it's immediate children are Resolved.
-   It is meant to be use later as the main tile of building a general
-   recursive resolve function which will take care of the additional
-   bureaucracy (such as the undo and such) *)
-exception Unresolved
-
-let resolve = 
-  let convert arr =(* converts an array of `Resolved into an array of constr *)
-    Array.map 
-      (function | `Resolved constr -> constr
-                | _ -> raise Unresolved) arr
-  in
-
-  function | `Subproof sp -> 
-                    let sub_constr = convert sp.node in
-		    `Resolved (sp.callback sub_constr)
-           | (`Resolved _) as rg -> rg
-	   | `Open _ -> raise Unresolved
-
-
-(* arnaud: virer ce truc inutile, comprendre une solution à base de dictionaire
-   ou filtre éventuellement
-(* The following function switches two proof_node (identified by their indices)
-   of a given subproof. *)
-(* spiwack: I don't really know if it will prove a useful function. It has
-     the very big default that it does not scale up very well. Indeed,
-     it does not allow switching proofs that are in different subtrees,
-     which is what the user may wants to do, but can't be done at this 
-     level.
-     It is  not currently in the .mli would require a bit of thinking
-     to get the right version. *)
-(* arnaud : cette fonction mute le callback, faire attention à bien faire
-   l'undo proprement *)
-let switch =
-  let array_switch i j arr =
-    let buf_i = arr.(i) in
-    let buf_j = arr.(j) in (* not necessary, could be replaced by a 
-                              length check *)
-    arr.(i) <- buf_j; arr.(j) <- buf_i
-  in
-
-  fun i j sp ->
-    array_switch i j sp.node;
-    sp.callback <- (fun arr -> array_switch i j arr; 
-		                                (* the array that is switched
-						   back is a newly born array
-						   no risk of corrupting data
-						   by modifying it *)
-		               sp.callback arr)    
-*)
-
-(* The following function creates a new subproof *)
-let open_proof ?(subgoals=[||]) ~callback =
-  `Subproof { node = Array.map (fun g -> `Open g) subgoals;
-              callback = callback }
-
-
-(* This function returns the subproof pointed by the position [pos] *)
-let of_position pos =
-  match pos.handle with
-  | Root sp -> sp.node.(pos.index)
-  | Node sp -> sp.node.(pos.index)
-
-(* The following function returns the position of the nth opened subgoal.
-   Raises not_found if there is not that many subgoals. 
-   It acts either on a subproof of the form `Subproof _ or on a position *)
-let rec nth_subgoal = 
-  (* [nth_subgoal] basically does a depth-first search of the proof
-     subtree.
-     The implementation of the function is a bit tricky, due to typing
-     issue (again the absence of existential types makes things a bit 
-     more tedious (yet less than if we used an encoding)).
-     The main subfunction is the function [abstract_traverse] which
-     takes as arguments the recursive calls. The argument [traverse]
-     is the function that is called when checking the next goal of
-     a node (and is abstracted inside the function [next]). The
-     argument [deep_traverse] is called when going one node deeper
-     in the subproof tree. The [return] argument is used when
-     backtracking to a parent node. [n] is the number of open goals
-     to find before we find the goal we look for: it is decreased by
-     [1] each time we find a open subgoal, except if it is already [1]
-     in which case we terminate the algorithm on the first open subgoal
-     we find. [ix] represent the current index in the array of the node.
-     [pn] is the current subproof node we are currently traversing.
-     Finally [box] is a function giving a way to coerce the current
-     [proof_node] (namely [pn]) into the appropriate ['a deep_node]
-     where ['a] correspond to the return type of the root of the proof
-     we consider.
-     This function being defined we can define the two main subroutines
-     [deep_traverse] is basically [abstract_traverse deep_traverse 
-     deep_traverse]. It performs the search inside any non-root node
-     since all of them are of type [constr proof_node] it is simply
-     self-recursive.
-     The function [traverse] takes care of the search on the root node.
-     That is, basically, [abstract_traverse traverse deep_traverse].
-     Because of the heterogeneous typing of the root and deep nodes
-     it calls deep_traverse when it goes deeper in the tree *)
-  let abstract_traverse traverse deep_traverse return n ix pn box =
-    if ix < Array.length pn.node then
-      let next n = traverse n (ix+1) pn in
-      match pn.node.(ix) with
-      | `Open _ when n = 1     -> {handle=box pn;index=ix}
-      | `Open _                -> next (n-1)
-      | `Resolved _            -> next n
-      | `Subproof rpn -> deep_traverse next n 0 rpn
-    else
-      return n
-  in
-  let node u = Node u in
-  let rec deep_traverse return n ix pn =
-    abstract_traverse (deep_traverse return) deep_traverse return n ix pn node
-  in
-  let root u = Root u in
-  let rec traverse n ix pn =
-    abstract_traverse traverse
-                      deep_traverse
-                      (fun _ -> raise Not_found)
-                      n
-                      ix
-                      pn root
-  in
-  fun n sp ->
-    if n < 1 then
-      invalid_arg "Subproof.nth_subgoal: no non-positive open goal"
-    else
-      match sp with
-      | `Subproof pn -> traverse n 0 pn
-      | `Position pos ->  
-	  match of_position pos with
-	  | `Subproof pn     -> deep_traverse (fun _ -> raise Not_found) n 0 pn
-	  | `Open _ when n=1 -> pos
-	  | `Open _          -> raise Not_found
-	  | `Resolved _      -> raise Not_found
-
-(* arnaud: to clean  
-  let abstract_traverse traverse n parents ix sp dsp =
-    if ix < Array.length sp.node then
-      match sp.node.(ix) with
-      | `Open _ when n = 1     -> {handle=dsp;index=ix}
-      | `Open _                -> traverse (n-1) parents (ix+1) dsp
-      | `Resolved _            -> traverse n parents (ix+1) dsp
-      | `Subproof rsp -> traverse n ((dsp, ix)::parents)
-	                                      0 (Node rsp)
-    else
-      match parents with
-      | (dsp, jx)::q -> traverse n q (jx+1) dsp
-      | [] -> raise Not_found
-  in
-  let rec traverse n parents ix = function
-    | (Root sp) as dsp -> abstract_traverse traverse n parents ix sp dsp
-    | (Node sp) as dsp -> abstract_traverse traverse n parents ix sp dsp
-  in
-  fun n (`Subproof sp )->
-    if n < 1 then
-      invalid_arg "Subproof.nth_subgoal: no non-positive open goal"
-    else
-      traverse n [] 0 (Root sp) *)
-
-
-(* This function changes the goal at a certain position *)
-let mutate pos new_content =
-  match pos.handle with
-  | Root sp -> sp.node.(pos.index) <- new_content
-  | Node sp -> sp.node.(pos.index) <- new_content
-
-
-(* This function iters a function on all the subproofs of a proof node,
-   except the node of the root *)
-let iter f pn =
-  let bpn = Node pn in
-  Array.iteri (fun i -> f { handle=bpn ; index=i}) pn.node
-
-(* This function iters a function on all the subproof of the root proof
-   node *)
-let root_iter f pn =
-  let bpn = Root pn in
-  Array.iteri (fun i -> f { handle=bpn ; index=i}) pn.node
-*)
diff --git a/proofs/subproof.mli b/proofs/subproof.mli
deleted file mode 100644
index edb9b23846..0000000000
--- a/proofs/subproof.mli
+++ /dev/null
@@ -1,180 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: subproof.mli aspiwack $ *)
-
-
-(* This module implements the primitive data type of the interractive
-   proof system : subproofs. A subproof is essentially a forest of 
-   subproof. The subproofs on the leaves are said open (they are visible
-   by the user), the subproofs on the nodes are either partially resolved
-   (some of their children are leaves) or resolved (no more of their 
-   children are leaves). The node with no children are not considered 
-   leaves (they are the simplest form of resolved nodes).
-
-   Very little invariants are actually enforced in this module
-   only the basic functions for use in the more complete proof sytem
-   which starts in proof.ml. *)
-
-(* The two main types subproof et pointer are, in essence, mutually 
-   recursive. Pointers have to be understood as references to subproofs.
-   But subproof, as containing mutable parts are not a persistent datatype.
-
-   The second parameter of the types subproof and pointer is a parameter
-   stating the shape of the proof. The different shapes are `Subproof,
-   `Open and `Resolved. `Open corresponds to a subproof containing a single
-   open goal. `Resolved corresponds to a subproof which is resolved.
-   `Subproof corresponds to a node in the tree, a partially resolved
-   subproof.
-
-   For the subproof type, this shape parameter should be seen as the
-   root of the proof. For a pointer, it represents the type of subproof
-   it can hold.*)
-
-(* The following invariants are enforced:
-   - it is not possible to build a (t,[`Open]) subproof where
-     t is not Term.constr.
-   - all the function are pure except mutate and reorder
-
-   Some invariants are not enforced:
-   - it seemed too inefficient to try and keep the internal structure
-     sound. The system handling the reordering of the open goals is
-     the cause of it. Thus it is not as transparent as it might appear
-     by reading the API. It is advised to avoid mutating a pointer unless 
-     it has no open goal on the leaves or you are reversing an earlier
-     mutation. If you do not use the API with care, you might mess up the
-     internal structure, and get rather unexpected results.
-   (* spiwack: some might argue the choice of separating proof and subproof
-      in to different files, since the API of subproof is not really
-      independant from that of proof. However, I considered it interesting
-      since it allowed a better separation of matters and, hopefully,
-      much clearer code*)
-*)
-open Term
-
-type ('a,+'b) subproof
-type ('a,+'b) pointer
-
-(* Gives the subproof held by a pointer *)
-val get : ('a,'b) pointer -> ('a,'b) subproof
-
-(* Changes the subproof held by a pointer *)
-val mutate : ('a,'b) pointer -> ('a,'b) subproof -> unit
-
-
-(* Type of functions to  be used with [percolate] *)
-type iterator =
-    { iterator : 'a.('a,[ `Subproof | `Open | `Resolved ]) pointer -> unit }
-
-(* The percolation function applies a function to all node pointer in the
-   subproof. It is guaranteed that an ancestor node will have the function
-   applied after all its descendants. *)
-(* This function may be a little ad hoc, it has been design mostly solely
-   for the interaction with [resolve] and [mutate] and being able to add 
-   undo information around the resolution. *)
-val percolate : iterator -> ('a,'b)  pointer -> unit
-
-(* This function is meant to turn a subproof that is actually
-   resolved into a Resolved Goal.
-   It can fail by raising the exception Unresolved when the current goal is
-   open or when not all it's immediate children are Resolved.
-   It is meant to be use later as the main tile of building a general
-   recursive resolve function which will take care of the additional
-   bureaucracy (such as the undo and such) *)
-exception Unresolved
-val resolve : ('a,'b) subproof -> ('a, [> `Resolved]) subproof
-
-(* This function returns [true] if it's argument is resolved, and
-   [false] otherwise] *)
-val is_resolved : ('a,'b) subproof -> bool
-
-(* This function returns the array containing pointers to all the open 
-   subgoals of a given subproof pointer *)
-val opengoals : ('a,'b) pointer -> (constr, [> `Open]) pointer array
-
-(* This function returns the result of a resolved subproof *)
-val get_result : ('a,[< `Result ]) subproof -> 'a
-
-(* This function returns the actual goal represented by an open 
-   goal subproof *)
-val get_goal : (constr, [< `Open ]) subproof -> Goal.goal
-
-(* Reorders the open goals of the given pointer, according to the 
-   permutation *)
-val reorder : Permutation.permutation -> ('a, 'b) pointer -> unit
-
-(* The following function creates a new subproof *)
-val open_subproof : ?subgoals:Goal.goal array -> 
-                    resolver:(constr array -> 'a) ->
-                    ('a, [>`Subproof]) subproof
-
-(* The following function creates a new pointer with a new subproof in it *)
-val start_subproof : ?subgoals:Goal.goal array -> 
-                    resolver:(constr array -> 'a) ->
-                    ('a, [>`Subproof]) pointer
-
-
-(* arnaud:
-open Term
-open Goal
-
-(* A type which corresponds to the `Subproof case of subproofs *)
-type 'a proof_node
-
-(* The type 'a subproof represents the type of subproof "returning"
-   an object of type 'a. *)
-type 'a subproof = 
-    [ `Open of goal
-    | `Resolved of 'a
-    | `Subproof of 'a proof_node ]
-
-
-(* The type to identify a specific node or leaf of a subproof.
-   Be careful, it indicates a physical position. It can give
-   unexpected results if it is used after a proof has mutated *)
-type 'a position
-
-
-(* This function is meant to turn a PartiallyResolvedGoal that is actually
-   resolved into a Resolved Goal.
-   It can fail by raising the exception Unresolved when the current goal is
-   open or when not all it's immediate children are Resolved.
-   It is meant to be use later as the main tile of building a general
-   recursive resolve function which will take care of the additional
-   bureaucracy (such as the undo and such).
-   It is a pure function. *)
-exception Unresolved
-
-val resolve : [< 'a subproof ] -> [> `Resolved of 'a ]
-
-
-(* The following function creates a new subproof *)
-val open_proof : ?subgoals:goal array -> 
-                 callback:(constr array -> 'a) -> 
-               [ `Subproof of 'a proof_node ]
-
-(* The following function returns the position of the nth opened subgoal.
-   Raises not_found if there is not that many subgoals. *)
-val nth_subgoal : int -> [< `Subproof of 'a proof_node 
-                          | `Position of 'a position ] -> 'a position
-  
-(* This function changes the goal at a certain position *)
-val mutate : 'a position -> constr subproof -> unit
-
-(* This function returns the subproof pointed by the position [pos] *)
-val of_position : 'a position -> constr subproof
-
-(* This function iters a function on all the subproofs of a proof node,
-   except the node of the root *)
-val iter : ('a position -> constr subproof ->unit) -> constr proof_node -> unit
-
-
-(* This function iters a function on all the subproof of the root proof
-   node *)
-val root_iter : ('a position -> constr subproof->unit) -> 'a proof_node -> unit
-*)
diff --git a/proofs/transactional_stack.ml b/proofs/transactional_stack.ml
deleted file mode 100644
index 74b95e6c0b..0000000000
--- a/proofs/transactional_stack.ml
+++ /dev/null
@@ -1,127 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: transactional_stack.ml aspiwack $ *)
-
-(* This module implements a datastructure that is not strictly bound
-   to the interractive proof system. But currently it is used as an 
-   undo stack for the proof system thus it is present in the proofs
-   directory *)
-
-(* The datastructure implemented in this module is a transactional 
-   stack, i.e. a stack of transactions. A transaction is a list of 
-   sequential actions (the type of action is 'a (independent from the
-   implementation)) which are pushed one after another. When the 
-   transaction is finished, it is then committed to the stack.
-   Other basic operations include rollback (cancelling the current 
-   transaction), pop (consuming the last committed transaction).
-
-   In the case of an undo stack, here is the spirit of how it is used:
-   when the user types a command, first, a transaction is started, 
-   then for each atomic action executed by the command, an action
-   to revert it is pushed in the transaction.
-   If the command fails, then the transaction is rolled back
-   If the command succeeds, then the transaction is committed.
-
-   In case an undo happen, the last transaction is popped, and 
-   all of its action are undone. 
-
-   The rollback and pop operations are implemented in the continuation
-   passing style, because they are meant to be easily lifted *)
-
-
-(* The internal representation of a transactional stack is essentially 
-   a stack of lists, stack being represented as pointers to a list *)
-
-module Stack : (sig
-		  type 'a stack
-		  val create : unit -> 'a stack
-		  val push : 'a -> 'a stack -> unit
-		  val pop : 'a stack -> 'a
-		  val snapshot : 'a stack -> 'a list
-		  val lock : 'a stack -> unit
-		  val unlock : 'a stack -> unit
-		  val locked : 'a stack -> bool
-		end) = 
-  (* arnaud: the type of Stack has not been abstracted yet
-             out of sheer lazyness *)
-  (* stacks are basically a list without the possibility of map/fold.
-     they contain an extra lock that is hear for pure safety reasons.
-     trying to push or pop to a locked stack raises an anomaly *)
-  struct
-    type 'a stack = {mutable stack : 'a list ; mutable locked : bool }
-
-    let create () = { stack = [] ; locked = false}
-    let push a st = 
-      if st.locked then
-	Util.anomaly 
-	  "Transactional_stack.Stack.push: nsafe use of a stack"
-      else
-	st.stack <- a::st.stack
-	
-    let pop st = 
-      if st.locked then
-	Util.anomaly 
-	  "Transactional_stack.Stack.pop: unsafe use of a stack"
-      else
-      match st.stack with
-      | [] -> raise Not_found
-      | a::r -> st.stack <- r ; a
-    let snapshot st = st.stack
-
-    let lock st = st.locked <- true
-    let unlock st = st.locked <- false
-
-    let locked st = st.locked
-  end
-
-
-type 'a transactional_stack = 'a list Stack.stack
-type 'a transaction = { transaction: 'a Stack.stack;
-		        t_stack: 'a transactional_stack }
-
-
-(* General note : freezing/unfreezing of transactional stacks and
-   death of transactions both use the lock mechanism of stacks.
-   In some case it imposes naturally a restriction, in other cases
-   we also need to check the lock manually. *)
-
-
-let start_transaction t_st = 
-  if Stack.locked t_st then
-    Util.anomaly 
-      "Transitional_stack.start_transaction: cannot start a transaction from a frozen stack"
-  else
-    Stack.lock t_st;
-    { transaction = Stack.create () ;
-      t_stack = t_st }
-
-let commit tr =
-  if Stack.locked tr.transaction then
-    Util.anomaly "Transitional_stack.commit: cannot commit a dead transaction"
-  else
-    Stack.unlock tr.t_stack;
-    Stack.push (Stack.snapshot tr.transaction) tr.t_stack;
-    Stack.lock tr.transaction
-			 
-let rollback cont tr =
-  if Stack.locked tr.transaction then
-    Util.anomaly 
-      "Transitional_stack.rollback: cannot rollback a dead transaction"
-  else
-    Stack.unlock tr.t_stack;
-    Stack.lock tr.transaction;
-    cont (Stack.snapshot tr.transaction)
-
-
-
-let push action tr = Stack.push action tr.transaction
-
-
-let pop cont t_st =
-  cont (Stack.pop t_st)
diff --git a/proofs/transactional_stack.mli b/proofs/transactional_stack.mli
deleted file mode 100644
index 9792641878..0000000000
--- a/proofs/transactional_stack.mli
+++ /dev/null
@@ -1,61 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: transactional_stack.mli aspiwack $ *)
-
-(* The datastructure implemented in this module is a transactional 
-   stack, i.e. a stack of transactions. A transaction is a list of 
-   sequential actions (the type of action is 'a (independent from the
-   implementation)) which are pushed one after another. When the 
-   transaction is finished, it is then committed to the stack.
-   Other basic operations include rollback (cancelling the current 
-   transaction), pop (consuming the last committed transaction).
-
-   In the case of an undo stack, here is the spirit of how it is used:
-   when the user types a command, first, a transaction is started, 
-   then for each atomic action executed by the command, an action
-   to revert it is pushed in the transaction.
-   If the command fails, then the transaction is rolled back
-   If the command succeeds, then the transaction is committed.
-
-   In case an undo happen, the last transaction is popped, and 
-   all of its action are undone. 
-
-   The rollback and pop operations are implemented in the continuation
-   passing style, because they are meant to be easily lifted *)
-
-type 'a transactional_stack
- (** The type of transactional stacks *)
-type 'a transaction
- (** The type of handlers to transactions (they are implicitely associated 
-     to a stack) *)
-
-val start_transaction :  'a transactional_stack -> 'a transaction
- (** [start_transaction st] starts a new transaction bound to the
-     stack [st]. In addition [st] is frozen until the new transaction
-     ends. (While [st] is frozen you can't open any other transaction,
-     nor pop the last transaction, it would raise an anomaly) *)
-
-val commit : 'a transaction -> unit
- (** [commit tr] commits the transaction [tr] to the stack it is bound
-     to. The transaction is then killed (you can't use it anymore, trying
-     to do so raises an anomaly) and the associated stack is released. *)
-			 
-val rollback : ('a list -> 'b) -> 'a transaction -> 'b
- (** [rollback cont tr] rolls the transaction back, by executing
-     cont on the list representing the transaction. The transaction 
-     is then killed and the associated stack released. *)
-
-
-val push : 'a -> 'a transaction -> unit
- (** [push a tr] pushes the action [a] onto the transaction [tr] *)
-
-
-val pop  : ('a list -> 'b) -> 'a transactional_stack -> 'b
- (** [pop cont st] pops the last transaction out of [st] 
-     and applies [cont] to the list representing it *)