Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation.

Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.



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

22 files changed, 729 insertions, 998 deletions

diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 04852da664..8eeb8b642d 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -130,7 +130,7 @@ let mk_open_instance id gl m t=
 	      RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1)
 	| _-> anomaly "can't happen" in
   let ntt=try 
-    Pretyping.understand evmap env (raux m rawt)
+    Pretyping.Default.understand evmap env (raux m rawt)
   with _ -> 
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     Sign.decompose_lam_n_assum m ntt
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index cb43a45ed9..8fcdb5d90a 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -400,7 +400,7 @@ let inspect n =
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
 		     | (sp,kn), "MUTUALINDUCTIVE" ->
 			 add_search2 (Nametab.locate (qualid_of_sp sp))
-			   (Pretyping.understand Evd.empty (Global.env())
+			   (Pretyping.Default.understand Evd.empty (Global.env())
 			      (RRef(dummy_loc, IndRef(kn,0))))
 		     | _ -> failwith ("unexpected value 1 for "^ 
 				      (string_of_id (basename (fst oname)))))
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 19b06a30d3..d2f71bfc2f 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -34,7 +34,7 @@ let get_hyp_by_name g name =
   let evd = project g in
   let env = pf_env g in
   try (let judgment = 
-         Pretyping.understand_judgment 
+         Pretyping.Default.understand_judgment 
           evd env (RVar(zz, name)) in
        ("hyp",judgment.uj_type))
 (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index f973548457..36ebaff11f 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -34,6 +34,7 @@ open Pfedit
 open Topconstr
 open Rawterm
 open Pretyping
+open Pretyping.Default
 open Safe_typing
 open Constrintern
 open Hiddentac
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 14990a24c5..6face72d11 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -21,7 +21,7 @@ End FixPoint.
 
 End Well_founded.
 
-Check Fix_sub.
+(*Check Fix_sub.*)
 
 Notation "'forall' { x : A | P } , Q" :=
   (forall x:{x:A|P}, (fun x => Q) (proj1_sig x))
diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli
new file mode 100644
index 0000000000..671d6f3619
--- /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/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4
index f435219936..095e5fafc9 100644
--- a/contrib/subtac/g_eterm.ml4
+++ b/contrib/subtac/g_eterm.ml4
@@ -23,5 +23,5 @@ TACTIC EXTEND eterm
   [ "eterm" ] -> [ 
     (fun gl ->
        let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in
-         Eterm.etermtac (Global.env ()) (evm, t) gl) ]
+         Eterm.etermtac (evm, t) gl) ]
 END
diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/g_subtac.ml4
index 43214c87bd..d9c7a8c023 100644
--- a/contrib/subtac/sparser.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -49,7 +49,7 @@ GEXTEND Gram
     ;
   END
 
-(* type wf_proof_type_argtype = (Scoq.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
+(* type wf_proof_type_argtype = (Subtac_utils.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
 
 (* let (wit_subtac_wf_proof_type : wf_proof_type_argtype), *)
 (*   (globwit_subtac_wf_proof_type : wf_proof_type_argtype), *)
@@ -63,7 +63,7 @@ let (wit_subtac_gallina_loc : gallina_loc_argtype),
   (rawwit_subtac_gallina_loc : gallina_loc_argtype) =
   Genarg.create_arg "subtac_gallina_loc"
 
-(* type subtac_recdef_argtype = (Scoq.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
+(* type subtac_recdef_argtype = (Subtac_utils.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
 
 (* let (wit_subtac_recdef : subtac_recdef_argtype), *)
 (*   (globwit_subtac_recdef : subtac_recdef_argtype), *)
diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml
deleted file mode 100644
index d338c34452..0000000000
--- a/contrib/subtac/interp.ml
+++ /dev/null
@@ -1,666 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-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 Pretyping
-
-open Subtac_coercion
-open Scoq
-open Coqlib
-open Printer
-open Subtac_errors
-open Context
-open Eterm
-
-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
-
-(* Taken from pretyping.ml *)
-let evd_comb0 f isevars =
-  let (evd',x) = f !isevars in
-  isevars := evd';
-  x
-let evd_comb1 f isevars x =
-  let (evd',y) = f !isevars x in
-  isevars := evd';
-  y
-let evd_comb2 f isevars x y =
-  let (evd',z) = f !isevars x y in
-  isevars := evd';
-  z
-let evd_comb3 f isevars x y z =
-  let (evd',t) = f !isevars x y z in
-  isevars := evd';
-  t
-
-(************************************************************************)
-(* This concerns Cases *)
-open Declarations
-open Inductive
-open Inductiveops
-
-(************************************************************************)
-
-let mt_evd = Evd.empty
-
-let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
-
-(* Utilisé pour inférer le prédicat des Cases *)
-(* Semble exagérement fort *)
-(* Faudra préférer une unification entre les types de toutes les clauses *)
-(* et autoriser des ? à rester dans le résultat de l'unification *)
-
-let evar_type_fixpoint loc env isevars lna lar vdefj =
-  let lt = Array.length vdefj in 
-    if Array.length lar = lt then 
-      for i = 0 to lt-1 do 
-        if not (e_cumul env isevars (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env (evars_of !isevars)
-            i lna vdefj lar
-      done
-
-let check_branches_message loc env isevars c (explft,lft) = 
-  for i = 0 to Array.length explft - 1 do
-    if not (e_cumul env isevars lft.(i) explft.(i)) then 
-      let sigma = evars_of !isevars in
-      error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
-  done
-
-(* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon loc env isevars j = function
-   | None -> j
-   | Some typ -> evd_comb2 (Subtac_coercion.inh_conv_coerce_to loc env) isevars j typ
-
-let push_rels vars env = List.fold_right push_rel vars env
-
-let strip_meta id = (* For Grammar v7 compatibility *)
-  let s = string_of_id id in
-  if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
-  else id
-
-let pretype_id loc env (lvar,unbndltacvars) id =
-  let id = strip_meta id in (* May happen in tactics defined by Grammar *)
-  try
-    let (n,typ) = lookup_rel_id id (rel_context env) in
-    { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
-  with Not_found ->
-  try
-    List.assoc id lvar
-  with Not_found ->
-  try
-    let (_,_,typ) = lookup_named id env in
-    { uj_val  = mkVar id; uj_type = typ }
-  with Not_found ->
-  try (* To build a nicer ltac error message *)
-    match List.assoc id unbndltacvars with
-      | None -> user_err_loc (loc,"",
-	  str (string_of_id id ^ " ist not bound to a term"))
-      | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
-  with Not_found ->
-    error_var_not_found_loc loc id
-
-(* make a dependent predicate from an undependent one *)
-
-let make_dep_of_undep env (IndType (indf,realargs)) pj =
-  let n = List.length realargs in
-  let rec decomp n p =
-    if n=0 then p else
-      match kind_of_term p with
-	| Lambda (_,_,c) -> decomp (n-1) c
-	| _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) 
-  in
-  let sign,s = decompose_prod_n n pj.uj_type in
-  let ind = build_dependent_inductive env indf in
-  let s' = mkProd (Anonymous, ind, s) in
-  let ccl = lift 1 (decomp n pj.uj_val) in
-  let ccl' = mkLambda (Anonymous, ind, ccl) in
-  {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
-
-(*************************************************************************)
-(* Main pretyping function                                               *)
-
-let pretype_ref isevars env ref = 
-  let c = constr_of_global ref in
-  make_judge c (Retyping.get_type_of env Evd.empty c)
-
-let pretype_sort = function
-  | RProp c -> judge_of_prop_contents c
-  | RType _ -> judge_of_new_Type ()
-
-let my_print_tycon env = function
-    Some t -> my_print_constr env t
-  | None -> str "None"
-
-(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
-(* in environment [env], with existential variables [(evars_of isevars)] and *)
-(* the type constraint tycon *)
-let rec pretype tycon env isevars lvar c = 
-  trace (str "pretype for " ++ (my_print_rawconstr env c) ++
-	   str " and tycon "++ my_print_tycon env tycon ++
-	   str " in environment: " ++ my_print_env env);
-  match c with
-
-  | RRef (loc,ref) ->
-      inh_conv_coerce_to_tycon loc env isevars
-	(pretype_ref isevars env ref)
-	tycon
-
-  | RVar (loc, id) ->
-      inh_conv_coerce_to_tycon loc env isevars
-	(pretype_id loc env lvar id)
-	tycon
-
-  | REvar (loc, ev, instopt) ->
-      (* Ne faudrait-il pas s'assurer que hyps est bien un
-      sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-      let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
-      let args = match instopt with
-        | None -> instance_from_named_context hyps
-        | Some inst -> failwith "Evar subtitutions not implemented" in
-      let c = mkEvar (ev, args) in
-      let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
-      inh_conv_coerce_to_tycon loc env isevars j tycon
-
-  | RPatVar (loc,(someta,n)) -> 
-      anomaly "Found a pattern variable in a rawterm to type"
-	   
-  | RHole (loc,k) ->
-      let ty =
-        match tycon with 
-          | Some ty -> ty
-          | None ->
-              e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
-      { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
-
-  | RRec (loc,fixkind,names,bl,lar,vdef) ->
-      let rec type_bl env ctxt = function
-          [] -> ctxt
-        | (na,None,ty)::bl ->
-            let ty' = pretype_type empty_valcon env isevars lvar ty in
-            let dcl = (na,None,ty'.utj_val) in
-            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
-        | (na,Some bd,ty)::bl ->
-            let ty' = pretype_type empty_valcon env isevars lvar ty in
-            let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
-            let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
-            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
-      let ctxtv = Array.map (type_bl env empty_rel_context) bl in
-      let larj =
-        array_map2
-          (fun e ar ->
-            pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
-          ctxtv lar in
-      let lara = Array.map (fun a -> a.utj_val) larj in
-      let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
-      let nbfix = Array.length lar in
-      let names = Array.map (fun id -> Name id) names in
-      (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-      let newenv = push_rec_types (names,ftys,[||]) env in
-      let vdefj =
-	array_map2_i 
-	  (fun i ctxt def ->
-            (* we lift nbfix times the type in tycon, because of
-	     * the nbfix variables pushed to newenv *)
-            let (ctxt,ty) =
-              decompose_prod_n_assum (rel_context_length ctxt)
-                (lift nbfix ftys.(i)) in
-            let nenv = push_rel_context ctxt newenv in
-            let j = pretype (mk_tycon ty) nenv isevars lvar def in
-            { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
-              uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
-          ctxtv vdef in
-      evar_type_fixpoint loc env isevars names ftys vdefj;
-      let fixj =
-	match fixkind with
-	  | RFix (vn,i) ->
-	      let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in
-	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkFix fix) ftys.(i)
-	  | RCoFix i -> 
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
-	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkCoFix cofix) ftys.(i) in
-      inh_conv_coerce_to_tycon loc env isevars fixj tycon
-
-  | RSort (loc,s) ->
-      inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
-
-  | RApp (loc,f,args) -> 
-      let fj = pretype empty_tycon env isevars lvar f in
-      let floc = loc_of_rawconstr f in
-      let rec apply_rec env n resj = function
-	| [] -> resj
-	| c::rest ->
-	    let argloc = loc_of_rawconstr c in
-	    let resj = evd_comb1 (inh_app_fun env) isevars resj in
-            let resty =
-              whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
-	      match kind_of_term resty with
-	      | Prod (na,c1,c2) ->
-		  let hj = pretype (mk_tycon c1) env isevars lvar c in
-		  let newresj =
-      		    { uj_val = applist (j_val resj, [j_val hj]);
-		      uj_type = subst1 hj.uj_val c2 } in
-		  apply_rec env (n+1) newresj rest
-
-	      | _ ->
-		  let hj = pretype empty_tycon env isevars lvar c in
-		  error_cant_apply_not_functional_loc 
-		    (join_loc floc argloc) env (evars_of !isevars)
-	      	    resj [hj]
-      in let resj = apply_rec env 1 fj args in
-      inh_conv_coerce_to_tycon loc env isevars resj tycon
-
-  | RLambda(loc,name,c1,c2)      ->
-      let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
-      let dom_valcon = valcon_of_tycon dom in
-      let j = pretype_type dom_valcon env isevars lvar c1 in
-      let var = (name,None,j.utj_val) in
-      let j' = pretype rng (push_rel var env) isevars lvar c2 in 
-      judge_of_abstraction env name j j'
-
-  | RProd(loc,name,c1,c2)        ->
-      let j = pretype_type empty_valcon env isevars lvar c1 in
-      let var = (name,j.utj_val) in
-      let env' = push_rel_assum var env in
-      let j' = pretype_type empty_valcon env' isevars lvar c2 in
-      let resj =
-	try judge_of_product env name j j'
-	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
-      inh_conv_coerce_to_tycon loc env isevars resj tycon
-	
-  | RLetIn(loc,name,c1,c2)      ->
-      let j = pretype empty_tycon env isevars lvar c1 in
-      let t = refresh_universes j.uj_type in
-      let var = (name,Some j.uj_val,t) in
-        let tycon = option_app (lift 1) tycon in
-      let j' = pretype tycon (push_rel var env) isevars lvar c2 in
-      { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
-	uj_type = subst1 j.uj_val j'.uj_type }
-
-  | RLetTuple (loc,nal,(na,po),c,d) ->
-      let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs)) = 
-	try find_rectype env (evars_of !isevars) cj.uj_type
-	with Not_found ->
-	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
-      in
-      let cstrs = get_constructors env indf in
-      if Array.length cstrs <> 1 then
-        user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
-      let cs = cstrs.(0) in
-      if List.length nal <> cs.cs_nargs then
-        user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
-      let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
-        (List.rev nal) cs.cs_args in
-      let env_f = push_rels fsign env in
-      (* Make dependencies from arity signature impossible *)
-      let arsgn,_ = get_arity env indf in
-      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
-      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
-      let nar = List.length arsgn in
-      (match po with
-	 | Some p ->
-             let env_p = push_rels psign env in
-             let pj = pretype_type empty_valcon env_p isevars lvar p in
-             let ccl = nf_evar (evars_of !isevars) pj.utj_val in
-	     let psign = make_arity_signature env true indf in (* with names *)
-	     let p = it_mkLambda_or_LetIn ccl psign in
-             let inst = 
-	       (Array.to_list cs.cs_concl_realargs)
-	       @[build_dependent_constructor cs] in
-	     let lp = lift cs.cs_nargs p in
-             let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
-	     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
-	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env LetStyle mis in
-	       mkCase (ci, p, cj.uj_val,[|f|]) in 
-	     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
-
-	 | None -> 
-             let tycon = option_app (lift cs.cs_nargs) tycon in
-	     let fj = pretype tycon env_f isevars lvar d in
-	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-	     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
-             let ccl =
-               if noccur_between 1 cs.cs_nargs ccl then
-                 lift (- cs.cs_nargs) ccl 
-               else
-                 error_cant_find_case_type_loc loc env (evars_of !isevars) 
-                   cj.uj_val in
-             let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env LetStyle mis in
-	       mkCase (ci, p, cj.uj_val,[|f|] ) 
-	     in
-	     { uj_val = v; uj_type = ccl })
-
-  | RIf (loc,c,(na,po),b1,b2) ->
-      let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs)) = 
-	try find_rectype env (evars_of !isevars) cj.uj_type
-	with Not_found ->
-	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
-      let cstrs = get_constructors env indf in 
-      if Array.length cstrs <> 2 then
-        user_err_loc (loc,"",
-	  str "If is only for inductive types with two constructors");
-
-      (* Make dependencies from arity signature possible ! *)
-      let arsgn,_ = get_arity env indf in
-      let arsgn = List.map (fun (n,b,t) -> 
-			      debug 2 (str "If case arg: " ++ Nameops.pr_name n);
-			      (n,b,t)) arsgn in
-      let nar = List.length arsgn in
-      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
-      let pred,p = match po with
-	| Some p ->
-	    let env_p = push_rels psign env in
-            let pj = pretype_type empty_valcon env_p isevars lvar p in
-            let ccl = nf_evar (evars_of !isevars) pj.utj_val in
-	    let pred = it_mkLambda_or_LetIn ccl psign in
-	    pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
-	| None -> 
-	    let p = match tycon with
-	    | Some ty -> ty
-	    | None ->
-                e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
-	    in
-	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-      let f cs b =
-	let n = rel_context_length cs.cs_args in
-	let pi = liftn n 2 pred in
-	let pi = beta_applist (pi, [build_dependent_constructor cs]) in
-	let csgn = 
-	  List.map (fun (n,b,t) ->
-		      match n with 
-			  Name _ -> (n, b, t)
-			| Anonymous -> (Name (id_of_string "H"), b, t))
-	    cs.cs_args 
-	in
-	let env_c = push_rels csgn env in 
-	let bj = pretype (Some pi) env_c isevars lvar b in
-	it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
-      let b1 = f cstrs.(0) b1 in
-      let b2 = f cstrs.(1) b2 in
-      let pred = nf_evar (evars_of !isevars) pred in
-      let p = nf_evar (evars_of !isevars) p in
-      let v =
-	let mis,_ = dest_ind_family indf in
-	let ci = make_default_case_info env IfStyle mis in
-	mkCase (ci, pred, cj.uj_val, [|b1;b2|])
-      in
-      { uj_val = v; uj_type = p }
-
-  | RCases (loc,po,tml,eqns) ->
-      Cases.compile_cases loc
-	((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
-	tycon env (* loc *) (po,tml,eqns)
-    
-  | RCast(loc,c,k,t) ->
-      let tj = pretype_type empty_tycon env isevars lvar t in
-      let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
-      (* User Casts are for helping pretyping, experimentally not to be kept*)
-      (* ... except for Correctness *)
-      let v = mkCast (cj.uj_val, k, tj.utj_val) in
-      let cj = { uj_val = v; uj_type = tj.utj_val } in
-      inh_conv_coerce_to_tycon loc env isevars cj tycon
-
-  | RDynamic (loc,d) ->
-    if (tag d) = "constr" then
-      let c = Pretyping.constr_out d in
-      let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
-      j
-      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
-    else
-      user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
-
-(* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
-and pretype_type valcon env isevars lvar = function
-  | RHole loc ->
-      (match valcon with
-	 | Some v ->
-             let s =
-               let sigma = evars_of !isevars in
-               let t = Retyping.get_type_of env sigma v in
-               match kind_of_term (whd_betadeltaiota env sigma t) with
-                 | Sort s -> s
-                 | Evar v when is_Type (existential_type sigma v) -> 
-                     evd_comb1 (define_evar_as_sort) isevars v
-                 | _ -> anomaly "Found a type constraint which is not a type"
-             in
-	     { utj_val = v;
-	       utj_type = s }
-	 | None ->
-	     let s = new_Type_sort () in
-	     { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
-	       utj_type = s})
-  | c ->
-      let j = pretype empty_tycon env isevars lvar c in
-      let loc = loc_of_rawconstr c in
-      let tj = evd_comb1 (inh_coerce_to_sort loc env) isevars j in
-      match valcon with
-	| None -> tj
-	| Some v ->
-	    if e_cumul env isevars v tj.utj_val then tj
-	    else
-	      (debug 2 (str "here we are");
-	       error_unexpected_type_loc
-                 (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v)
-
-
-
-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
-    j.uj_val, 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
-
-let pretype_gen isevars env lvar kind c =
-  let c' = match kind with
-  | OfType exptyp ->
-    let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-    (pretype tycon env isevars lvar c).uj_val
-  | IsType ->
-    (pretype_type empty_valcon env isevars lvar c).utj_val in
-  nf_evar (evars_of !isevars) c'
-
-(* [check_evars] fails if some unresolved evar remains *)
-(* it assumes that the defined existentials have already been substituted
-   (should be done in unsafe_infer and unsafe_infer_type) *)
-
-let check_evars env initial_sigma isevars c =
-  let sigma = evars_of !isevars in
-  let rec proc_rec c =
-    match kind_of_term c with
-      | Evar (ev,args) ->
-          assert (Evd.in_dom sigma ev);
-	  if not (Evd.in_dom initial_sigma ev) then
-            let (loc,k) = evar_source ev !isevars in
-	    let _ = trace (str "Evar " ++ int ev ++ str " not solved, applied to args : " ++
-			   Scoq.print_args env args ++ str " in evar map: " ++
-			   Evd.pr_evar_map sigma) 
-	    in
-	    error_unsolvable_implicit loc env sigma k
-      | _ -> iter_constr proc_rec c
-  in
-  proc_rec c(*;
-  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-  if pbs <> [] then begin
-    pperrnl
-      (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-      prlist_with_sep fnl
-        (fun  (pb,c1,c2) ->
-          Termops.print_constr c1 ++
-          (if pb=Reduction.CUMUL then str " <="++ spc()
-           else str" =="++spc()) ++
-          Termops.print_constr c2)
-        pbs ++ fnl())
-  end*)
-
-(* TODO: comment faire remonter l'information si le typage a resolu des
-       variables du sigma original. il faudrait que la fonction de typage
-       retourne aussi le nouveau sigma...
-*)
-
-let understand_judgment isevars env c =
-  let j = pretype empty_tycon env isevars ([],[]) c in
-  let j = j_nf_evar (evars_of !isevars) j in
-  check_evars env (Evd.evars_of !isevars) isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-  j
-
-(* Raw calls to the unsafe inference machine: boolean says if we must
-   fail on unresolved evars; the unsafe_judgment list allows us to
-   extend env with some bindings *)
-
-let ise_pretype_gen fail_evar isevars env lvar kind c : Evd.open_constr =
-  let c = pretype_gen isevars env lvar kind c in
-  if fail_evar then check_evars env (Evd.evars_of !isevars) isevars c;
-    let c = nf_evar (evars_of !isevars) c in
-    let evm = non_instanciated_map env isevars in
-      (evm, c)
-
-(** Entry points of the high-level type synthesis algorithm *)
-
-let understand_gen kind isevars env c =
-  ise_pretype_gen false isevars env ([],[]) kind c
-
-let understand isevars env ?expected_type:exptyp c =
-  ise_pretype_gen false isevars env ([],[]) (OfType exptyp) c
-
-let understand_type isevars env c =
-  ise_pretype_gen false isevars env ([],[]) IsType c
-
-let understand_ltac isevars env lvar kind c =
-  ise_pretype_gen false isevars env lvar kind c
-
-let understand_tcc isevars env ?expected_type:exptyp c =
-  ise_pretype_gen false isevars env ([],[]) (OfType exptyp) c
-
-
-    
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index c34338236d..12755960ef 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -33,7 +33,7 @@ open Dyn
 open Vernacexpr
 
 open Subtac_coercion
-open Scoq
+open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
@@ -46,7 +46,7 @@ let require_library dirpath =
 
 let subtac_one_fixpoint env isevars (f, decl) = 
   let ((id, n, bl, typ, body), decl) = 
-    Interp_fixpoint.rewrite_fixpoint env [] (f, 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)
@@ -125,13 +125,13 @@ let subtac (loc, command) =
 	  let isevars = ref (create_evar_defs Evd.empty) in
 	    (match expr with
 		 ProveBody (bl, c) -> 
-		   let evm, c, ctyp = Interp.subtac_process env isevars id bl c None in
+		   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 = Interp.subtac_process env isevars id bl c tycon in
+		   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;
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
new file mode 100644
index 0000000000..a0d2fb2b9e
--- /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
index 015eb5d171..c605314018 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -22,7 +22,7 @@ open Retyping
 open Evd
 
 open Global
-open Scoq
+open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
@@ -33,340 +33,343 @@ open Pp
 let pair_of_array a = (a.(0), a.(1))
 let make_name s = Name (id_of_string s)
 
-exception NoCoercion
+module Coercion = struct
 
-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
+  exception NoCoercion
 
+  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 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 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
+  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
 
-and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
-    : (Term.constr -> Term.constr) option 
-    =
-  trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
-	 str " and "++ my_print_constr env y);
+  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
 
-  let rec coerce_unify env x y =
-    if e_cumul env isevars x y then (
-      trace (str "Unified " ++ (my_print_constr env x) ++ 
+  and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
+      : (Term.constr -> Term.constr) option 
+      =
+    trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
 	     str " and "++ my_print_constr env y);
-      None
-    ) else coerce' env x y (* head recutions needed *)
-  and coerce' env x y : (Term.constr -> Term.constr) option =
-    let subco () = subset_coerce env 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' ->
-		   let len = Array.length l in
-		   let existS = Lazy.force existS in
-		     if len = Array.length l' && len = 2
-		       && i = i' && i = Term.destInd existS.typ 
-		     then
-		       begin (* Sigma types *)
-			 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 remove_head c = 
-			   let (_, _, x) = Term.destProd c in
-			     x
-			 in
-			 let b, b' = remove_head pb, remove_head 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 -> 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, [| x ; y |]))
-		       end
-		     else subco ()
-	       | _ ->  subco ())
-	| _, _ ->  subco ()
 
-  and subset_coerce env 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 NoCoercion
-  in coerce_unify env x y
+    let rec coerce_unify env x y =
+      if e_cumul env isevars x y then (
+	trace (str "Unified " ++ (my_print_constr env x) ++ 
+		 str " and "++ my_print_constr env y);
+	None
+      ) else coerce' env x y (* head recutions needed *)
+    and coerce' env x y : (Term.constr -> Term.constr) option =
+      let subco () = subset_coerce env 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' ->
+		     let len = Array.length l in
+		     let existS = Lazy.force existS in
+		       if len = Array.length l' && len = 2
+			 && i = i' && i = Term.destInd existS.typ 
+		       then
+			 begin (* Sigma types *)
+			   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 remove_head c = 
+			     let (_, _, x) = Term.destProd c in
+			       x
+			   in
+			   let b, b' = remove_head pb, remove_head 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 -> 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, [| x ; y |]))
+			 end
+		       else subco ()
+		 | _ ->  subco ())
+	  | _, _ ->  subco ()
 
-let coerce_itf loc env isevars hj c1 =
-  let {uj_val = v; uj_type = t} = hj in
-  let evars = ref isevars in
-  let coercion = coerce loc env evars t c1 in
-    !evars, {uj_val = app_opt coercion v;
-	     uj_type = t}
-      
-(* Taken from pretyping/coercion.ml *)
+    and subset_coerce env 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 NoCoercion
+    in coerce_unify env x y
 
-(* Typing operations dealing with coercions *)
+  let coerce_itf loc env isevars hj c1 =
+    let {uj_val = v; uj_type = t} = hj in
+    let evars = ref isevars in
+    let coercion = coerce loc env evars t c1 in
+      !evars, {uj_val = app_opt coercion v;
+	       uj_type = t}
+	
+  (* Taken from pretyping/coercion.ml *)
 
-let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+  (* Typing operations dealing with coercions *)
 
-(* 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
+  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
 
-exception NoCoercion
+  (* 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
+  (* appliquer le chemin de coercions de patterns 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
+  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
 
-(* appliquer le chemin de coercions p à hj *)
+  (* 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
 
-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"
+  (* appliquer le chemin de coercions p à hj *)
 
-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 NoCoercion ->
-	     (isevars,j))
+  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_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_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 NoCoercion ->
+		 (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_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_fail env isevars c1 hj =
-  let hj' =
-    try 
-      let t1,i1 = class_of1 env (evars_of isevars) c1 in
-      let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
-      let p = lookup_path_between (i2,i1) in
-      apply_coercion env p hj t2
-    with Not_found -> raise NoCoercion 
-  in
-  try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
-  with Reduction.NotConvertible -> raise NoCoercion
+  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 rec inh_conv_coerce_to_fail env isevars hj c1 =
-  let {uj_val = v; uj_type = t} = hj in
-  try (the_conv_x_leq env t c1 isevars, hj)
-  with Reduction.NotConvertible ->
-    (try 
-      inh_coerce_to_fail env isevars c1 hj
-    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' = whd_betadeltaiota env (evars_of isevars) v in
-             let (evd',b) =
-               match kind_of_term v' with
-                 | Lambda (_,v1,v2) ->
-                     (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
-                     with Reduction.NotConvertible -> (isevars, false))
-                 | _  -> (isevars,false) in
-             if b
-             then 
-	       let (x,v1,v2) = destLambda v' in
-               let env1 = push_rel (x,None,v1) env in
-               let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
+  let inh_coerce_to_fail env isevars c1 hj =
+    let hj' =
+      try 
+	let t1,i1 = class_of1 env (evars_of isevars) c1 in
+	let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
+	let p = lookup_path_between (i2,i1) in
+	  apply_coercion env p hj t2
+      with Not_found -> raise NoCoercion 
+    in
+      try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+      with Reduction.NotConvertible -> raise NoCoercion
+
+  let rec inh_conv_coerce_to_fail env isevars hj c1 =
+    let {uj_val = v; uj_type = t} = hj in
+      try (the_conv_x_leq env t c1 isevars, hj)
+      with Reduction.NotConvertible ->
+	(try 
+	   inh_coerce_to_fail env isevars c1 hj
+	 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' = whd_betadeltaiota env (evars_of isevars) v in
+		    let (evd',b) =
+		      match kind_of_term v' with
+			| Lambda (_,v1,v2) ->
+			    (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
+			     with Reduction.NotConvertible -> (isevars, false))
+			| _  -> (isevars,false) in
+		      if b
+		      then 
+			let (x,v1,v2) = destLambda v' in
+			let env1 = push_rel (x,None,v1) env in
+			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
 			  {uj_val = v2; uj_type = t2 } u2 in
-               (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
-                 uj_type = mkProd (x, v1, h2.uj_type) })
-             else 
-               (* 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',h1) =
-		 inh_conv_coerce_to_fail env1 isevars
-		   {uj_val = mkRel 1; uj_type = (lift 1 u1) }
-                   (lift 1 t1) in
-               let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
-			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
-                           uj_type = subst1 h1.uj_val t2 }
+			  (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
+				   uj_type = mkProd (x, v1, h2.uj_type) })
+		      else 
+			(* 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',h1) =
+			  inh_conv_coerce_to_fail env1 isevars
+			    {uj_val = mkRel 1; uj_type = (lift 1 u1) }
+			    (lift 1 t1) in
+			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
+			  { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
+                            uj_type = subst1 h1.uj_val t2 }
                           u2
-	       in
-               (evd'',
-                { uj_val = mkLambda (name, u1, h2.uj_val);
-                  uj_type = mkProd (name, u1, h2.uj_type) })
-	 | _ -> raise NoCoercion))
+			in
+			  (evd'',
+			   { uj_val = mkLambda (name, u1, h2.uj_val);
+			     uj_type = mkProd (name, u1, h2.uj_type) })
+		| _ -> 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 t =
-  trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++ 
-	   str " and "++ my_print_constr env t);
-  let (evd',cj') = 
-    try 
-      inh_conv_coerce_to_fail env isevars cj t
-    with NoCoercion ->
-      try
-	coerce_itf loc env isevars cj t
+  (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
+  let inh_conv_coerce_to loc env isevars cj t =
+    trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++ 
+	     str " and "++ my_print_constr env t);
+    let (evd',cj') = 
+      try 
+	inh_conv_coerce_to_fail env isevars cj t
       with NoCoercion ->
-	let sigma = evars_of isevars in
-	  debug 2 (str "No coercion found");
-	  error_actual_type_loc loc env sigma cj t
-  in
-  (evd',{ uj_val = cj'.uj_val; uj_type = t })
+	try
+	  coerce_itf loc env isevars cj t
+	with NoCoercion ->
+	  let sigma = evars_of isevars in
+	    debug 2 (str "No coercion found");
+	    error_actual_type_loc loc env sigma cj t
+    in
+      (evd',{ uj_val = cj'.uj_val; uj_type = t })
+end
diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli
new file mode 100644
index 0000000000..53a8d21338
--- /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
index 34eff9a176..64aee76119 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -34,15 +34,14 @@ open Mod_subst
 open Printer
 open Inductiveops
 open Syntax_def
-open Pretyping
 
 open Tacinterp
 open Vernacexpr
 open Notation
 
-open Interp
-open Scoq
-
+module SPretyping = Subtac_pretyping.Pretyping
+open Subtac_utils
+open Pretyping
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -50,11 +49,10 @@ open Scoq
 let interp_gen kind isevars env 
                ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
                c =
-  let c' = Constrintern.intern_gen (kind=Pretyping.IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
-  let c'' = Interp_fixpoint.rewrite_cases c' in
-    understand_gen kind isevars env 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 c' in
+    Evd.evars_of !isevars, SPretyping.pretype_gen isevars env ([],[]) kind c''
     
-
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c 
 
@@ -65,10 +63,14 @@ 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 =
-  understand_tcc isevars env (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+  SPretyping.pretype_gen isevars env ([], []) (OfType None) 
+    (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
 
 let interp_constr_judgment isevars env c =
-  understand_judgment isevars env (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+  let s, j = SPretyping.understand_judgment_tcc (Evd.evars_of !isevars) env
+    (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+  in 
+    Evd.create_evar_defs s, j
 
 (* try to find non recursive definitions *)
 
@@ -118,7 +120,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
   and protos = List.map (fun ((f, n, _, _, _),_) -> f,n) lnameargsardef
   in 
   let lnameargsardef = 
-    List.map (fun (f, d) -> Interp_fixpoint.rewrite_fixpoint env0 protos (f, d))
+    List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))
       lnameargsardef
   in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
new file mode 100644
index 0000000000..23a03290c8
--- /dev/null
+++ b/contrib/subtac/subtac_command.mli
@@ -0,0 +1,103 @@
+module SPretyping :
+  sig
+    module Cases :
+      sig
+        val compile_cases :
+          Util.loc ->
+          (Evarutil.type_constraint ->
+           Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment) *
+          Evd.evar_defs ref ->
+          Evarutil.type_constraint ->
+          Environ.env ->
+          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 -> Environ.unsafe_judgment
+      end
+    val understand_tcc :
+      Evd.evar_map ->
+      Environ.env ->
+      ?expected_type:Term.types -> Rawterm.rawconstr -> Evd.open_constr
+    val understand_ltac :
+      Evd.evar_map ->
+      Environ.env ->
+      Pretyping.var_map * Pretyping.unbound_ltac_var_map ->
+      Pretyping.typing_constraint ->
+      Rawterm.rawconstr -> Evd.evar_defs * Term.constr
+    val understand :
+      Evd.evar_map ->
+      Environ.env ->
+      ?expected_type:Term.types -> Rawterm.rawconstr -> Term.constr
+    val understand_type :
+      Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
+    val understand_gen :
+      Pretyping.typing_constraint ->
+      Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
+    val understand_judgment :
+      Evd.evar_map ->
+      Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment
+    val understand_judgment_tcc :
+      Evd.evar_map ->
+      Environ.env ->
+      Rawterm.rawconstr -> Evd.evar_map * Environ.unsafe_judgment
+    val pretype :
+      Evarutil.type_constraint ->
+      Environ.env ->
+      Evd.evar_defs ref ->
+      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
+      Rawterm.rawconstr -> Environ.unsafe_judgment
+    val pretype_type :
+      Evarutil.val_constraint ->
+      Environ.env ->
+      Evd.evar_defs ref ->
+      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
+      Rawterm.rawconstr -> Environ.unsafe_type_judgment
+    val pretype_gen :
+      Evd.evar_defs ref ->
+      Environ.env ->
+      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
+      Pretyping.typing_constraint -> Rawterm.rawconstr -> Term.constr
+  end
+val interp_gen :
+  Pretyping.typing_constraint ->
+  Evd.evar_defs ref ->
+  Environ.env ->
+  ?impls:Constrintern.full_implicits_env ->
+  ?allow_soapp:bool ->
+  ?ltacvars:Constrintern.ltac_sign ->
+  Topconstr.constr_expr -> Evd.evar_map * Term.constr
+val interp_constr :
+  Evd.evar_defs ref ->
+  Environ.env -> Topconstr.constr_expr -> Evd.evar_map * Term.constr
+val interp_type :
+  Evd.evar_defs ref ->
+  Environ.env ->
+  ?impls:Constrintern.full_implicits_env ->
+  Topconstr.constr_expr -> Evd.evar_map * Term.constr
+val interp_casted_constr :
+  Evd.evar_defs ref ->
+  Environ.env ->
+  ?impls:Constrintern.full_implicits_env ->
+  Topconstr.constr_expr -> Term.types -> Evd.evar_map * Term.constr
+val interp_open_constr :
+  Evd.evar_defs ref -> Environ.env -> Topconstr.constr_expr -> Term.constr
+val interp_constr_judgment :
+  Evd.evar_defs ref ->
+  Environ.env ->
+  Topconstr.constr_expr -> Evd.evar_defs * Environ.unsafe_judgment
+val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
+val collect_non_rec :
+  Environ.env ->
+  Names.identifier list ->
+  ('a * Term.types) list ->
+  'b list ->
+  'c list ->
+  (Names.identifier * ('a * Term.types) * 'b) list *
+  (Names.identifier array * ('a * Term.types) array * 'b array * 'c array)
+val recursive_message : Libnames.global_reference array -> Pp.std_ppcmds
+val build_recursive :
+  (Topconstr.fixpoint_expr * Vernacexpr.decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_errors.mli b/contrib/subtac/subtac_errors.mli
new file mode 100644
index 0000000000..8d75b9c017
--- /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/interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 8191357091..c668c3503b 100644
--- a/contrib/subtac/interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -23,7 +23,7 @@ open Dyn
 open Topconstr
 
 open Subtac_coercion
-open Scoq
+open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
new file mode 100644
index 0000000000..5a84b27730
--- /dev/null
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -0,0 +1,42 @@
+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 abstract_constr_expr_bl :
+  Topconstr.constr_expr ->
+  (Names.name Util.located * Topconstr.constr_expr) list ->
+  Topconstr.constr_expr
+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 : Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
new file mode 100644
index 0000000000..8dd6f9b8fe
--- /dev/null
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -0,0 +1,146 @@
+(************************************************************************)
+(*  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$ *)
+
+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
+
+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
+    j.uj_val, 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 0000000000..97e56ecb24
--- /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/scoq.ml b/contrib/subtac/subtac_utils.ml
index eb9888c161..eb9888c161 100644
--- a/contrib/subtac/scoq.ml
+++ b/contrib/subtac/subtac_utils.ml
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
new file mode 100644
index 0000000000..5bbd4639eb
--- /dev/null
+++ b/contrib/subtac/subtac_utils.mli
@@ -0,0 +1,53 @@
+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 -> Term.constr
+val init_reference : string list -> string -> Libnames.global_reference
+val fixsub : Term.constr lazy_t
+val make_ref : string -> Libnames.reference
+val well_founded_ref : Libnames.reference
+val acc_ref : Libnames.reference
+val acc_inv_ref : Libnames.reference
+val fix_sub_ref : Libnames.reference
+val lt_wf_ref : Libnames.reference
+val sig_ref : Libnames.reference
+val proj1_sig_ref : Libnames.reference
+val proj2_sig_ref : Libnames.reference
+val build_sig : unit -> Coqlib.coq_sigma_data
+val sig_ : Coqlib.coq_sigma_data lazy_t
+val eqind : Term.constr lazy_t
+val eqind_ref : Libnames.global_reference lazy_t
+val refl_equal_ref : Libnames.global_reference lazy_t
+val boolind : Term.constr lazy_t
+val sumboolind : Term.constr lazy_t
+val natind : Term.constr lazy_t
+val intind : Term.constr lazy_t
+val existSind : Term.constr lazy_t
+val existS : Coqlib.coq_sigma_data lazy_t
+val well_founded : Term.constr lazy_t
+val fix : Term.constr lazy_t
+val extconstr : Term.constr -> Topconstr.constr_expr
+val extsort : Term.sorts -> Topconstr.constr_expr
+val my_print_constr : Environ.env -> Term.constr -> Pp.std_ppcmds
+val my_print_context : Environ.env -> Pp.std_ppcmds
+val my_print_env : Environ.env -> Pp.std_ppcmds
+val my_print_rawconstr : Environ.env -> Rawterm.rawconstr -> Pp.std_ppcmds
+val debug_level : int ref
+val debug : int -> Pp.std_ppcmds -> unit
+val debug_msg : int -> Pp.std_ppcmds -> Pp.std_ppcmds
+val trace : Pp.std_ppcmds -> unit
+val wf_relations : (Term.constr, Term.constr lazy_t) Hashtbl.t
+val std_relations : unit Lazy.t
+type binders = Topconstr.local_binder list
+val app_opt : ('a -> 'a) option -> 'a -> 'a
+val print_args : Environ.env -> Term.constr array -> Pp.std_ppcmds
+val make_existential :
+  Util.loc -> Environ.env -> Evd.evar_defs ref -> Term.types -> Term.constr
+val make_existential_expr : Util.loc -> 'a -> 'b -> Topconstr.constr_expr
+val string_of_hole_kind : Evd.hole_kind -> string
+val non_instanciated_map : Environ.env -> Evd.evar_defs ref -> Evd.evar_map
+val global_kind : Decl_kinds.logical_kind
+val goal_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind
+val global_fix_kind : Decl_kinds.logical_kind
+val goal_fix_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind