Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.

May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).


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

9 files changed, 456 insertions, 366 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 606352d220..c1c835b923 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -304,7 +304,7 @@ let do_generate_principle fixpoint_exprl  =
 			 snd
 			 (Topconstr.names_of_local_assums args) 
 		     in 
-		     let annot = Util.list_index (Name id) names - 1 in 
+		     let annot = Util.list_index (Name id) names - 1, Topconstr.CStructRec in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
 		 | (name,None,args,types,body),recdef -> 
 		     let names =  (Topconstr.names_of_local_assums args) in
@@ -313,7 +313,7 @@ let do_generate_principle fixpoint_exprl  =
 			 (Util.dummy_loc,"GenFixpoint",
 			  Pp.str "the recursive argument needs to be specified")
 		     else 
-		       (name,0,args,types,body),(None:Vernacexpr.decl_notation)
+		       (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
 		       ("Cannot use mutual definition with well-founded recursion")
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 323d885a27..4556d818e0 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -415,7 +415,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
         CT_cofixc(xlate_ident id,
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
-     let strip_mutrec (fid, n, bl, arf, ardef) =
+     let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
         let (struct_arg,bl,arf,ardef) =
          if bl = [] then
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
@@ -1860,7 +1860,7 @@ let rec xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
    | VernacFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
+      let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) =
         let (struct_arg,bl,arf,ardef) =
          if bl = [] then
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 4279c17f57..14990a24c5 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -1,18 +1,28 @@
-Require Import Coq.Init.Wf.
-
-Section FixPoint.
+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))).
+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.
+
+Check Fix_sub.
+
+Notation "'forall' { x : A | P } , Q" :=
+  (forall x:{x:A|P}, (fun x => Q) (proj1_sig x))
+  (at level 200, x ident, right associativity).
\ No newline at end of file
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 99727e5f25..66a2b36019 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -96,7 +96,7 @@ let eterm evm t =
 	   y' :: l) 
       [] evl 
   in 
-  let t' = (* Substitute evar refs in the term to De Bruijn indices *)
+  let t' = (* Substitute evar refs in the term by De Bruijn indices *)
     subst_evars evts 0 t 
   in
   let t'' = 
@@ -106,8 +106,6 @@ let eterm evm t =
 	 mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
 		   c, acc))
       t' evts
-      
-
   in
   let _declare_evar (id, c) =
     let id = id_of_string ("Evar" ^ string_of_int id) in
@@ -120,8 +118,8 @@ let eterm evm t =
   in
     msgnl (str "Term constructed in Eterm" ++
 	   Termops.print_constr_env (Global.env ()) t'');
-   Tactics.apply_term (Reduction.nf_betaiota t'') (map (fun _ -> Evarutil.mk_new_meta ()) evts)
-       
+    Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts)
+     
 open Tacmach
 
 let etermtac (evm, t) = eterm evm t
diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4
index 095e5fafc9..f435219936 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 (evm, t) gl) ]
+         Eterm.etermtac (Global.env ()) (evm, t) gl) ]
 END
diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml
index f4827c7549..d338c34452 100644
--- a/contrib/subtac/interp.ml
+++ b/contrib/subtac/interp.ml
@@ -30,6 +30,7 @@ open Rawterm
 open Evarconv
 open Pattern
 open Dyn
+open Pretyping
 
 open Subtac_coercion
 open Scoq
@@ -178,9 +179,9 @@ let my_print_tycon env = function
 (* 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); *)
+  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) ->
@@ -255,8 +256,8 @@ let rec pretype tycon env isevars lvar c =
       evar_type_fixpoint loc env isevars names ftys vdefj;
       let fixj =
 	match fixkind with
-	  | RFix (vn,i as vni) ->
-	      let fix = (vni,(names,ftys,Array.map j_val vdefj)) in
+	  | 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 -> 
@@ -444,7 +445,7 @@ let rec pretype tycon env isevars lvar c =
       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
@@ -497,7 +498,88 @@ and pretype_type valcon env isevars lvar = function
                  (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v)
 
 
-type typing_constraint = OfType of types option | IsType
+
+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
@@ -520,6 +602,10 @@ let check_evars env initial_sigma isevars c =
           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
@@ -542,256 +628,39 @@ let check_evars env initial_sigma isevars c =
        retourne aussi le nouveau sigma...
 *)
 
-let understand_judgment sigma env c =
-  let isevars = ref (create_evar_defs sigma) in
+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 sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+  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 sigma env lvar kind c =
-  let isevars = ref (create_evar_defs sigma) in
+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 sigma isevars c;
-  (!isevars, c)
+  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 *)
 
-type var_map = (identifier * unsafe_judgment) list
-type unbound_ltac_var_map = (identifier * identifier option) list
-
-let understand_gen kind sigma env c =
-  snd (ise_pretype_gen true sigma env ([],[]) kind c)
+let understand_gen kind isevars env c =
+  ise_pretype_gen false isevars env ([],[]) kind c
 
-let understand sigma env ?expected_type:exptyp c =
-  snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
+let understand isevars env ?expected_type:exptyp c =
+  ise_pretype_gen false isevars env ([],[]) (OfType exptyp) c
 
-let understand_type sigma env c =
-  snd (ise_pretype_gen true sigma env ([],[]) IsType c)
+let understand_type isevars env c =
+  ise_pretype_gen false isevars env ([],[]) IsType c
 
-let understand_ltac sigma env lvar kind c =
-  ise_pretype_gen false sigma env lvar kind c
+let understand_ltac isevars env lvar kind c =
+  ise_pretype_gen false isevars env lvar kind c
 
-let understand_tcc sigma env ?expected_type:exptyp c =
-  let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
-  evars_of evars,c
+let understand_tcc isevars env ?expected_type:exptyp c =
+  ise_pretype_gen false isevars env ([],[]) (OfType exptyp) c
 
-(** Miscellaneous interpretation functions *)
 
-let interp_sort = function
-  | RProp c -> Prop c
-  | RType _ -> new_Type_sort ()
-
-let interp_elimination_sort = function
-  | RProp Null -> InProp
-  | RProp Pos  -> InSet
-  | RType _ -> InType
-	    
-let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
-  
-let make_fixpoint t id term = 
-  let term = it_mkLambda_or_LetIn term t.args_after in
-  let term' = mkLambda (Name id, t.f_fulltype, term) in
-    mkApp (Lazy.force fixsub, 
-	   [| t.arg_type; t.wf_relation; t.wf_proof; t.f_type; 
-	      mkLambda (t.arg_name, t.arg_type, term') |])       
-
-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 require_library dirpath =
-  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
-    Library.require_library [qualid] None
-
-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
-
-let subtac' recursive id l env (s, t) =
-  check_required_library ["Coq";"Init";"Datatypes"];
-  check_required_library ["Coq";"Init";"Specif"];
-  require_library "Coq.subtac.FixSub";
-  try
-    let evd = ref (create_evar_defs Evd.empty) in
-    let coqintern evd env = Constrintern.intern_constr (evars_of evd) env in
-    let coqinterp evd env = Constrintern.interp_constr (evars_of evd) env in
-    let rec env_with_binders ((env, rels) as acc) = function
-	Topconstr.LocalRawDef ((loc, name), def) :: tl -> 
-	  let rawdef = coqintern !evd env def in
-	  let coqdef, deftyp = interp env evd rawdef empty_tycon in
-	  let reldecl = (name, Some coqdef, deftyp) in
-	    env_with_binders (push_rel reldecl env, reldecl :: rels) tl
-      | Topconstr.LocalRawAssum (bl, typ) :: tl ->
-	  let rawtyp = coqintern !evd env typ in
-	  let coqtyp, typtyp = interp env evd 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
-	    env_with_binders acc tl
-      | [] -> acc
-    in
-    trace (str "Creating env with binders");
-    let env', binders_rel = env_with_binders (env, []) l in
-    trace (str "New env created:" ++ my_print_context env');
-    let s = coqintern !evd env' s in
-    trace (str "Internalized specification: " ++ my_print_rawconstr env s);
-    let coqtype, rec_info, env', binders_type, binders_term =
-      match recursive with
-	  Some (Some (StructRec _) | None) -> assert(false)
-	| Some (Some (WfRec (rel, (loc, n)))) ->
-	    let index, ((n, def, ntype) as nrel) = find_with_index n (rel_context env') in
-	    let after, before = list_split_at index (rel_context env') in
-	    let envbefore = push_rel_context before env in
-	    let typeenv = env' in
-	    let coqrel = coqinterp !evd envbefore rel in
-	    let coqs, styp = interp env' evd s empty_tycon in
-	    let fullcoqs = it_mkProd_or_LetIn coqs after in
-	    let ntype = lift index ntype in
-	    let ftype = mkLambda (n, ntype,  fullcoqs) in
-	    (*let termenv = 
-	      push_rel_context (subst_ctx (mkApp ((Lazy.force _sig).proj1, mkRel 1)) after) *)
-		
-	    let argtype = 
-	      mkApp ((Lazy.force sig_).typ, 
-		     [| ntype;
-			mkLambda (n, ntype, 
-				  mkApp (coqrel, [| mkRel 1; mkRel (index + 2)|])) |])
-	    in
-	    let fulltype = mkProd (n, argtype, fullcoqs) in
-	    let proof = 
-	      let wf_rel = mkApp (Lazy.force well_founded, [| ntype; coqrel |]) in
-		make_existential dummy_loc envbefore evd wf_rel
-	    in
-	    let rec_info = 
-	      { arg_name = n;
-		arg_type = ntype;
-		args_after = after;
-		wf_relation = coqrel;
-		wf_proof = proof;
-		f_type = ftype;
-		f_fulltype = fulltype;
-	      }
-	    in 
-	    let env' = push_rel (Name id, None, fulltype) env' in 
-	      coqs, Some rec_info, env', binders_rel, before
-	| None ->
-	    let coqs, _ = interp env' evd s empty_tycon in
-	      coqs, None, env', binders_rel, binders_rel
-    in
-    (match rec_info with 
-	 Some rec_info -> trace (str "Got recursion info: " ++ my_print_rec_info env rec_info)
-       | None -> ());
-    trace (str "Interpreted type: " ++ my_print_constr env' coqtype);
-    let tycon = mk_tycon coqtype in
-    let t = coqintern !evd env' t in
-    trace (str "Internalized term: " ++ my_print_rawconstr env t);   
-    let coqt, ttyp = interp env' evd t tycon in
-    trace (str "Interpreted term: " ++ my_print_constr env' coqt ++ spc () ++
-	   str "Infered type: " ++ my_print_constr env' ttyp);
-    let coercespec = Subtac_coercion.coerce dummy_loc env' evd ttyp coqtype in
-    trace (str "Specs coercion successfull");
-    let realt = app_opt coercespec coqt in
-    trace (str "Term Specs coercion successfull: " ++ my_print_constr env' realt);
-    let realt = 
-      match rec_info with
-	  Some t -> make_fixpoint t id realt
-	| None -> realt
-    in
-    (try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !evd));
-     with Not_found -> trace (str "Not found in pr_evar_map"));
-    let realt = it_mkLambda_or_LetIn realt binders_term and
-      coqtype = it_mkProd_or_LetIn coqtype binders_type
-    in
-    let realt = Evarutil.nf_evar (evars_of !evd) realt in
-    let coqtype = Evarutil.nf_evar (evars_of !evd) coqtype in
-    trace (str "Coq term: " ++ my_print_constr env realt ++ spc ()
-	   ++ str "Coq type: " ++ my_print_constr env coqtype);
-    let evm = non_instanciated_map env evd in
-      (try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm);
-       with Not_found -> trace (str "Not found in pr_evar_map"));
-    let tac = Eterm.etermtac (evm, realt) in 
-    msgnl (str "Starting proof");
-    Command.start_proof id goal_kind coqtype (fun _ _ -> ());
-    msgnl (str "Started proof");
-    Pfedit.by tac
-  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 -> raise e)
-  
-    | e -> 
-	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e));
-	raise e
-	
-	  
-	
-
-let subtac recursive id l env (s, t) =
-  subtac' recursive id l (Global.env ()) (s, t)
diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml
index 7a84898890..eb9888c161 100644
--- a/contrib/subtac/scoq.ml
+++ b/contrib/subtac/scoq.ml
@@ -10,11 +10,23 @@ open Util
 
 let contrib_name = "subtac"
 
-let subtac_dir = ["subtac"]
-let subfix_module = subtac_dir @ ["FixSub"]
+let subtac_dir = [contrib_name]
+let fix_sub_module = "FixSub"
+let fixsub_module = subtac_dir @ [fix_sub_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 subfix_module "Fix_sub")
+let fixsub = lazy (init_constant fixsub_module "Fix_sub")
+
+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";
@@ -26,6 +38,8 @@ let build_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 boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
 let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
@@ -49,12 +63,6 @@ let my_print_context = Termops.print_rel_context
 let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
 
-let mknewexist = 
-  let exist_counter = ref 0 in
-    fun () -> let i = exist_counter in
-      incr exist_counter;
-      !i
-
 let debug_level = ref 0
 
 let debug n s = 
@@ -80,15 +88,6 @@ let std_relations () =
       
 let std_relations = Lazy.lazy_from_fun std_relations
 
-type wf_proof_type = 
-    AutoProof 
-  | ManualProof of Topconstr.constr_expr
-  | ExistentialProof
-
-type recursion_order =
-  | StructRec of name located
-  | WfRec of Topconstr.constr_expr * name located
-
 type binders = Topconstr.local_binder list
 
 let app_opt c e = 
@@ -96,11 +95,20 @@ let app_opt c e =
       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: " ++
-	     Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str ""));
+	     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
@@ -125,3 +133,8 @@ let non_instanciated_map env evd =
 	       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
diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4
index 657f11b306..43214c87bd 100644
--- a/contrib/subtac/sparser.ml4
+++ b/contrib/subtac/sparser.ml4
@@ -29,110 +29,53 @@ open Topconstr
  *)
 
 module Gram = Pcoq.Gram
-module Constr = Pcoq.Constr
-module Tactic = Pcoq.Tactic
-module Prim = Pcoq.Prim
-
-module Subtac =
-  struct
-    let gec s = Gram.Entry.create ("Subtac."^s)
-    (* types *)
-    let subtac_wf_proof_type : Scoq.wf_proof_type Gram.Entry.e = gec "subtac_wf_proof_type"
-    let subtac_binders : Scoq.binders Gram.Entry.e = gec "subtac_binders"
-    let subtac_fixannot : Scoq.recursion_order option Gram.Entry.e = gec "subtac_fixannot"
-
-    (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
-    (* admissible notation "(x t)" 
-       taken from g_constrnew.ml4 *)
-    let test_lpar_id_coloneq =
-      Gram.Entry.of_parser "test_lpar_id_coloneq"
-	(fun strm ->
-	   Pp.msgnl (Pp.str ("Testing lpar_id_coloneq:" ^ 
-			       (snd (List.hd (Stream.npeek 1 strm)))));
-	   
-	   match Stream.npeek 1 strm with
-             | [("","(")] ->
-		 (match Stream.npeek 2 strm with
-		    | [_; ("IDENT",s)] ->
-			(match Stream.npeek 3 strm with
-			   | [_; _; ("", ":=")] ->
-                               Stream.junk strm; Stream.junk strm; Stream.junk strm;
-			       Pp.msgnl (Pp.str "Success");
-                               Names.id_of_string s
-			   | _ -> raise Stream.Failure)
-		    | _ -> raise Stream.Failure)
-             | _ -> raise Stream.Failure)
-
-    let test_id_coloneq =
-      Gram.Entry.of_parser "test_id_coloneq"
-	(fun strm ->
-	   Pp.msgnl (Pp.str ("Testing id_coloneq:" ^ 
-			       (snd (List.hd (Stream.npeek 1 strm)))));
-	   
-	   (match Stream.npeek 1 strm with
-	      | [("IDENT",s)] ->
-		  (match Stream.npeek 2 strm with
-		     | [_; ("", ":=")] ->
-                         Stream.junk strm; Stream.junk strm;
-			 Pp.msgnl (Pp.str "Success");
-                         Names.id_of_string s
-		     | _ -> raise Stream.Failure)
-	      | _ -> raise Stream.Failure))
-end 
-
-open Subtac
+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_wf_proof_type subtac_binders subtac_fixannot;
+  GLOBAL: subtac_gallina_loc;
  
-  subtac_wf_proof_type:
-    [ [ IDENT "proof"; t = Constr.constr -> 
-	  Scoq.ManualProof t
-      | IDENT "auto" -> Scoq.AutoProof
-      | -> Scoq.ExistentialProof
-      ]
-    ]
+  subtac_gallina_loc:
+    [ [ g = Vernac.gallina -> loc, g ] ]
     ;
-  
-  subtac_fixannot:
-    [ [ "{"; IDENT "struct"; id=Prim.name; "}" -> Some (Scoq.StructRec id)
-      | "{"; IDENT "wf"; rel= Constr.constr; id=Prim.name; "}" -> Some (Scoq.WfRec (rel, id))
-      | -> None ] ]
-  ;
-
-  subtac_binders: [ [ bl = LIST0 Constr.binder_let -> bl ] ]
-  ;
   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 = (Scoq.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),
-  (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) =
-  Genarg.create_arg "subtac_wf_proof_type"
+(* let (wit_subtac_wf_proof_type : wf_proof_type_argtype), *)
+(*   (globwit_subtac_wf_proof_type : wf_proof_type_argtype), *)
+(*   (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) = *)
+(*   Genarg.create_arg "subtac_wf_proof_type" *)
 
-type subtac_binders_argtype = (Scoq.binders, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
 
-let (wit_subtac_binders : subtac_binders_argtype),
-  (globwit_subtac_binders : subtac_binders_argtype),
-  (rawwit_subtac_binders : subtac_binders_argtype) =
-  Genarg.create_arg "subtac_binders"
+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"
 
-type subtac_fixannot_argtype = (Scoq.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+(* type subtac_recdef_argtype = (Scoq.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
 
-let (wit_subtac_fixannot : subtac_fixannot_argtype),
-  (globwit_subtac_fixannot : subtac_fixannot_argtype),
-  (rawwit_subtac_fixannot : subtac_fixannot_argtype) =
-  Genarg.create_arg "subtac_fixannot"
+(* let (wit_subtac_recdef : subtac_recdef_argtype), *)
+(*   (globwit_subtac_recdef : subtac_recdef_argtype), *)
+(*   (rawwit_subtac_recdef : subtac_recdef_argtype) = *)
+(*   Genarg.create_arg "subtac_recdef" *)
 
-VERNAC COMMAND EXTEND SubtacRec
-[ "Recursive" "program" ident(id) subtac_binders(l) subtac_fixannot(f)
-    ":" lconstr(s) ":=" lconstr(t) ] -> 
-  [ Interp.subtac (Some f) id l Environ.empty_env (s, t) ]
-END
+(* VERNAC COMMAND EXTEND SubtacRec *)
+(* [ "Recursive" "program" ident(id) subtac_binders(l) subtac_recdef(f) ] ->  *)
+(*   [ Interp.subtac id l Environ.empty_env f ] *)
+(* END *)
   
 VERNAC COMMAND EXTEND Subtac
-[ "Program" ident(id) subtac_binders(l) ":" lconstr(s) ":=" lconstr(t) ] -> 
-  [ Interp.subtac None id l Environ.empty_env (s, t) ]
+[ "Program" subtac_gallina_loc(g) ] -> 
+  [ Subtac.subtac g ]
 END
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
new file mode 100644
index 0000000000..34eff9a176
--- /dev/null
+++ b/contrib/subtac/subtac_command.ml
@@ -0,0 +1,257 @@
+
+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 Pretyping
+
+open Tacinterp
+open Vernacexpr
+open Notation
+
+open Interp
+open Scoq
+
+
+(*********************************************************************)
+(* Functions to parse and interpret constructions *)
+
+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 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 =
+  understand_tcc isevars env (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)
+
+(* 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 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 build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+  let sigma = Evd.empty
+  and env0 = Global.env()
+  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))
+      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,_,bl,arityc,_),_) -> 
+        let arityc = Command.generalize_constr_expr arityc bl in
+	let isevars = ref (Evd.create_evar_defs sigma) in
+        let isevars, 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, 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),_) (evm, arity) ->
+             let def = abstract_constr_expr def bl in
+               interp_casted_constr (ref (Evd.create_evar_defs evm)) rec_sign ~impls:([],rec_impls)
+		def arity)
+          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);
+      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 snd arrec
+    in declare arrec recvec
+  in
+  let recdefs = Array.length defrec in
+    trace (int recdefs ++ str " recursive definitions");
+    (* Solve remaining evars *)
+  let rec solve_evars i acc = 
+    if i < recdefs then
+      let (evm, def) = defrec.(i) in
+	if Evd.dom evm = [] then 
+	  solve_evars (succ i) (def :: acc)
+	else
+	  let _,typ = arrec.(i) in
+	  let id = namerec.(i) 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 tac = Eterm.etermtac (evm, def) in 
+	  let _ =
+	    trace (str "Starting proof of a fixpoint def:" ++ spc () ++ my_print_constr env0 def ++
+		   spc () ++ str " with goal: " ++ my_print_constr env0 typ ++
+		   spc () ++ str " with evar map = " ++ Evd.pr_evar_map evm)
+	  in
+	    begin
+	      Command.start_proof (id_of_string (string_of_id id ^ "_evars"))  goal_kind typ
+		(fun _ 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 def = Environ.constant_value (Global.env ()) constant in
+		       let _ = trace (str "Got constant value") in		 
+		       let _, c = decompose_lam_n recdefs def in
+		       let _ = trace (str "Fixpoint body is: " ++ spc () ++ my_print_constr (Global.env ()) c) in
+			 solve_evars (succ i) (c :: acc)
+		     with Environ.NotEvaluableConst cer ->
+		       match cer with
+			   Environ.NoBody -> trace (str "Constant has no body")
+			 | Environ.Opaque -> trace (str "Constant is opaque")
+		);
+	      trace (str "Started proof");
+	      Pfedit.by tac;
+	      trace (str "Applied eterm tac");
+	    end
+    else declare (List.rev acc)
+  in solve_evars 0 []
+
+