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

27 files changed, 579 insertions, 413 deletions

diff --git a/.depend.camlp4 b/.depend.camlp4
index 95f25b75b2..741158e9b1 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -31,7 +31,7 @@ parsing/q_util.ml:
 parsing/q_coqast.ml: 
 parsing/g_prim.ml: 
 parsing/g_minicoq.ml: 
-parsing/g_vernac.ml: 
+parsing/g_vernac.ml: parsing/grammar.cma
 parsing/g_proofs.ml: 
 parsing/g_xml.ml: 
 parsing/g_constr.ml: 
diff --git a/Makefile b/Makefile
index 0d2c5abe31..6edd5ca47d 100644
--- a/Makefile
+++ b/Makefile
@@ -299,6 +299,9 @@ SUBTACCMO=\
 	contrib/subtac/subtac_errors.cmo \
 	contrib/subtac/subtac_coercion.cmo \
 	contrib/subtac/interp.cmo \
+	contrib/subtac/interp_fixpoint.cmo \
+	contrib/subtac/subtac_command.cmo \
+	contrib/subtac/subtac.cmo \
 	contrib/subtac/sparser.cmo
 
 
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 []
+
+    
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ff494c7825..0fe01799e1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -719,7 +719,8 @@ let rec extern inctx scopes vars r =
                  let (ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
-		 (fi,nv.(i), bl, extern_typ scopes vars0 ty,
+		 let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in
+		 (fi, (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
@@ -834,6 +835,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
+and extern_recursion_order scopes vars = function
+    RStructRec -> CStructRec
+  | RWfRec c -> CWfRec (extern true scopes vars c)
+
+
 let extern_rawconstr vars c =
   extern false (None,Notation.current_scopes()) vars c
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 608e1bc900..bda43f8121 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -785,18 +785,29 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
         let idl = Array.map
-          (fun (id,n,bl,ty,bd) ->
-            let ((ids',_,_),rbl) =
-              List.fold_left intern_local_binder (env,[]) bl in
+          (fun (id,(n,order),bl,ty,bd) ->
+	    let ro, ((ids',_,_),rbl) =
+	      (match order with
+		   CStructRec -> 
+		     RStructRec,
+		     List.fold_left intern_local_binder (env,[]) bl
+		 | CWfRec c -> 
+		     let before, after = list_chop (succ n) bl in
+		     let ((ids',_,_),rafter) =
+		       List.fold_left intern_local_binder (env,[]) after in
+		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
+		       ro, List.fold_left intern_local_binder (env,rafter) before)
+	    in
 	    let ids'' = List.fold_right Idset.add lf ids' in
-            (List.rev rbl,
+	     ((n, ro), List.rev rbl, 
              intern_type (ids',tmp_scope,scopes) ty,
              intern (ids'',None,scopes) bd)) dl in
-	RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+	RRec (loc,RFix 
+	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
-              Array.map (fun (bl,_,_) -> bl) idl,
-              Array.map (fun (_,ty,_) -> ty) idl,
-              Array.map (fun (_,_,bd) -> bd) idl)
+              Array.map (fun (_,bl,_,_) -> bl) idl,
+              Array.map (fun (_,_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,_,bd) -> bd) idl)
     | CCoFix (loc, (locid,iddef), dl) ->
         let lf = List.map (fun (id,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 6a4ad1f59b..4d4e3f88a0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -530,8 +530,9 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
+
 and fixpoint_expr =
-    identifier * int * local_binder list * constr_expr * constr_expr
+    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
@@ -540,6 +541,10 @@ and local_binder =
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
 
+and recursion_order_expr = 
+  | CStructRec
+  | CWfRec of constr_expr
+
 (***********************)
 (* For binders parsing *)
 
@@ -551,6 +556,9 @@ let rec local_binders_length = function
 let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
 
+let names_of_local_binders bl =
+  List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+
 (**********************************************************************)
 (* Functions on constr_expr *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 11475cdaa2..073f9ba0b3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -114,11 +114,15 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * int * local_binder list * constr_expr * constr_expr
+    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
 
+and recursion_order_expr = 
+  | CStructRec
+  | CWfRec of constr_expr
+
 and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * constr_expr
@@ -157,6 +161,9 @@ val local_binders_length : local_binder list -> int
 (* Does not take let binders into account *)
 val names_of_local_assums : local_binder list -> name located list
 
+(* With let binders *)
+val names_of_local_binders : local_binder list -> name located list
+
 (* Used in correctness and interface; absence of var capture not guaranteed *)
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6208952d32..9c39878c7d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -57,29 +57,29 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
-let rec index_of_annot loc bl ann =
+let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
-    | [_], None -> 0
-    | lids, Some x ->
+    | [_], (None, r) -> 0, r
+    | lids, (Some x, ro) ->
         let ids = List.map snd lids in
-        (try list_index (snd x) ids - 1
+        (try list_index (snd x) ids - 1, ro
         with Not_found ->
           user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
     | _ -> user_err_loc(loc,"index_of_annot",
       Pp.str "cannot guess decreasing argument of fix")
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
-  let n = index_of_annot (fst id) bl ann in
+  let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole loc in
-  (snd id,n,bl,ty,body)
+  (snd id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
-       Pp.str"Annotation forbidden in cofix expression")) ann in
+       Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole loc in
@@ -243,8 +243,10 @@ GEXTEND Gram
         c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
-      | -> None ] ]
+    [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
+      | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
+      | ->  (None, CStructRec)
+      ] ]
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ad3cc5b363..87f388a748 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (* $Id$ *)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
 open Util
@@ -211,11 +212,11 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = ident; bl = LIST1 binder_let;
-        annot = OPT rec_annotation; type_ = type_cstr; 
+        annot = rec_annotation; type_ = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (names_of_local_assums bl) in
           let ni =
-            match annot with
+            match fst annot with
                 Some id ->
                   (try list_index (Name id) names - 1
                   with Not_found ->  Util.user_err_loc
@@ -227,7 +228,7 @@ GEXTEND Gram
                       (loc,"Fixpoint",
                        Pp.str "the recursive argument needs to be specified");
                   0 in
-	  ((id, ni, bl, type_, def),ntn) ] ]
+	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
   ;
   corec_definition:
     [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
@@ -235,7 +236,10 @@ GEXTEND Gram
           (id,bl,c ,def) ] ]
   ;
   rec_annotation:
-    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
+    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
+      | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | ->  (None, CStructRec)
+      ] ]
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c 
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 7b7e471c64..1df3d1f256 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -187,12 +187,31 @@ and interp_xml_decl_alias s x =
 and interp_xml_def x = interp_xml_decl_alias "def" x
 and interp_xml_decl x = interp_xml_decl_alias "decl" x
 
+and interp_xml_recursionOrder x =
+  let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
+  let (locs, s) = get_xml_attr "type" al in
+    match s with
+	"Structural" -> 
+	  (match l with [] -> RStructRec
+	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)"))
+      | "WellFounded" -> 
+	  (match l with
+	       [c] -> RWfRec (interp_xml_type c)
+	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+      | _ ->
+          user_err_loc (locs,"",str "invalid recursion order")
+
+
 and interp_xml_FixFunction x =
   match interp_xml_tag "FixFunction" x with
-  | (loc,al,[x1;x2]) ->
-      (nmtoken (get_xml_attr "recIndex" al),
+  | (loc,al,[x1;x2;x3]) ->
+      ((nmtoken (get_xml_attr "recIndex" al),
+	interp_xml_recursionOrder x1),
+       (get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
+  | (loc,al,[x1;x2]) -> (* For backwards compatibility *)
+      ((nmtoken (get_xml_attr "recIndex" al), RStructRec),
        (get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
-    | (loc,_,_) -> 
+  | (loc,_,_) -> 
         user_err_loc (loc,"",str "wrong number of arguments (expect one)")
 
 and interp_xml_CoFixFunction x =
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 8bf2f42075..a95fa4bad8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -374,13 +374,18 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
-let pr_fixdecl pr prd dangling_with_for (id,n,bl,t,c) =
+let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
   let annot =
     let ids = names_of_local_assums bl in
-    if List.length ids > 1 then 
-      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
-    else mt() in
-  pr_recursive_decl pr prd dangling_with_for id bl annot t c
+      match ro with
+	  CStructRec ->
+	    if List.length ids > 1 then 
+	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+	    else mt() 
+	| CWfRec c ->
+	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}"
+  in
+    pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
 let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) =
   pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e7fc0e01ff..c08b076173 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -549,7 +549,7 @@ let rec pr_vernac = function
         | LocalRawAssum (nal,_) -> nal
         | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | (id,n,bl,type_,def),ntn ->
+        | (id,(n,ro),bl,type_,def),ntn ->
             let (bl',def,type_) =
               if Options.do_translate() then extract_def_binders def type_
               else ([],def,type_) in
@@ -561,9 +561,13 @@ let rec pr_vernac = function
                 warn (str "non-printable fixpoint \""++pr_id id++str"\"");
                 Anonymous in
             let annot =
-              if List.length ids > 1 then 
-                spc() ++ str "{struct " ++ pr_name name ++ str"}"
-              else mt() in
+	      match (ro : Topconstr.recursion_order_expr) with
+		  CStructRec -> 
+		    if List.length ids > 1 then 
+                      spc() ++ str "{struct " ++ pr_name name ++ str"}"
+		    else mt()
+		| CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}"
+	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
             ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++ 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 38675da786..a815e5d2f8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -421,7 +421,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  RRec(dl,RFix nvn,Array.of_list (List.rev lfi),
+  RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index e6bdcbd9bb..8550258c45 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -28,6 +28,9 @@ open Reductionops
 val new_meta : unit -> metavariable
 val mk_new_meta : unit -> constr
 
+(* [new_untyped_evar] is a generator of unique evar keys *)
+val new_untyped_evar : unit -> existential_key
+
 (***********************************************************)
 (* Creating a fresh evar given their type and context *)
 val new_evar :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7d0c926fac..df76f992d0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -232,8 +232,8 @@ let rec pretype tycon env isevars lvar = function
       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 -> 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index d07b83ebac..8a7946cd72 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -75,8 +75,8 @@ val constr_out : Dyn.t -> constr
  *)
 val pretype : 
   type_constraint -> env -> evar_defs ref -> 
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_judgment
+  var_map * (identifier * identifier option) list ->
+  rawconstr -> unsafe_judgment
 
 val pretype_type : 
   val_constraint -> env -> evar_defs ref ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d06395b09d..1c59004175 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -34,8 +34,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type fix_kind = RFix of (int array * int) | RCoFix of int
-
 type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -73,6 +71,10 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
+and fix_recursion_order = RStructRec | RWfRec of rawconstr
+
+and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 11b43ddfcc..cbd215d85e 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -31,8 +31,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type fix_kind = RFix of (int array * int) | RCoFix of int
-
 type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -70,6 +68,10 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
+and fix_recursion_order = RStructRec | RWfRec of rawconstr
+
+and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+
 val cases_predicate_names : 
   (rawconstr * (name * (loc * inductive * name list) option)) list -> name list
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 72139404b5..9f8bbad25f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -501,7 +501,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
   let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     let ce = 
-      { const_entry_body = mkFix ((nvrec,i),recdecls);
+      { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
         const_entry_type = Some arrec.(i);
         const_entry_opaque = false;
         const_entry_boxed = boxed} in