Quelques structures de donnée plus les modules principaux (et

parfaitement en cours) de la nouvelle machinerie de preuves.



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

12 files changed, 1435 insertions, 0 deletions

diff --git a/lib/biassoc.ml b/lib/biassoc.ml
new file mode 100644
index 0000000000..2c8fc32167
--- /dev/null
+++ b/lib/biassoc.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..45426d1bc3
--- /dev/null
+++ b/lib/biassoc.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..2172373170
--- /dev/null
+++ b/proofs/goal.ml
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..829f4f23cb
--- /dev/null
+++ b/proofs/goal.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..8477f14960
--- /dev/null
+++ b/proofs/permutation.ml
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..9063f58159
--- /dev/null
+++ b/proofs/permutation.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..c0bfc6f755
--- /dev/null
+++ b/proofs/proof.ml
@@ -0,0 +1,259 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..4e30d8dafa
--- /dev/null
+++ b/proofs/proof.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..66c87ae298
--- /dev/null
+++ b/proofs/subproof.ml
@@ -0,0 +1,503 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..edb9b23846
--- /dev/null
+++ b/proofs/subproof.mli
@@ -0,0 +1,180 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..74b95e6c0b
--- /dev/null
+++ b/proofs/transactional_stack.ml
@@ -0,0 +1,127 @@
+(************************************************************************)
+(*  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
new file mode 100644
index 0000000000..9792641878
--- /dev/null
+++ b/proofs/transactional_stack.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  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 *)