Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

22 files changed, 2330 insertions, 0 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
new file mode 100644
index 00000000..bbf722db
--- /dev/null
+++ b/contrib/subtac/FixSub.v
@@ -0,0 +1,22 @@
+Require Import Wf.
+
+Section Well_founded.
+Variable A : Set.
+Variable R : A -> A -> Prop.
+Hypothesis Rwf : well_founded R.
+
+Section FixPoint.
+
+Variable P : A -> Set.
+
+Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
+ 
+Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
+   F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
+   (Acc_inv r (proj1_sig y) (proj2_sig y))).
+
+Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
+
+End FixPoint.
+
+End Well_founded.
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
new file mode 100644
index 00000000..9acb10ae
--- /dev/null
+++ b/contrib/subtac/Utils.v
@@ -0,0 +1,34 @@
+Set Implicit Arguments.
+
+Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
+intros.
+induction t.
+exact x.
+Defined.
+
+Check proj1_sig.
+Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
+  (t : sig P), P (proj1_sig t).
+Proof.
+intros.
+induction t.
+ simpl ; auto.
+Qed.
+
+Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
+ P (ex_pi1 t).
+intros A P.
+dependent inversion t.
+simpl.
+exact p.
+Defined.
+
+Notation "'forall' { x : A | P } , Q" :=
+  (forall x:{x:A|P}, Q)
+  (at level 200, x ident, right associativity).
+
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml
new file mode 100644
index 00000000..236b0ea5
--- /dev/null
+++ b/contrib/subtac/context.ml
@@ -0,0 +1,35 @@
+open Term
+open Names
+
+type t = rel_declaration list (* name, optional coq interp, algorithmic type *)
+
+let assoc n t = 
+  let _, term, typ = List.find (fun (x, _, _) -> x = n) t in
+    term, typ
+
+let assoc_and_index x l =
+  let rec aux i = function
+      (y, term, typ) :: tl -> if x = y then i, term, typ else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
+
+let id_of_name = function
+    Name id -> id
+  | Anonymous -> raise (Invalid_argument "id_of_name")
+(*
+
+let subst_ctx ctx c = 
+  let rec aux ((ctx, n, c) as acc) = function
+      (name, None, typ) :: tl -> 
+	aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), 
+	     pred n, c) tl
+    | (name, Some term, typ) :: tl ->
+	let t' = Term.substnl [term] n c in
+	  aux (ctx, n, t') tl
+    | [] -> acc
+  in 
+  let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in 
+    (x, rel_to_vars x z)
+*)
+
+let subst_env env c = (env, c)
diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli
new file mode 100644
index 00000000..671d6f36
--- /dev/null
+++ b/contrib/subtac/context.mli
@@ -0,0 +1,5 @@
+type t = Term.rel_declaration list
+val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c
+val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c
+val id_of_name : Names.name -> Names.identifier
+val subst_env : 'a -> 'b -> 'a * 'b
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
new file mode 100644
index 00000000..5703c0ef
--- /dev/null
+++ b/contrib/subtac/eterm.ml
@@ -0,0 +1,168 @@
+(**
+   - Get types of existentials ;
+   - Flatten dependency tree (prefix order) ;
+   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+   - Apply term prefixed by quantification on "existentials".
+*)
+
+open Term
+open Names
+open Evd
+open List
+open Pp
+open Util
+
+let reverse_array arr = 
+  Array.of_list (List.rev (Array.to_list arr))
+    
+let trace s = 
+  if !Options.debug then msgnl s
+  else ()
+
+(** Utilities to find indices in lists *)
+let list_index x l =
+  let rec aux i = function
+      k :: tl -> if k = x then i else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
+
+let list_assoc_index x l =
+  let rec aux i = function
+      (k, _, v) :: tl -> if k = x then i else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
+
+(** Substitute evar references in t using De Bruijn indices, 
+  where n binders were passed through. *)
+let subst_evars evs n t = 
+  let evar_info id = 
+    let rec aux i = function
+	(k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl
+      | [] -> raise Not_found
+    in 
+    let (idx, hyps, v) = aux 0 evs in
+      n + idx + 1, hyps
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Evar (k, args) ->
+	(try 
+	   let index, hyps = evar_info k in
+	     trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+		    int (List.length hyps) ++ str " hypotheses");
+
+	   let ex = mkRel (index + depth) in
+	     (* Evar arguments are created in inverse order, 
+		and we must not apply to defined ones (i.e. LetIn's)
+	     *)
+	   let args =
+	     let rec aux hyps args acc =
+	       match hyps, args with
+		   ((_, None, _) :: tlh), (c :: tla) -> 
+		     aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+		 | ((_, Some _, _) :: tlh), (_ :: tla) ->
+		     aux tlh tla acc
+		 | [], [] -> acc
+		 | _, _ -> failwith "subst_evars: invalid argument"
+	     in aux hyps (Array.to_list args) [] 
+	   in
+	     mkApp (ex, Array.of_list args)
+	 with Not_found -> 
+	   anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found"))
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+      
+(** Substitute variable references in t using De Bruijn indices, 
+  where n binders were passed through. *)
+let subst_vars acc n t = 
+  let var_index id = 
+    let idx = list_index id acc in
+      idx + 1
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+
+(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
+  to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+  Changes evars and hypothesis references to De Bruijn indices.
+*)
+let etype_of_evar evs ev hyps =
+  let rec aux acc n = function
+      (id, copt, t) :: tl ->
+	let t' = subst_evars evs n t in
+	let t'' = subst_vars acc 0 t' in
+ 	  mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
+    | [] ->
+	let t' = subst_evars evs n ev.evar_concl in
+	  subst_vars acc 0 t'	
+  in aux [] 0 (rev hyps)
+
+
+open Tacticals
+    
+let eterm_term evm t tycon = 
+  (* 'Serialize' the evars, we assume that the types of the existentials
+     refer to previous existentials in the list only *)
+  let evl = to_list evm in
+  let evts = 
+    (* Remove existential variables in types and build the corresponding products *)
+    fold_right 
+      (fun (id, ev) l ->
+	 let hyps = Environ.named_context_of_val ev.evar_hyps in
+	 let y' = (id, hyps, etype_of_evar l ev hyps) in
+	   y' :: l) 
+      evl []
+  in 
+  let t' = (* Substitute evar refs in the term by De Bruijn indices *)
+    subst_evars evts 0 t 
+  in
+  let evar_names = 
+    List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts
+  in
+  let evar_bl =
+    List.map (fun (id, c) -> Name id, None, c) evar_names
+  in
+  let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
+    (* Generalize over the existential variables *)
+  let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl 
+  and tycon = option_app 
+		(fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
+  in
+  let _declare_evar (id, c) =
+    let id = id_of_string ("Evar" ^ string_of_int id) in
+      ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
+					  Decl_kinds.IsAssumption Decl_kinds.Definitional))
+  in
+  let _declare_assert acc (id, c) =
+    let id = id_of_string ("Evar" ^ string_of_int id) in
+      tclTHEN acc (Tactics.assert_tac false (Name id) c)
+  in
+    trace (str "Term given to eterm" ++ spc () ++
+	   Termops.print_constr_env (Global.env ()) t);
+    trace (str "Term constructed in eterm" ++ spc () ++
+	   Termops.print_constr_env (Global.env ()) t'');
+    ignore(option_app 
+	     (fun typ ->
+		trace (str "Type :" ++ spc () ++
+		       Termops.print_constr_env (Global.env ()) typ))
+	     tycon);
+    t'', tycon, evar_names
+
+let mkMetas n = 
+  let rec aux i acc = 
+    if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
+    else acc
+  in aux n []
+
+let eterm evm t (tycon : types option) = 
+  let t, tycon, evs = eterm_term evm t tycon in
+    match tycon with
+	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) []
+      | None -> Tactics.apply_term t (mkMetas (List.length evs))
+     
+open Tacmach
+
+let etermtac (evm, t) = eterm evm t None
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
new file mode 100644
index 00000000..fbe2ac1d
--- /dev/null
+++ b/contrib/subtac/eterm.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: eterm.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+
+open Tacmach
+open Term
+open Evd
+open Names
+
+val mkMetas : int -> constr list
+
+val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
+
+val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4
new file mode 100644
index 00000000..d9dd42cd
--- /dev/null
+++ b/contrib/subtac/g_eterm.ml4
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: g_eterm.ml4 8654 2006-03-22 15:36:58Z msozeau $ *)
+
+open Eterm
+
+TACTIC EXTEND eterm
+  [ "eterm" ] -> [ 
+    (fun gl ->
+       let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in
+         Eterm.etermtac (evm, t) gl) ]
+END
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
new file mode 100644
index 00000000..c3f2a24d
--- /dev/null
+++ b/contrib/subtac/g_subtac.ml4
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*
+  Syntax for the subtac terms and types.
+  Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
+
+(* $Id: g_subtac.ml4 8688 2006-04-07 15:08:12Z msozeau $ *)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Options
+open Util
+open Names
+open Nameops
+open Vernacentries
+open Reduction
+open Term
+open Libnames
+open Topconstr
+
+(* We define new entries for programs, with the use of this module
+ * Subtac. These entries are named Subtac.<foo>
+ *)
+
+module Gram = Pcoq.Gram
+module Vernac = Pcoq.Vernac_
+
+module SubtacGram =
+struct
+  let gec s = Gram.Entry.create ("Subtac."^s)
+		(* types *)
+  let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+end
+
+open SubtacGram 
+open Util
+
+GEXTEND Gram
+  GLOBAL: subtac_gallina_loc;
+ 
+  subtac_gallina_loc:
+    [ [ g = Vernac.gallina -> loc, g ] ]
+    ;
+  END
+
+type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+
+let (wit_subtac_gallina_loc : gallina_loc_argtype),
+  (globwit_subtac_gallina_loc : gallina_loc_argtype),
+  (rawwit_subtac_gallina_loc : gallina_loc_argtype) =
+  Genarg.create_arg "subtac_gallina_loc"
+
+VERNAC COMMAND EXTEND Subtac
+[ "Program" subtac_gallina_loc(g) ] -> 
+  [ Subtac.subtac g ]
+END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
new file mode 100644
index 00000000..84b7d39b
--- /dev/null
+++ b/contrib/subtac/subtac.ml
@@ -0,0 +1,203 @@
+(************************************************************************)
+(*  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: subtac.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+
+open Global
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Vernacexpr
+
+open Subtac_coercion
+open Subtac_utils
+open Coqlib
+open Printer
+open Subtac_errors
+open Context
+open Eterm
+
+let require_library dirpath =
+  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
+    Library.require_library [qualid] None
+
+let subtac_one_fixpoint env isevars (f, decl) = 
+  let ((id, n, bl, typ, body), decl) = 
+    Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
+  in
+  let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
+		 Ppconstr.pr_constr_expr body)
+  in ((id, n, bl, typ, body), decl)
+    
+	      
+let subtac_fixpoint isevars l = 
+  (* TODO: Copy command.build_recursive *)
+  ()
+(*
+let save id const (locality,kind) hook =
+  let {const_entry_body = pft;
+       const_entry_type = tpo;
+       const_entry_opaque = opacity } = const in
+  let l,r = match locality with
+    | Local when Lib.sections_are_opened () ->
+        let k = logical_kind_of_goal_kind kind in
+	let c = SectionLocalDef (pft, tpo, opacity) in
+	let _ = declare_variable id (Lib.cwd(), c, k) in
+	(Local, VarRef id)
+    | Local ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	(Global, ConstRef kn)
+    | Global ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	(Global, ConstRef kn) in
+  Pfedit.delete_current_proof ();
+  hook l r;
+  definition_message id
+
+let save_named opacity =
+  let id,(const,persistence,hook) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
+  save id const persistence hook
+
+let check_anonymity id save_ident =
+  if atompart_of_id id <> "Unnamed_thm" then
+    error "This command can only be used for unnamed theorem"
+(*
+    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
+*)
+
+let save_anonymous opacity save_ident =
+  let id,(const,persistence,hook) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
+  check_anonymity id save_ident;
+  save save_ident const persistence hook
+
+let save_anonymous_with_strength kind opacity save_ident =
+  let id,(const,_,hook) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
+  check_anonymity id save_ident;
+  (* we consider that non opaque behaves as local for discharge *)
+  save save_ident const (Global, Proof kind) hook
+
+let subtac_end_proof = function
+  | Admitted -> admit ()
+  | Proved (is_opaque,idopt) ->
+    if_verbose show_script ();
+    match idopt with
+    | None -> save_named is_opaque
+    | Some ((_,id),None) -> save_anonymous is_opaque id
+    | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
+
+	*)
+
+let subtac (loc, command) =
+  check_required_library ["Coq";"Init";"Datatypes"];
+  check_required_library ["Coq";"Init";"Specif"];
+  require_library "Coq.subtac.FixSub";
+  require_library "Coq.subtac.Utils";
+  try
+    match command with
+	VernacDefinition (defkind, (locid, id), expr, hook) -> 
+	  let env = Global.env () in
+	  let isevars = ref (create_evar_defs Evd.empty) in
+	    (match expr with
+		 ProveBody (bl, c) -> 
+		   let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in
+		     trace (str "Starting proof");
+		     Command.start_proof id goal_kind c hook;
+		     trace (str "Started proof");	     
+		     
+	       | DefineBody (bl, _, c, tycon) -> 
+		   let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c tycon in
+		   let tac = Eterm.etermtac (evm, c) in 
+		     trace (str "Starting proof");
+		     Command.start_proof id goal_kind ctyp hook;
+		     trace (str "Started proof");
+		     Pfedit.by tac)
+      | VernacFixpoint (l, b) -> 
+	  let _ = trace (str "Building fixpoint") in
+	    ignore(Subtac_command.build_recursive l b)
+      (*| VernacEndProof e -> 
+	  subtac_end_proof e*)
+
+      | _ -> user_err_loc (loc,"", str ("Invalid Program command"))
+  with 
+    | Typing_error e ->
+	msg_warning (str "Type error in Program tactic:");
+	let cmds = 
+	  (match e with
+	     | NonFunctionalApp (loc, x, mux, e) ->
+		 str "non functional application of term " ++ 
+		 e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
+	     | NonSigma (loc, t) ->
+		 str "Term is not of Sigma type: " ++ t
+	     | NonConvertible (loc, x, y) ->
+		 str "Unconvertible terms:" ++ spc () ++
+		   x ++ spc () ++ str "and" ++ spc () ++ y
+	     | IllSorted (loc, t) ->
+		 str "Term is ill-sorted:" ++ spc () ++ t
+	  )
+	in msg_warning cmds
+	     
+    | Subtyping_error e ->
+	msg_warning (str "(Program tactic) Subtyping error:");
+	let cmds = 
+	  match e with
+	    | UncoercibleInferType (loc, x, y) ->
+		str "Uncoercible terms:" ++ spc ()
+		++ x ++ spc () ++ str "and" ++ spc () ++ y
+	    | UncoercibleInferTerm (loc, x, y, tx, ty) ->
+		str "Uncoercible terms:" ++ spc ()
+		++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
+		++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
+	    | UncoercibleRewrite (x, y) ->
+		str "Uncoercible terms:" ++ spc ()
+		++ x ++ spc () ++ str "and" ++ spc () ++ y
+	in msg_warning cmds
+    
+    | Type_errors.TypeError (env, e) ->
+	debug 2 (Himsg.explain_type_error env e)
+	  
+    | Pretype_errors.PretypeError (env, e) ->
+	debug 2 (Himsg.explain_pretype_error env e)
+	  
+    | Stdpp.Exc_located (loc, e) ->
+	debug 2 (str "Parsing exception: ");
+	(match e with
+	   | Type_errors.TypeError (env, e) ->
+	       debug 2 (Himsg.explain_type_error env e)
+		 
+	   | Pretype_errors.PretypeError (env, e) ->
+	       debug 2 (Himsg.explain_pretype_error env e)
+
+	   | e -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e))
+  
+    | e -> 
+	msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e)
+
+
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
new file mode 100644
index 00000000..a0d2fb2b
--- /dev/null
+++ b/contrib/subtac/subtac.mli
@@ -0,0 +1,14 @@
+val require_library : string -> unit
+val subtac_one_fixpoint :
+  'a ->
+  'b ->
+  (Names.identifier * (int * Topconstr.recursion_order_expr) *
+   Topconstr.local_binder list * Topconstr.constr_expr *
+   Topconstr.constr_expr) *
+  'c ->
+  (Names.identifier * (int * Topconstr.recursion_order_expr) *
+   Topconstr.local_binder list * Topconstr.constr_expr *
+   Topconstr.constr_expr) *
+  'c
+val subtac_fixpoint : 'a -> 'b -> unit
+val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
new file mode 100644
index 00000000..7c8ea2d6
--- /dev/null
+++ b/contrib/subtac/subtac_coercion.ml
@@ -0,0 +1,485 @@
+(************************************************************************)
+(*  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: subtac_coercion.ml 8695 2006-04-10 16:33:52Z msozeau $ *)
+
+open Util
+open Names
+open Term
+open Reductionops
+open Environ
+open Typeops
+open Pretype_errors
+open Classops
+open Recordops
+open Evarutil
+open Evarconv
+open Retyping
+open Evd
+
+open Global
+open Subtac_utils
+open Coqlib
+open Printer
+open Subtac_errors
+open Context
+open Eterm
+open Pp
+
+let pair_of_array a = (a.(0), a.(1))
+let make_name s = Name (id_of_string s)
+
+module Coercion = struct
+
+  exception NoSubtacCoercion
+
+  let rec disc_subset x = 
+    match kind_of_term x with
+      | App (c, l) ->
+	  (match kind_of_term c with
+	       Ind i ->
+		 let len = Array.length l in
+		 let sig_ = Lazy.force sig_ in
+		   if len = 2 && i = Term.destInd sig_.typ
+		   then
+		     let (a, b) = pair_of_array l in
+		       Some (a, b)
+		   else None
+	     | _ -> None)
+      | _ -> None
+	  
+  and disc_exist env x =
+    trace (str "Disc_exist: " ++ my_print_constr env x);
+    match kind_of_term x with
+      | App (c, l) ->
+	  (match kind_of_term c with
+	       Construct c ->	       
+		 if c = Term.destConstruct (Lazy.force sig_).intro
+		 then Some (l.(0), l.(1), l.(2), l.(3))
+		 else None
+	     | _ -> None)
+      | _ -> None
+
+
+  let disc_proj_exist env x =
+    trace (str "disc_proj_exist: " ++ my_print_constr env x);
+    match kind_of_term x with
+      | App (c, l) ->
+	  (if Term.eq_constr c (Lazy.force sig_).proj1 
+	     && Array.length l = 3 
+	   then disc_exist env l.(2)
+	   else None)
+      | _ -> None
+
+
+  let sort_rel s1 s2 = 
+    match s1, s2 with
+	Prop Pos, Prop Pos -> Prop Pos
+      | Prop Pos, Prop Null -> Prop Null
+      | Prop Null, Prop Null -> Prop Null
+      | Prop Null, Prop Pos -> Prop Pos
+      | Type _, Prop Pos -> Prop Pos
+      | Type _, Prop Null -> Prop Null
+      | _, Type _ -> s2
+
+  let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
+
+  let rec mu env isevars t =   
+    let rec aux v = 
+      match disc_subset v with
+	  Some (u, p) -> 
+	    let f, ct = aux u in
+	      (Some (fun x ->		   
+		       app_opt f (mkApp ((Lazy.force sig_).proj1, 
+					 [| u; p; x |]))),
+	       ct)
+	| None -> (None, t)
+    in aux t
+
+  and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
+      : (Term.constr -> Term.constr) option 
+      =
+    let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
+      trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
+	     str " and "++ my_print_constr env y ++ 
+	     str " with evars: " ++ spc () ++
+	     my_print_evardefs !isevars);
+    let rec coerce_unify env x y =
+      trace (str "coerce_unify from " ++ (my_print_constr env x) ++ 
+	     str " to "++ my_print_constr env y);
+      try 
+	isevars := the_conv_x_leq env x y !isevars;
+	trace (str "Unified " ++ (my_print_constr env x) ++ 
+	       str " and "++ my_print_constr env y);
+	None
+      with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
+    and coerce' env x y : (Term.constr -> Term.constr) option =
+      let subco () = subset_coerce env isevars x y in
+	trace (str "coerce' from " ++ (my_print_constr env x) ++ 
+		 str " to "++ my_print_constr env y);
+	match (kind_of_term x, kind_of_term y) with
+	  | Sort s, Sort s' -> 
+	      (match s, s' with
+		   Prop x, Prop y when x = y -> None
+		 | Prop _, Type _ -> None
+		 | Type x, Type y when x = y -> None (* false *)
+		 | _ -> subco ())
+	  | Prod (name, a, b), Prod (name', a', b') ->
+	      let c1 = coerce_unify env a' a in
+	      let env' = push_rel (name', None, a') env in
+	      let c2 = coerce_unify env' b b' in
+		(match c1, c2 with
+		     None, None -> failwith "subtac.coerce': Should have detected equivalence earlier"
+		   | _, _ ->
+		       Some
+			 (fun f -> 
+			    mkLambda (name', a',
+				      app_opt c2
+					(mkApp (Term.lift 1 f, 
+						[| app_opt c1 (mkRel 1) |])))))
+		  
+	  | App (c, l), App (c', l') ->
+	      (match kind_of_term c, kind_of_term c' with
+		   Ind i, Ind i' -> (* Sigma types *)
+		     let len = Array.length l in
+		     let existS = Lazy.force existS in
+		     let prod = Lazy.force prod in
+		       if len = Array.length l' && len = 2 && i = i'
+		       then 
+			 if i = Term.destInd existS.typ 
+			 then
+			   begin 
+			     debug 1 (str "In coerce sigma types");
+			     let (a, pb), (a', pb') = 
+			       pair_of_array l, pair_of_array l' 
+			     in
+			     let c1 = coerce_unify env a a' in
+			     let rec remove_head a c = 
+			       match kind_of_term c with 
+				 | Lambda (n, t, t') -> c, t'
+				     (*| Prod (n, t, t') -> t'*)
+				 | Evar (k, args) ->
+				     let (evs, t) = Evarutil.define_evar_as_lambda !isevars (k,args) in
+				       isevars := evs;
+				       let (n, dom, rng) = destLambda t in
+				       let (domk, args) = destEvar dom in
+					 isevars := evar_define domk a !isevars;
+					 t, rng
+				 | _ -> raise NoSubtacCoercion
+			     in
+			     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
+			     let env' = push_rel (make_name "x", None, a) env in
+			     let c2 = coerce_unify env' b b' in
+			       match c1, c2 with
+				   None, None -> 
+				     trace (str "No coercion needed");
+				     None
+				 | _, _ ->
+				     Some 
+				       (fun x ->
+					  let x, y = 
+					    app_opt c1 (mkApp (existS.proj1,
+							       [| a; pb; x |])),
+					    app_opt c2 (mkApp (existS.proj2, 
+							       [| a; pb; x |]))
+					  in
+					    mkApp (existS.intro, [| a'; pb'; x ; y |]))
+			   end
+			 else if i = Term.destInd prod.typ then
+			   begin 
+			     debug 1 (str "In coerce prod types");
+			     let (a, b), (a', b') = 
+			       pair_of_array l, pair_of_array l' 
+			     in
+			     let c1 = coerce_unify env a a' in
+			     let c2 = coerce_unify env b b' in
+			       match c1, c2 with
+				   None, None -> None
+				 | _, _ ->
+				     Some 
+				       (fun x ->
+					  let x, y = 
+					    app_opt c1 (mkApp (prod.proj1,
+							       [| a; b; x |])),
+					    app_opt c2 (mkApp (prod.proj2, 
+							       [| a; b; x |]))
+					  in
+					    mkApp (prod.intro, [| a'; b'; x ; y |]))
+			   end
+			 else subco ()
+		       else subco ()
+		 | _ ->  subco ())
+	  | _, _ ->  subco ()
+
+    and subset_coerce env isevars x y =
+      match disc_subset x with
+	  Some (u, p) -> 
+	    let c = coerce_unify env u y in
+	    let f x = 
+	      app_opt c (mkApp ((Lazy.force sig_).proj1, 
+				[| u; p; x |]))
+	    in Some f
+	| None ->
+	    match disc_subset y with
+		Some (u, p) ->
+		  let c = coerce_unify env x u in
+		    Some 
+		      (fun x ->
+			 let cx = app_opt c x in
+			 let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |]))
+			 in
+			   (mkApp 
+			      ((Lazy.force sig_).intro, 
+			       [| u; p; cx; evar |])))
+	      | None -> 
+		  raise NoSubtacCoercion
+		    (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
+		  None*)
+    in coerce_unify env x y
+
+  let coerce_itf loc env isevars v t c1 =
+    let evars = ref isevars in
+    let coercion = coerce loc env evars t c1 in
+      !evars, option_app (app_opt coercion) v, t
+	
+  (* Taken from pretyping/coercion.ml *)
+
+  (* Typing operations dealing with coercions *)
+
+  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+
+  (* Here, funj is a coercion therefore already typed in global context *)
+  let apply_coercion_args env argl funj =
+    let rec apply_rec acc typ = function
+      | [] -> { uj_val = applist (j_val funj,argl);
+		uj_type = typ }
+      | h::restl ->
+	  (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
+  	  match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
+	    | Prod (_,c1,c2) -> 
+		(* Typage garanti par l'appel à app_coercion*)
+		apply_rec (h::acc) (subst1 h c2) restl
+	    | _ -> anomaly "apply_coercion_args"
+    in 
+      apply_rec [] funj.uj_type argl
+
+  (* appliquer le chemin de coercions de patterns p *)
+  exception NoCoercion
+
+  let apply_pattern_coercion loc pat p =
+    List.fold_left
+      (fun pat (co,n) ->
+	 let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
+	   Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+      pat p
+
+  (* raise Not_found if no coercion found *)
+  let inh_pattern_coerce_to loc pat ind1 ind2 =
+    let i1 = inductive_class_of ind1 in
+    let i2 = inductive_class_of ind2 in
+    let p = lookup_pattern_path_between (i1,i2) in
+      apply_pattern_coercion loc pat p
+
+  (* appliquer le chemin de coercions p à hj *)
+
+  let apply_coercion env p hj typ_cl =
+    try 
+      fst (List.fold_left
+             (fun (ja,typ_cl) i -> 
+		let fv,isid = coercion_value i in
+		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let jres = apply_coercion_args env argl fv in
+		  (if isid then 
+		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
+		   else 
+		     jres),
+		jres.uj_type)
+             (hj,typ_cl) p)
+    with _ -> anomaly "apply_coercion"
+
+  let inh_app_fun env isevars j = 
+    let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+      match kind_of_term t with
+	| Prod (_,_,_) -> (isevars,j)
+	| Evar ev when not (is_defined_evar isevars ev) ->
+	    let (isevars',t) = define_evar_as_arrow isevars ev in
+	      (isevars',{ uj_val = j.uj_val; uj_type = t })
+	| _ ->
+       	    (try
+ 	       let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+      	       let p = lookup_path_to_fun_from i1 in
+		 (isevars,apply_coercion env p j t)
+	     with Not_found ->
+	       try 
+		 let coercef, t = mu env isevars t in
+		   (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
+	       with NoSubtacCoercion | NoCoercion ->
+		 (isevars,j))
+
+  let inh_tosort_force loc env isevars j =
+    try
+      let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+      let p = lookup_path_to_sort_from i1 in
+      let j1 = apply_coercion env p j t in 
+	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+    with Not_found ->
+      error_not_a_type_loc loc env (evars_of isevars) j
+
+  let inh_coerce_to_sort loc env isevars j =
+    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+      match kind_of_term typ with
+	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
+	| Evar ev when not (is_defined_evar isevars ev) ->
+	    let (isevars',s) = define_evar_as_sort isevars ev in
+	      (isevars',{ utj_val = j.uj_val; utj_type = s })
+	| _ ->
+	    inh_tosort_force loc env isevars j
+
+  let inh_coerce_to_fail env isevars c1 v t =
+    let v', t' =
+      try 
+	let t1,i1 = class_of1 env (evars_of isevars) c1 in
+	let t2,i2 = class_of1 env (evars_of isevars) t in
+	let p = lookup_path_between (i2,i1) in
+	  match v with
+	      Some v -> 
+		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		  Some j.uj_val, j.uj_type
+	    | None -> None, t
+      with Not_found -> raise NoCoercion 
+    in
+      try (the_conv_x_leq env t' c1 isevars, v', t')
+      with Reduction.NotConvertible -> raise NoCoercion
+
+  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+    (try
+       trace (str "inh_conv_coerce_to_fail called for " ++
+	      Termops.print_constr_env env t ++ str " and "++ spc () ++
+	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
+	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+	      Termops.print_env env);
+     with _ -> ());
+    try (the_conv_x_leq env t c1 isevars, v, t)
+    with Reduction.NotConvertible ->
+      (try 
+	 inh_coerce_to_fail env isevars c1 v t
+	 with NoCoercion ->
+	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
+		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
+		    let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
+		    let (evd',b) =
+		      match v' with 
+			  Some v' ->
+			    (match kind_of_term v' with
+			       | Lambda (x,v1,v2) ->
+				   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)  (* leq v1 u1? *)
+				    with Reduction.NotConvertible -> (isevars, None))
+			       | _  -> (isevars, None))
+			| None -> (isevars, None)
+		    in 
+		      (match b with
+			   Some (x, v1, v2) ->
+			     let env1 = push_rel (x,None,v1) env in
+			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+						       (Some v2) t2 u2 in
+			       (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2', 
+				mkProd (x, v1, t2'))
+			 | None ->
+			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+			     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+			     (* has type (name:u1)u2 (with v' recursively obtained) *)
+			     let name = (match name with 
+					   | Anonymous -> Name (id_of_string "x")
+					   | _ -> name) in
+			     let env1 = push_rel (name,None,u1) env in
+			     let (evd', v1', t1') =
+			       inh_conv_coerce_to_fail loc env1 isevars
+				 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) 
+			     in
+			     let (evd'', v2', t2') = 
+			       let v2 =
+				 match v with 
+				     Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+				   | None -> None
+			       and evd', t2 =
+				 match v1' with 
+				     Some v1' -> evd', subst1 v1' t2
+				   | None -> 
+				       let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
+					 evd', subst1 ev t2
+			       in
+				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+			     in
+			       (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2',
+				mkProd (name, u1, t2')))
+		| _ -> raise NoCoercion))
+
+	
+  (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
+  let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
+    (try 
+       trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
+	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ 
+	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
+	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+	      Termops.print_env env);
+     with _ -> ());
+    match n with
+	None ->
+	  let (evd', val', type') = 
+	    try 
+	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	    with NoCoercion ->
+	      let sigma = evars_of isevars in
+		try
+		  coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+		with NoSubtacCoercion ->
+		  error_actual_type_loc loc env sigma cj t
+	  in
+	  let val' = match val' with Some v -> v | None -> assert(false) in
+	    (evd',{ uj_val = val'; uj_type = t })
+      | Some (init, cur) ->
+	  (isevars, cj)
+
+  let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
+    (try 
+       trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
+	      Termops.print_constr_env env t ++ str " and "++ spc () ++ 
+	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
+	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+	      Termops.print_env env);
+     with _ -> ());
+    let nabsinit, nabs = 
+      match abs with
+	  None -> 0, 0
+	| Some (init, cur) -> init, cur
+    in
+    let (rels, rng) = 
+      (* a little more effort to get products is needed *) 
+      try decompose_prod_n nabs t
+      with _ -> 
+	trace (str "decompose_prod_n failed");
+	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
+    in
+      (* The final range free variables must have been replaced by evars, we accept only that evars
+	 in rng are applied to free vars. *)
+      if noccur_with_meta 0 (succ nabsinit) rng then (
+	trace (str "No occur between 0 and " ++ int (succ nabsinit));
+	let env', t, t' = 
+	  let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+	    env', rng, lift nabs t'
+	in
+	  try 
+	    pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+		 with NoCoercion ->
+		   coerce_itf loc env' isevars None t t') 
+	  with NoSubtacCoercion ->
+	    let sigma = evars_of isevars in
+	      error_cannot_coerce env' sigma (t, t'))
+      else isevars 
+end
diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli
new file mode 100644
index 00000000..53a8d213
--- /dev/null
+++ b/contrib/subtac/subtac_coercion.mli
@@ -0,0 +1 @@
+module Coercion : Coercion.S
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
new file mode 100644
index 00000000..1b92c691
--- /dev/null
+++ b/contrib/subtac/subtac_command.ml
@@ -0,0 +1,422 @@
+open Closure
+open RedFlags
+open Declarations
+open Entries
+open Dyn
+open Libobject
+open Pattern
+open Matching
+open Pp
+open Rawterm
+open Sign
+open Tacred
+open Util
+open Names
+open Nameops
+open Libnames
+open Nametab
+open Pfedit
+open Proof_type
+open Refiner
+open Tacmach
+open Tactic_debug
+open Topconstr
+open Term
+open Termops
+open Tacexpr
+open Safe_typing
+open Typing
+open Hiddentac
+open Genarg
+open Decl_kinds
+open Mod_subst
+open Printer
+open Inductiveops
+open Syntax_def
+open Environ
+open Tactics
+open Tacticals
+open Tacinterp
+open Vernacexpr
+open Notation
+
+module SPretyping = Subtac_pretyping.Pretyping
+open Subtac_utils
+open Pretyping
+
+(*********************************************************************)
+(* Functions to parse and interpret constructions *)
+
+let evar_nf isevars c =
+  isevars := Evarutil.nf_evar_defs !isevars;
+  Evarutil.nf_isevar !isevars c
+
+let interp_gen kind isevars env 
+               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               c =
+  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
+  let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
+    msgnl (str "Pretyping " ++ my_print_constr_expr c);
+  let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
+    evar_nf isevars c'
+    
+let interp_constr isevars env c =
+  interp_gen (OfType None) isevars env c 
+
+let interp_type isevars env ?(impls=([],[])) c =
+  interp_gen IsType isevars env ~impls c
+
+let interp_casted_constr isevars env ?(impls=([],[])) c typ =
+  interp_gen (OfType (Some typ)) isevars env ~impls c 
+
+let interp_open_constr isevars env c =
+    msgnl (str "Pretyping " ++ my_print_constr_expr c);
+  let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
+  let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
+    evar_nf isevars c'
+
+let interp_constr_judgment isevars env c =
+  let j = 
+    SPretyping.understand_judgment_tcc isevars env
+      (Constrintern.intern_constr (Evd.evars_of !isevars) env c) 
+  in
+    { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
+
+let locate_if_isevar loc na = function
+  | RHole _ -> 
+      (try match na with
+	| Name id ->  Reserve.find_reserved_type id
+	| Anonymous -> raise Not_found 
+      with Not_found -> RHole (loc, Evd.BinderType na))
+  | x -> x
+
+let interp_binder sigma env na t =
+  let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
+    SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t)
+      
+
+let interp_context sigma env params = 
+  List.fold_left
+    (fun (env,params) d -> match d with
+      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+	  let t = interp_binder sigma env na t in
+	  let d = (na,None,t) in
+	  (push_rel d env, d::params)
+      | LocalRawAssum (nal,t) ->
+	  let t = interp_type sigma env t in
+	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	  let ctx = List.rev ctx in
+	  (push_rel_context ctx env, ctx@params)
+      | LocalRawDef ((_,na),c) ->
+	  let c = interp_constr_judgment sigma env c in
+	  let d = (na, Some c.uj_val, c.uj_type) in
+	  (push_rel d env,d::params))
+    (env,[]) params
+
+(* try to find non recursive definitions *)
+
+let list_chop_hd i l = match list_chop i l with
+  | (l1,x::l2) -> (l1,x,l2)
+  | _ -> assert false
+
+let collect_non_rec env = 
+  let rec searchrec lnonrec lnamerec ldefrec larrec nrec = 
+    try
+      let i = 
+        list_try_find_i
+          (fun i f ->
+             if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec
+             then i else failwith "try_find_i")
+          0 lnamerec 
+      in
+      let (lf1,f,lf2) = list_chop_hd i lnamerec in
+      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
+      let (lar1,ar,lar2) = list_chop_hd i larrec in
+      let newlnv = 
+	try 
+	  match list_chop i nrec with 
+            | (lnv1,_::lnv2) -> (lnv1@lnv2)
+	    | _ -> [] (* nrec=[] for cofixpoints *)
+        with Failure "list_chop" -> []
+      in 
+      searchrec ((f,def,ar)::lnonrec) 
+	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
+    with Failure "try_find_i" -> 
+      (List.rev lnonrec,
+       (Array.of_list lnamerec, Array.of_list ldefrec,
+        Array.of_list larrec, Array.of_list nrec))
+  in 
+  searchrec [] 
+
+let definition_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+let recursive_message v =
+  match Array.length v with
+    | 0 -> error "no recursive definition"
+    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+		    spc () ++ str "are recursively defined")
+
+let filter_map f l = 
+  let rec aux acc = function
+      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
+		     | None -> aux acc tl)
+    | [] -> List.rev acc
+  in aux [] l
+
+let list_of_local_binders l = 
+  let rec aux acc = function
+      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
+    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
+	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
+    | [] -> List.rev acc
+  in aux [] l
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+  let sigma = Evd.empty
+  and env0 = Global.env()
+  in 
+  let lnameargsardef =
+    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
+      lnameargsardef
+  in
+  let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
+  and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
+  in
+  (* Build the recursive context and notations for the recursive types *)
+  let (rec_sign,rec_impls,arityl) = 
+    List.fold_left 
+      (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) -> 
+	let isevars = ref (Evd.create_evar_defs sigma) in	  
+	  match ro with
+	      CStructRec ->
+		let arityc = Command.generalize_constr_expr arityc bl in
+		let arity = interp_type isevars env0 arityc in
+		let impl = 
+		  if Impargs.is_implicit_args()
+		  then Impargs.compute_implicits env0 arity
+		  else [] in
+		let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+		  (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
+	    | CWfRec r -> 		    
+		let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
+			       Ppconstr.pr_binders bl ++ str " : " ++ 
+			       Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+			       Ppconstr.pr_constr_expr body)
+		in
+		let env', binders_rel = interp_context isevars env0 bl in
+		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
+		let argid = match argname with Name n -> n | _ -> assert(false) in
+		let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
+		let envwf = push_rel_context before env0 in
+		let wf_rel = interp_constr isevars envwf r in
+		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
+		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
+		let argid' = id_of_string (string_of_id argid ^ "'") in
+		let before_length, after_length = List.length before, List.length after in
+		let full_length = before_length + 1 + after_length in
+		let wfarg len = (Name argid, None, 
+				 mkSubset (Name argid') argtyp 
+				   (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+		in
+		let new_bl = after' @ (accarg :: arg :: before)
+		and intern_bl =  after @ (wfarg (before_length + 1) :: before)
+		in
+		let intern_env = push_rel_context intern_bl env0 in
+		let env' = push_rel_context new_bl env0 in
+		let arity = interp_type isevars intern_env arityc in
+		let intern_arity = it_mkProd_or_LetIn arity intern_bl in
+		let arity' = interp_type isevars env' arityc in
+		let arity' = it_mkProd_or_LetIn arity' new_bl in
+		let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
+		let _ = 
+		  let pr c = my_print_constr env c in
+		  let prr = Printer.pr_rel_context env in
+		    trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+			     str "Intern bl" ++ prr intern_bl ++ spc () ++
+			     str "Extern bl" ++ prr new_bl ++ spc () ++
+			     str "Intern arity: " ++ pr intern_arity)
+		in
+		let impl = 
+		  if Impargs.is_implicit_args()
+		  then Impargs.compute_implicits intern_env arity'
+		  else [] in
+		let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
+		  (Environ.push_named (recname,None,arity') env, impls', 
+		   (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
+      (env0,[],[]) lnameargsardef in
+  let arityl = List.rev arityl in
+  let notations = 
+    List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
+      lnameargsardef [] in
+
+  let recdef =
+
+    (* Declare local notations *)
+    let fs = States.freeze() in
+    let def = 
+      try
+	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
+	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
+	List.map2
+	  (fun ((_,_,bl,_,def),_) (isevars, info, arity) ->
+	     match info with
+		 None ->
+		   let def = abstract_constr_expr def bl in
+		     isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+		       def arity
+	       | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
+		   let rec_sign = push_rel_context fun_bl rec_sign in
+		   let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+				def intern_arity
+		   in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
+          lnameargsardef arityl
+      with e ->
+	States.unfreeze fs; raise e in
+    States.unfreeze fs; def 
+  in
+
+  let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
+    collect_non_rec env0 lrecnames recdef arityl nv in
+  let nvrec' = Array.map fst nvrec in(* ignore rec order *)
+  let declare arrec defrec =
+    let recvec = 
+      Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
+    let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
+    let rec declare i fi =
+      trace (str "Declaring: " ++ pr_id fi ++ spc () ++
+	     my_print_constr env0 (recvec.(i)));
+      let ce = 
+	{ const_entry_body = mkFix ((nvrec',i),recdecls); 
+          const_entry_type = Some arrec.(i);
+          const_entry_opaque = false;
+          const_entry_boxed = boxed} in
+      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+      in (ConstRef kn)
+    in 
+      (* declare the recursive definitions *)
+    let lrefrec = Array.mapi declare namerec in
+      Options.if_verbose ppnl (recursive_message lrefrec);
+
+
+      (*(* The others are declared as normal definitions *)
+      let var_subst id = (id, Constrintern.global_reference id) in
+      let _ = 
+	List.fold_left
+	  (fun subst (f,def,t) ->
+	     let ce = { const_entry_body = replace_vars subst def;
+			const_entry_type = Some t;
+			const_entry_opaque = false;
+			const_entry_boxed = boxed } in
+	     let _ =
+	       Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+	     in
+      	       warning ((string_of_id f)^" is non-recursively defined");
+      	       (var_subst f) :: subst)
+	  (List.map var_subst (Array.to_list namerec))
+	  lnonrec 
+      in*)
+      List.iter (fun (df,c,scope) ->
+		   Metasyntax.add_notation_interpretation df [] c scope) notations
+  in 
+  let declare l = 
+    let recvec = Array.of_list l
+    and arrec = Array.map pi3 arrec
+    in declare arrec recvec
+  in
+  let recdefs = Array.length defrec in
+    trace (int recdefs ++ str " recursive definitions");
+    (* Solve remaining evars *)
+  let rec collect_evars i acc = 
+    if i < recdefs then
+      let (isevars, info, def) = defrec.(i) in
+      let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) in
+      let def = evar_nf isevars def in
+      let isevars = Evd.undefined_evars !isevars in
+      let _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) in
+      let evm = Evd.evars_of isevars in
+      let _, _, typ = arrec.(i) in
+      let id = namerec.(i) in
+      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 	
+      (* Generalize by the recursive prototypes  *)
+      let def = 
+	Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
+      and typ = 
+	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) 
+      in
+      (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
+      (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
+      (*let ce = 
+	{ const_entry_body = evars_def; 
+	  const_entry_type = Some evars_typ;
+	  const_entry_opaque = false;
+	  const_entry_boxed = boxed} in
+      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in
+	definition_message fi;
+	trace (str (string_of_id fi) ++ str " is defined");*)
+	let evar_sum =
+	  if evars = [] then None
+	  else 
+	    let sum = Subtac_utils.build_dependent_sum evars in
+	      trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum));
+	      Some sum
+	in
+	  collect_evars (succ i) ((id, evars_def, evar_sum) :: acc)
+    else acc
+  in 
+  let defs = collect_evars 0 [] in
+
+  (* Solve evars then create the definitions *)
+  let real_evars = 
+    filter_map (fun (id, kn, sum) ->
+		  match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None)
+      defs
+  in
+    Subtac_utils.and_tac real_evars
+      (fun f _ gr ->
+	 let _ = trace (str "Got a proof of: " ++ pr_global gr) in
+	 let constant = match gr with Libnames.ConstRef c -> c
+	   | _ -> assert(false)
+	 in
+	   try
+	     (*let value = Environ.constant_value (Global.env ()) constant in*)
+	     let pis = f (mkConst constant) in
+	       trace (str "Accessors: " ++
+		      List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
+			pis (mt()));
+	       trace (str "Applied existentials: " ++
+		      (List.fold_right
+			 (fun (id, kn, sumg, pi) acc ->
+			    let args = Subtac_utils.destruct_ex pi sumg in
+			      my_print_constr env0 (mkApp (kn, Array.of_list args)))
+			 pis (mt ())));
+	       let rec aux pis acc = function
+		   (id, kn, sum) :: tl ->
+		     (match sum with 
+			  None -> aux pis (kn :: acc) tl
+			| Some (sumg, _, _) -> 
+			    let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
+			    let args = Subtac_utils.destruct_ex pi sumg in
+			    let args = 
+			      List.map (fun c -> 
+					  try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c
+					  with Not_found ->
+					    trace (str "Not_found while reducing " ++
+						   my_print_constr (Global.env ()) c);
+					    c
+				       ) args 				  
+			    in
+			    let _, newdef = decompose_lam_n (recdefs + List.length args) kn in
+			    let constr = Term.substl (mkRel 1 :: List.rev args) newdef in
+			      aux pis (constr :: acc) tl)
+		 | [] -> List.rev acc
+	       in
+		 declare (aux pis [] defs)
+	   with Environ.NotEvaluableConst cer ->
+	     match cer with
+		 Environ.NoBody -> trace (str "Constant has no body")
+	       | Environ.Opaque -> trace (str "Constant is opaque")
+      )
+      
+      
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
new file mode 100644
index 00000000..e1bbbbb5
--- /dev/null
+++ b/contrib/subtac/subtac_command.mli
@@ -0,0 +1,42 @@
+open Pretyping
+open Evd
+open Environ
+open Term
+open Topconstr
+open Names
+open Libnames
+open Pp
+open Vernacexpr
+open Constrintern
+
+val interp_gen :
+  typing_constraint ->
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  ?allow_soapp:bool ->
+  ?ltacvars:ltac_sign ->
+  constr_expr -> constr
+val interp_constr :
+  evar_defs ref ->
+  env -> constr_expr -> constr
+val interp_type :
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  constr_expr -> constr
+val interp_casted_constr :
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  constr_expr -> types -> constr
+val interp_open_constr :
+  evar_defs ref -> env -> constr_expr -> constr
+val interp_constr_judgment :
+  evar_defs ref ->
+  env ->
+  constr_expr -> unsafe_judgment
+val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
+val recursive_message : global_reference array -> std_ppcmds
+val build_recursive :
+  (fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_errors.ml b/contrib/subtac/subtac_errors.ml
new file mode 100644
index 00000000..3bbfe22b
--- /dev/null
+++ b/contrib/subtac/subtac_errors.ml
@@ -0,0 +1,24 @@
+open Util
+open Pp
+open Printer
+
+type term_pp = Pp.std_ppcmds
+
+type subtyping_error = 
+  | UncoercibleInferType of loc * term_pp * term_pp
+  | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp
+  | UncoercibleRewrite of term_pp * term_pp
+
+type typing_error = 
+  | NonFunctionalApp of loc * term_pp * term_pp * term_pp
+  | NonConvertible of loc * term_pp * term_pp
+  | NonSigma of loc * term_pp
+  | IllSorted of loc * term_pp
+
+exception Subtyping_error of subtyping_error
+exception Typing_error of typing_error
+  
+exception Debug_msg of string
+
+let typing_error e = raise (Typing_error e)
+let subtyping_error e = raise (Subtyping_error e)
diff --git a/contrib/subtac/subtac_errors.mli b/contrib/subtac/subtac_errors.mli
new file mode 100644
index 00000000..8d75b9c0
--- /dev/null
+++ b/contrib/subtac/subtac_errors.mli
@@ -0,0 +1,15 @@
+type term_pp = Pp.std_ppcmds
+type subtyping_error =
+    UncoercibleInferType of Util.loc * term_pp * term_pp
+  | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp
+  | UncoercibleRewrite of term_pp * term_pp
+type typing_error =
+    NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp
+  | NonConvertible of Util.loc * term_pp * term_pp
+  | NonSigma of Util.loc * term_pp
+  | IllSorted of Util.loc * term_pp
+exception Subtyping_error of subtyping_error
+exception Typing_error of typing_error
+exception Debug_msg of string
+val typing_error : typing_error -> 'a
+val subtyping_error : subtyping_error -> 'a
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
new file mode 100644
index 00000000..599dbe39
--- /dev/null
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -0,0 +1,219 @@
+open Global
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Topconstr
+
+open Subtac_coercion
+open Subtac_utils
+open Coqlib
+open Printer
+open Subtac_errors
+open Context
+open Eterm
+
+
+let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args)
+
+let mkSubset name typ prop = 
+  mkAppExplC (sig_ref,
+	      [ typ; mkLambdaC ([name], typ, prop) ])
+	      
+let mkProj1 u p x = 
+  mkAppExplC (proj1_sig_ref, [ u; p; x ])
+
+let mkProj2 u p x = 
+  mkAppExplC (proj2_sig_ref, [ u; p; x ])
+
+let list_of_local_binders l = 
+  let rec aux acc = function
+      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl
+    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
+	aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl
+    | [] -> List.rev acc
+  in aux [] l
+       
+let abstract_constr_expr_bl abs c bl =
+  List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c
+
+let pr_binder_list b = 
+  List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
+		     Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ()) 
+
+
+let rec rewrite_rec_calls l c = c
+
+let rewrite_fixpoint env l (f, decl) = 
+  let (id, (n, ro), bl, typ, body) = f in
+  let body = rewrite_rec_calls l body in
+    match ro with
+	CStructRec -> ((id, (n, ro), bl, typ, body), decl)
+      | CWfRec wfrel -> 
+	  let bls = list_of_local_binders bl in
+	  let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++ 
+			 Ppconstr.pr_binders bl ++ str " : " ++ 
+			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
+			 Ppconstr.pr_constr_expr body)
+	  in
+	  let before, after = list_chop n bls in
+	  let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
+			 pr_binder_list before ++ str "; after the recursion arg: " ++
+			 pr_binder_list after)
+	  in
+	  let ((locn, name) as lnid, ntyp), after = match after with
+	      hd :: tl -> hd, tl
+	    | _ -> assert(false) (* Rec arg must be in after *)
+	  in
+	  let nid = match name with
+	      Name id -> id
+	    | Anonymous -> assert(false) (* Rec arg _must_ be named *)
+	  in
+	  let _wfproof = 
+	    let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in
+	      (*make_existential_expr dummy_loc before wf_rel*)
+	      mkRefC lt_wf_ref
+	  in
+	  let nid', accproofid = 
+	    let nid = string_of_id nid in
+	      id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
+	  in
+	  let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
+	  let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
+	  let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in
+	  let typnid' = mkSubset lnid' ntyp wf_prop in
+	  let internal_type = 
+	    abstract_constr_expr_bl mkProdC 
+	      (mkProdC ([lnid'], typnid', 
+			mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'), 
+				  abstract_constr_expr_bl mkProdC typ after)))
+	      before
+	  in
+	  let body' =
+	    let body =
+	      (* cast or we will loose some info at pretyping time as body
+		 is a function *)
+	      CCast (dummy_loc, body,  DEFAULTcast, typ) 
+	    in
+	    let body' = (* body abstracted by rec call *)
+	      mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
+	    in
+	      mkAppC (body',
+		      [mkLambdaC 
+			 ([lnid'], typnid',
+			  mkAppC (mkIdentC id, 
+				  [mkProj1 ntyp lam_wf_prop (mkIdentC nid');
+				   (mkAppExplC (acc_inv_ref,
+						[ ntyp; wfrel;
+						  mkIdentC nid;
+						  mkIdentC accproofid;
+						  mkProj1 ntyp lam_wf_prop (mkIdentC nid');
+						  mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))])
+	  in
+	  let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
+	  let bl' = 
+	    let rec aux acc = function
+		Topconstr.LocalRawDef _ as x :: tl -> 
+		  aux (x :: acc) tl
+	      | Topconstr.LocalRawAssum (bl, typ) as assum :: tl ->
+		  let rec aux' bl' = function
+		      ((loc, name') as x) :: tl ->
+			if name' = name then
+			  (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @
+			  LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
+			    [LocalRawAssum (List.rev (x :: bl'), typ)]
+			else aux' (x :: bl') tl
+		    | [] -> [assum]
+		  in aux (aux' [] bl @ acc) tl
+	      | [] -> List.rev acc
+	    in aux [] bl
+	  in
+	  let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++ 
+			 Ppconstr.pr_binders bl' ++ str " : " ++ 
+			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
+			 Ppconstr.pr_constr_expr body')
+	  in (id, (succ n, ro), bl', typ, body'), decl
+
+let list_mapi f = 
+  let rec aux i = function 
+      hd :: tl -> f i hd :: aux (succ i) tl 
+    | [] -> []
+  in aux 0
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+  let tml = list_mapi (fun i (c, (n, opt)) -> c, 
+		       ((match n with
+			    Name id -> (match c with
+					  | RVar (_, id') when id = id' ->
+					      Name (id_of_string (string_of_id id ^ "'"))
+					  | _ -> n)
+			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
+			opt)) tml 
+  in
+  let mkHole = RHole (dummy_loc, InternalHole) in
+  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+		       [mkHole; c; n])
+  in
+  let eqs_types = 
+    List.map
+      (fun (c, (n, _)) ->
+	 let id = match n with Name id -> id | _ -> assert false in
+	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
+	   Name heqid, mkeq c (RVar (dummy_loc, id)))
+      tml
+  in
+  let po = 
+    List.fold_right
+      (fun (n,t) acc ->
+	 RProd (dummy_loc, Anonymous, t, acc))
+      eqs_types (match po with 
+		     Some e -> e
+		   | None -> mkHole)
+  in
+  let eqns =   
+    List.map (fun (loc, idl, cpl, c) ->
+		let c' = 
+		  List.fold_left 
+		    (fun acc (n, t) ->
+		       RLambda (dummy_loc, n, mkHole, acc))
+		    c eqs_types
+		in (loc, idl, cpl, c'))
+      eqns
+  in
+  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+			      [mkHole; c])
+  in
+  let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
+  let case = RCases (loc,Some po,tml,eqns) in
+  let app = RApp (dummy_loc, case, refls) in
+    app
+
+let rec rewrite_cases c = 
+  match c with 
+      RCases _ -> let c' = map_rawconstr rewrite_cases c in
+	(match c' with 
+	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+	   | _ -> assert(false))
+    | _ -> map_rawconstr rewrite_cases c
+	  
+let rewrite_cases env c =
+  let c' = rewrite_cases c in
+  let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+    c'
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
new file mode 100644
index 00000000..b0de0641
--- /dev/null
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -0,0 +1,39 @@
+val mkAppExplC :
+  Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr
+val mkSubset :
+  Names.name Util.located ->
+  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
+val mkProj1 :
+  Topconstr.constr_expr ->
+  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
+val mkProj2 :
+  Topconstr.constr_expr ->
+  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
+val list_of_local_binders :
+  Topconstr.local_binder list ->
+  (Names.name Util.located * Topconstr.constr_expr) list
+val pr_binder_list :
+  (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
+val rewrite_rec_calls : 'a -> 'b -> 'b
+val rewrite_fixpoint :
+  'a ->
+  'b ->
+  (Names.identifier * (int * Topconstr.recursion_order_expr) *
+   Topconstr.local_binder list * Topconstr.constr_expr *
+   Topconstr.constr_expr) *
+  'c ->
+  (Names.identifier * (int * Topconstr.recursion_order_expr) *
+   Topconstr.local_binder list * Topconstr.constr_expr *
+   Topconstr.constr_expr) *
+  'c
+val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
+val rewrite_cases_aux :
+  Util.loc * Rawterm.rawconstr option *
+  (Rawterm.rawconstr *
+   (Names.name * (Util.loc * Names.inductive * Names.name list) option))
+  list *
+  (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
+   Rawterm.rawconstr)
+  list -> Rawterm.rawconstr
+
+val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
new file mode 100644
index 00000000..104a0a58
--- /dev/null
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -0,0 +1,150 @@
+(************************************************************************)
+(*  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: subtac_pretyping.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+
+open Global
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+
+open Subtac_coercion
+open Subtac_utils
+open Coqlib
+open Printer
+open Subtac_errors
+open Context
+open Eterm
+
+module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion)
+
+open Pretyping
+
+let _ = Pretyping.allow_anonymous_refs := true
+
+type recursion_info = {
+  arg_name: name;
+  arg_type: types; (* A *)
+  args_after : rel_context;
+  wf_relation: constr; (* R : A -> A -> Prop *)
+  wf_proof: constr; (* : well_founded R *)
+  f_type: types; (* f: A -> Set *)
+  f_fulltype: types; (* Type with argument and wf proof product first *)
+}
+
+let my_print_rec_info env t = 
+  str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
+  str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
+  str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
+  str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
+  str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
+  str "Full type: " ++ my_print_constr env t.f_fulltype
+(*   trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
+(* 	   str " and tycon "++ my_print_tycon env tycon ++ *)
+(* 	   str " in environment: " ++ my_print_env env); *)
+
+let merge_evms x y = 
+  Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y
+
+let interp env isevars c tycon = 
+  let j = pretype tycon env isevars ([],[]) c in
+  let evm = evars_of !isevars in    
+    nf_evar evm j.uj_val, nf_evar evm j.uj_type
+
+let find_with_index x l =
+  let rec aux i = function
+      (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
+
+let list_split_at index l = 
+  let rec aux i acc = function
+      hd :: tl when i = index -> (List.rev acc), tl
+    | hd :: tl -> aux (succ i) (hd :: acc) tl
+    | [] -> failwith "list_split_at: Invalid argument"
+  in aux 0 [] l
+
+open Vernacexpr
+
+let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
+let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env
+
+let env_with_binders env isevars l =
+  let rec aux ((env, rels) as acc) = function
+      Topconstr.LocalRawDef ((loc, name), def) :: tl -> 
+	let rawdef = coqintern !isevars env def in
+	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
+	let reldecl = (name, Some coqdef, deftyp) in
+	  aux  (push_rel reldecl env, reldecl :: rels) tl
+    | Topconstr.LocalRawAssum (bl, typ) :: tl ->
+	let rawtyp = coqintern !isevars env typ in
+	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
+	let acc = 
+	  List.fold_left (fun (env, rels) (loc, name) -> 
+			    let reldecl = (name, None, coqtyp) in
+			      (push_rel reldecl env, 
+			       reldecl :: rels))
+	    (env, rels) bl
+	in aux acc tl
+    | [] -> acc
+  in aux (env, []) l
+
+let subtac_process env isevars id l c tycon =
+  let evars () = evars_of !isevars in
+  let _ = trace (str "Creating env with binders") in
+  let env_binders, binders_rel = env_with_binders env isevars l in
+  let _ = trace (str "New env created:" ++ my_print_context env_binders) in
+  let tycon = 
+    match tycon with
+	None -> empty_tycon
+      | Some t -> 
+	  let t = coqintern !isevars env_binders t in
+	  let _ = trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) in
+	  let coqt, ttyp = interp env_binders isevars t empty_tycon in
+	  let _ = trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) in
+	    mk_tycon coqt
+  in    
+  let c = coqintern !isevars env_binders c in
+  let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in
+  let coqc, ctyp = interp env_binders isevars c tycon in
+  let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
+		 str "Coq type: " ++ my_print_constr env_binders ctyp)
+  in
+  let _ = trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) in
+    
+  let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel 
+  and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
+  in
+  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
+  let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
+
+  let _ = trace (str "After evar normalization: " ++ spc () ++
+		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+		 ++ str "Coq type: " ++ my_print_constr env fullctyp) 
+  in
+  let evm = non_instanciated_map env isevars in
+  let _ = trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) in
+    evm, fullcoqc, fullctyp
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
new file mode 100644
index 00000000..97e56ecb
--- /dev/null
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -0,0 +1,12 @@
+open Term
+open Environ
+open Names
+open Sign
+open Evd
+open Global
+open Topconstr
+
+module Pretyping : Pretyping.S
+
+val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
+  constr_expr -> constr_expr option -> evar_map * constr * types
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
new file mode 100644
index 00000000..6c165dad
--- /dev/null
+++ b/contrib/subtac/subtac_utils.ml
@@ -0,0 +1,246 @@
+open Evd
+open Libnames
+open Coqlib
+open Term
+open Names
+open Util
+
+(****************************************************************************)
+(* Library linking *)
+
+let contrib_name = "subtac"
+
+let subtac_dir = [contrib_name]
+let fix_sub_module = "FixSub"
+let utils_module = "Utils"
+let fixsub_module = subtac_dir @ [fix_sub_module]
+let utils_module = subtac_dir @ [utils_module]
+let init_constant dir s = gen_constant contrib_name dir s
+let init_reference dir s = gen_reference contrib_name dir s
+
+let fixsub = lazy (init_constant fixsub_module "Fix_sub")
+let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
+let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
+
+let make_ref s =  Qualid (dummy_loc, (qualid_of_string s))
+let well_founded_ref = make_ref "Init.Wf.Well_founded"
+let acc_ref = make_ref "Init.Wf.Acc"
+let acc_inv_ref = make_ref "Init.Wf.Acc_inv"
+let fix_sub_ref = make_ref "Coq.subtac.FixSub.Fix_sub"
+let lt_wf_ref = make_ref "Coq.Wf_nat.lt_wf"
+let sig_ref = make_ref "Init.Specif.sig"
+let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
+let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
+
+let build_sig () = 
+  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
+    proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
+    elim = init_constant ["Init"; "Specif"] "sig_rec";
+    intro = init_constant ["Init"; "Specif"] "exist";
+    typ = init_constant ["Init"; "Specif"] "sig" }
+
+let sig_ = lazy (build_sig ())
+
+let eqind = lazy (init_constant ["Init"; "Logic"] "eq")
+let eqind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
+let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
+
+let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
+let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+
+let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
+let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+
+let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
+let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
+let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
+let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
+let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
+  
+let existS = lazy (build_sigma_set ())
+
+let prod = lazy (build_prod ())
+
+
+(* orders *)
+let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
+let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
+let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
+let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
+
+let extconstr = Constrextern.extern_constr true (Global.env ())
+let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
+
+open Pp
+
+let my_print_constr = Termops.print_constr_env
+let my_print_constr_expr = Ppconstr.pr_constr_expr
+let my_print_context = Termops.print_rel_context
+let my_print_env = Termops.print_env
+let my_print_rawconstr = Printer.pr_rawconstr_env
+let my_print_evardefs = Evd.pr_evar_defs
+
+let my_print_tycon_type = Evarutil.pr_tycon_type
+
+
+let debug n s = 
+  if !Options.debug then
+    msgnl s
+  else ()
+
+let debug_msg n s = 
+  if !Options.debug then s
+  else mt ()
+
+let trace s = 
+  if !Options.debug then msgnl s
+  else ()
+
+let wf_relations = Hashtbl.create 10
+
+let std_relations () = 
+  let add k v = Hashtbl.add wf_relations k v in
+    add (init_constant ["Init"; "Peano"] "lt")
+      (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
+      
+let std_relations = Lazy.lazy_from_fun std_relations
+
+type binders = Topconstr.local_binder list
+
+let app_opt c e = 
+  match c with
+      Some constr -> constr e
+    | None -> e	
+
+let print_args env args = 
+  Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
+
+let make_existential loc env isevars c =
+  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
+  let (key, args) = destEvar evar in
+    debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+	     print_args env args);
+    evar
+
+let make_existential_expr loc env c =
+  let key = Evarutil.new_untyped_evar () in
+  let evar = Topconstr.CEvar (loc, key) in
+    debug 2 (str "Constructed evar " ++ int key);
+    evar
+
+let string_of_hole_kind = function
+  | ImplicitArg _ -> "ImplicitArg"
+  | BinderType _ -> "BinderType"
+  | QuestionMark -> "QuestionMark"
+  | CasesType -> "CasesType"
+  | InternalHole -> "InternalHole"
+  | TomatchTypeParameter _ -> "TomatchTypeParameter"
+      
+let non_instanciated_map env evd =
+  let evm = evars_of !evd in
+    List.fold_left 
+      (fun evm (key, evi) -> 
+	 let (loc,k) = evar_source key !evd in
+	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
+		      str (string_of_hole_kind k));
+	   match k with 
+	       QuestionMark -> Evd.add evm key evi
+	     | _ ->
+	       debug 2 (str " and is an implicit");
+	       Pretype_errors.error_unsolvable_implicit loc env evm k)
+      Evd.empty (Evarutil.non_instantiated evm)
+
+let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+
+let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
+let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+
+open Tactics
+open Tacticals
+
+let build_dependent_sum l =
+  let rec aux (acc, tac, typ) = function
+      (n, t) :: tl ->
+	let t' = mkLambda (Name n, t, typ) in
+	  trace (str ("treating " ^ string_of_id n) ++
+		 str "assert: " ++ my_print_constr (Global.env ()) t);
+	let tac' = 
+	  tclTHEN (assert_tac true (Name n) t) 
+	    (tclTHENLIST
+	       [intros;
+		(tclTHENSEQ 
+		   [tclTRY (constructor_tac (Some 1) 1 
+		       (Rawterm.ImplicitBindings [mkVar n]));
+		    tac]);
+	       ])
+	in
+	  aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl
+    | [] -> acc, tac, typ
+  in 
+    match l with 
+	(_, hd) :: tl -> aux (hd, intros, hd) tl
+      | [] -> raise (Invalid_argument "build_dependent_sum")
+
+open Proof_type
+open Tacexpr
+
+let mkProj1 a b c = 
+  mkApp (Lazy.force proj1, [| a; b; c |])
+
+let mkProj2 a b c = 
+  mkApp (Lazy.force proj2, [| a; b; c |])
+
+let mk_ex_pi1 a b c =
+  mkApp (Lazy.force ex_pi1, [| a; b; c |])
+
+let mk_ex_pi2 a b c =
+  mkApp (Lazy.force ex_pi2, [| a; b; c |])
+    
+
+let mkSubset name typ prop = 
+  mkApp ((Lazy.force sig_).typ,
+	 [| typ; mkLambda (name, typ, prop) |])
+
+let and_tac l hook =
+  let andc = Coqlib.build_coq_and () in      
+  let rec aux ((accid, goal, tac, extract) as acc) = function
+    | [] -> (* Singleton *) acc
+	
+    | (id, x, elgoal, eltac) :: tl ->
+	let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
+	let proj = fun c -> mkProj2 goal elgoal c in
+	let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
+	  aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac', 
+	       (id, x, elgoal, proj) :: extract) tl
+
+  in
+  let and_proof_id, and_goal, and_tac, and_extract = 
+    match l with
+      | [] -> raise (Invalid_argument "and_tac: empty list of goals")
+      | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
+  in
+  let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
+    Command.start_proof and_proofid goal_kind and_goal
+      (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
+    trace (str "Started and proof");
+    Pfedit.by and_tac;
+    trace (str "Applied and tac")
+      
+
+let destruct_ex ext ex = 
+  let rec aux c acc = 
+    match kind_of_term c with
+	App (f, args) ->
+	  (match kind_of_term f with
+	       Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+		 let (dom, rng) = 
+		   try (args.(0), args.(1))
+		   with _ -> assert(false)
+		 in
+		   (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc)
+	     | _ -> [acc])
+      | _ -> [acc]
+  in aux ex ext
+
+
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
new file mode 100644
index 00000000..92a995c8
--- /dev/null
+++ b/contrib/subtac/subtac_utils.mli
@@ -0,0 +1,85 @@
+open Term
+open Libnames
+open Coqlib
+open Environ
+open Pp
+open Evd
+open Decl_kinds
+open Topconstr
+open Rawterm
+open Util
+open Evarutil
+open Names
+
+val contrib_name : string
+val subtac_dir : string list
+val fix_sub_module : string
+val fixsub_module : string list
+val init_constant : string list -> string -> constr
+val init_reference : string list -> string -> global_reference
+val fixsub : constr lazy_t
+val make_ref : string -> reference
+val well_founded_ref : reference
+val acc_ref : reference
+val acc_inv_ref : reference
+val fix_sub_ref : reference
+val lt_wf_ref : reference
+val sig_ref : reference
+val proj1_sig_ref : reference
+val proj2_sig_ref : reference
+val build_sig : unit -> coq_sigma_data
+val sig_ : coq_sigma_data lazy_t
+val eqind : constr lazy_t
+val eqind_ref : global_reference lazy_t
+val refl_equal_ref : global_reference lazy_t
+val boolind : constr lazy_t
+val sumboolind : constr lazy_t
+val natind : constr lazy_t
+val intind : constr lazy_t
+val existSind : constr lazy_t
+val existS : coq_sigma_data lazy_t
+val prod : coq_sigma_data lazy_t
+
+val well_founded : constr lazy_t
+val fix : constr lazy_t
+val acc : constr lazy_t
+val acc_inv : constr lazy_t
+val extconstr : constr -> constr_expr
+val extsort : sorts -> constr_expr
+val my_print_constr : env -> constr -> std_ppcmds
+val my_print_constr_expr : constr_expr -> std_ppcmds
+val my_print_evardefs : evar_defs -> std_ppcmds
+val my_print_context : env -> std_ppcmds
+val my_print_env : env -> std_ppcmds
+val my_print_rawconstr : env -> rawconstr -> std_ppcmds
+val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
+
+
+val debug : int -> std_ppcmds -> unit
+val debug_msg : int -> std_ppcmds -> std_ppcmds
+val trace : std_ppcmds -> unit
+val wf_relations : (constr, constr lazy_t) Hashtbl.t
+
+type binders = local_binder list
+val app_opt : ('a -> 'a) option -> 'a -> 'a
+val print_args : env -> constr array -> std_ppcmds
+val make_existential : loc -> env -> evar_defs ref -> types -> constr
+val make_existential_expr : loc -> 'a -> 'b -> constr_expr
+val string_of_hole_kind : hole_kind -> string
+val non_instanciated_map : env -> evar_defs ref -> evar_map
+val global_kind : logical_kind
+val goal_kind : locality_flag * goal_object_kind
+val global_fix_kind : logical_kind
+val goal_fix_kind : locality_flag * goal_object_kind
+
+val mkSubset : name -> constr -> constr -> constr
+val mkProj1 : constr -> constr -> constr -> constr
+val mkProj1 : constr -> constr -> constr -> constr
+val mk_ex_pi1 : constr -> constr -> constr -> constr
+val mk_ex_pi1 : constr -> constr -> constr -> constr
+
+val build_dependent_sum : (identifier * types) list -> constr * Proof_type.tactic * types
+val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->  
+  ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
+
+val destruct_ex : constr -> constr -> constr list