Backport code from command.ml to subtac_command.ml for definining

recursive definitions. Now program accepts cofixpoints and uses the new
way infer structurally decreasing arguments. Also, checks for correct
recursive calls before giving the definition to the obligations machine
(solves part 1 of bug #1784).


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

10 files changed, 350 insertions, 193 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 56ebc4f522..f3696f6ec9 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -151,9 +151,9 @@ let subtac (loc, command) =
       | VernacInstance (sup, is, props) ->
 	  Subtac_classes.new_instance sup is props
 
-(*       | VernacCoFixpoint (l, b) ->  *)
-(* 	  let _ = trace (str "Building cofixpoint") in *)
-(* 	    ignore(Subtac_command.build_recursive l b) *)
+      | VernacCoFixpoint (l, b) ->
+	  let _ = trace (str "Building cofixpoint") in
+	    ignore(Subtac_command.build_corecursive l b)
 
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 9afa6f0675..b06880bd3e 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -39,6 +39,8 @@ open Tacticals
 open Tacinterp
 open Vernacexpr
 open Notation
+open Evd
+open Evarutil
 
 module SPretyping = Subtac_pretyping.Pretyping
 open Subtac_utils
@@ -63,12 +65,15 @@ let interp_gen kind isevars env
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c 
 
-let interp_type isevars env ?(impls=([],[])) c =
+let interp_type_evars 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_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+  interp_gen (OfType (Some typ)) isevars env ~impls c 
+
 let interp_open_constr isevars env c =
     msgnl (str "Pretyping " ++ my_print_constr_expr c);
   let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
@@ -92,10 +97,9 @@ let locate_if_isevar loc na = function
 
 let interp_binder sigma env na t =
   let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
-    SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t)
+    SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
       
-
-let interp_context sigma env params = 
+let interp_context_evars sigma env params = 
   List.fold_left
     (fun (env,params) d -> match d with
       | LocalRawAssum ([_,na],k,(CHole _ as t)) ->
@@ -103,7 +107,7 @@ let interp_context sigma env params =
 	  let d = (na,None,t) in
 	  (push_rel d env, d::params)
       | LocalRawAssum (nal,k,t) ->
-	  let t = interp_type sigma env t in
+	  let t = interp_type_evars sigma env t in
 	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
 	  let ctx = List.rev ctx in
 	  (push_rel_context ctx env, ctx@params)
@@ -186,7 +190,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (* 		 Ppconstr.pr_constr_expr body) *)
 (*     with _ -> () *)
     (*   in *)
-  let env', binders_rel = interp_context isevars env bl in
+  let env', binders_rel = interp_context_evars isevars env bl in
   let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
   let before_length, after_length = List.length before, List.length after in
   let argid = match argname with Name n -> n | _ -> assert(false) in
@@ -225,7 +229,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   in
   let top_bl = after @ (arg :: before) in
   let top_env = push_rel_context top_bl env in
-  let top_arity = interp_type isevars top_env arityc in
+  let top_arity = interp_type_evars isevars top_env arityc in
   let intern_bl = wfarg 1 :: arg :: before in
   let intern_env = push_rel_context intern_bl env in
   let proj = (Lazy.force sig_).Coqlib.proj1 in
@@ -264,7 +268,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
 (*   (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
   let fun_env = push_rel_context fun_bl intern_before_env in
-  let fun_arity = interp_type isevars fun_env arityc in
+  let fun_arity = interp_type_evars isevars fun_env arityc in
   let intern_body = interp_casted_constr isevars fun_env body fun_arity in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
   let _ =
@@ -305,145 +309,148 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let typ = it_mkProd_or_LetIn top_arity binders_rel in
   let fullcoqc = Evarutil.nf_isevar !isevars def in
   let fullctyp = Evarutil.nf_isevar !isevars typ in
-(*   let _ = try trace (str "After evar normalization: " ++ spc () ++ *)
-(* 		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *)
-(* 		     ++ str "Coq type: " ++ my_print_constr env fullctyp)  *)
-(*      with _ -> ()  *)
-(*   in *)
   let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
   let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
   let evm = non_instanciated_map env isevars evm in
-
-    (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
   let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
-    (*     (try trace (str "Generated obligations : "); *)
-(*        Array.iter *)
-    (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
-    (* 	 evars; *)
-    (*      with _ -> ());     *)
     Subtac_obligations.add_definition recname evars_def evars_typ evars
 
 let nf_evar_context isevars ctx = 
   List.map (fun (n, b, t) -> 
     (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
-let build_mutrec lnameargsardef boxed = 
-  let sigma = Evd.empty and env = Global.env () in 
-  let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
-  and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
+let interp_fix_context evdref env fix =
+  interp_context_evars evdref env fix.Command.fix_binders
+
+let interp_fix_ccl evdref (env,_) fix =
+  interp_type_evars evdref env fix.Command.fix_type
+
+let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
+  let env = push_rel_context ctx env_rec in
+  let body = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in
+  it_mkLambda_or_LetIn body ctx
+
+let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
+
+let prepare_recursive_declaration fixnames fixtypes fixdefs =
+  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
+  let names = List.map (fun id -> Name id) fixnames in
+  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
+
+let compute_possible_guardness_evidences (n,_) fixtype =
+  match n with 
+  | Some n -> [n] 
+  | None -> 
+      (* If recursive argument was not given by user, we try all args.
+	 An earlier approach was to look only for inductive arguments,
+	 but doing it properly involves delta-reduction, and it finally 
+         doesn't seem to worth the effort (except for huge mutual 
+	 fixpoints ?) *)
+      let m = Term.nb_prod fixtype in
+      let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+	list_map_i (fun i _ -> i) 0 ctx
+
+let push_named_context = List.fold_right push_named
+
+let interp_recursive fixkind l boxed =
+  let env = Global.env() in
+  let fixl, ntnl = List.split l in
+  let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
+
+  (* Interp arities allowing for unresolved types *)
+  let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let fiximps = 
+    List.map 
+      (fun x -> Implicit_quantifiers.implicits_of_binders x.Command.fix_binders) 
+      fixl 
   in
-  let isevars = ref (Evd.create_evar_defs sigma) in	  
-    (* Build the recursive context and notations for the recursive types *)
-  let (rec_sign,rec_env,rec_impls,arityl) = 
-    List.fold_left 
-      (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) -> 
-	 let arityc = Command.generalize_constr_expr arityc bl in
-	 let arity = interp_type isevars env arityc in
-	 let impl = 
-	   if Impargs.is_implicit_args()
-	   then Impargs.compute_implicits env arity
-	   else [] in
-	 let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
-	   ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (None, arity)::arl))
-      ([],env,[],[]) lnameargsardef in
-  let arityl = List.rev arityl in
-  let notations = 
-    List.fold_right (fun (_,ntnopt) l -> Option.List.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),_) (info, arity) ->
-	     match info with
-		 None ->
-		   let def = abstract_constr_expr def bl in
-		     info, interp_casted_constr isevars rec_env ~impls:([],rec_impls)
-		       def arity
-	       | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
-		   let rec_env = push_rel_context fun_bl rec_env in
-		   let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls)
-				def intern_arity
-		   in info, it_mkLambda_or_LetIn cstr fun_bl)
-          lnameargsardef arityl
-      with e ->
-	States.unfreeze fs; raise e in
-    States.unfreeze fs; def 
+  let fixctxs = List.map (interp_fix_context evdref env) fixl in
+  let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
+  let fixtypes = List.map2 build_fix_type fixctxs fixccls in
+  let rec_sign = 
+    List.fold_left2 (fun env id t -> (id,None,t) :: env)
+      [] fixnames fixtypes
   in
-  let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
-    collect_non_rec env lrecnames recdef arityl nv in
-  if lnonrec <> [] then 
-    errorlabstrm "Subtac_command.build_mutrec"
-      (str "Non-recursive definitions not allowed in mutual fixpoint blocks");
-  let recdefs = Array.length defrec in
-    trace (str "built recursive definitions");
-    (* Normalize all types and defs with respect to *all* evars *)
-    Array.iteri 
-      (fun i (info, def) ->
-	let def = evar_nf isevars def in
-	let y, typ = arrec.(i) in
-	let typ = evar_nf isevars typ in
-	  arrec.(i) <- (y, typ);
-	  defrec.(i) <- (info, def))
-      defrec;
-    trace (str "normalized w.r.t. evars");
-  (* Normalize rec_sign which was built earlier *)
-  let rec_sign = nf_evar_context !isevars rec_sign in
-    trace (str "normalized context");
+  let env_rec = push_named_context rec_sign env in
+
+  (* Get interpretation metadatas *)
+  let impls = Command.compute_interning_datas env [] fixnames fixtypes in
+  let notations = List.fold_right Option.List.cons ntnl [] in
+
+  (* Interp bodies with rollback because temp use of notations/implicit *)
+  let fixdefs = 
+    States.with_heavy_rollback (fun () -> 
+      List.iter (Command.declare_interning_data impls) notations;
+      list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
+      () in
+
+  (* Instantiate evars and check all are resolved *)
+  let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
+  let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
+  let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
+  let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
+  let recdefs = List.length rec_sign in
+(*   List.iter (check_evars env_rec Evd.empty evd) fixdefs; *)
+(*   List.iter (check_evars env Evd.empty evd) fixtypes; *)
+(*   check_mutuality env kind (List.combine fixnames fixdefs); *)
+
+  (* Russell-specific code *)
+
   (* Get the interesting evars, those that were not instanciated *)
-  let isevars = Evd.undefined_evars !isevars in
-    trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
+  let isevars = Evd.undefined_evars evd in
+  trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
   let evm = Evd.evars_of isevars in
   trace (str "got the evm, recdefs is " ++ int recdefs);
   (* Solve remaining evars *)
-  let rec collect_evars i acc = 
-    if i < recdefs then
-      let (info, def) = defrec.(i) in
-      let y, typ = arrec.(i) in
-	trace (str "got the def" ++ int i);
-      let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
-      let id = namerec.(i) in
-	(* Generalize by the recursive prototypes  *)
-      let def = 
-	Termops.it_mkNamedLambda_or_LetIn def rec_sign
-      and typ =
-	Termops.it_mkNamedProd_or_LetIn typ rec_sign
-      in
-      let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
-      let evm' = Subtac_utils.evars_of_term evm evm' typ in
-      let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
-	collect_evars (succ i) ((id, def, typ, evars) :: acc)
-    else acc
+  let rec collect_evars id def typ imps = 
+    let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
+      (* Generalize by the recursive prototypes  *)
+    let def = 
+      Termops.it_mkNamedLambda_or_LetIn def rec_sign
+    and typ =
+      Termops.it_mkNamedProd_or_LetIn typ rec_sign
+    in
+    let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
+    let evm' = Subtac_utils.evars_of_term evm evm' typ in
+    let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
+      (id, def, typ, imps, evars)
   in 
-  let defs = collect_evars 0 [] in
-    Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec
-    
-      
+  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
+    (match fixkind with
+      | Command.IsFixpoint wfl ->
+	  let possible_indexes =
+	    List.map2 compute_possible_guardness_evidences wfl fixtypes in
+	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), 
+	    Array.of_list fixtypes, Array.of_list (List.map (subst_vars fixnames) fixdefs)
+	  in
+	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
+      | Command.IsCoFixpoint -> ());
+    Subtac_obligations.add_mutual_definitions defs notations fixkind
+
 let out_n = function
     Some n -> n
   | None -> 0
 
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
-  match lnameargsardef with
-    | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> 
-	ignore(build_wellfounded (id, out_n n, bl, typ, body) r false no boxed)
-    | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> 
-	ignore(build_wellfounded (id, out_n n, bl, typ, body) r true no boxed)
-    | l -> 
-	let lnameargsardef = 
-	  List.map (fun ((id, (n, ro), bl, typ, body), no) ->
-		 match ro with
-		     CStructRec -> (id, out_n n, bl, typ, body), no
-		   | CWfRec _ | CMeasureRec _ -> 
-		       errorlabstrm "Subtac_command.build_recursive"
-			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
-	    lnameargsardef
-	in build_mutrec lnameargsardef boxed
-	  
-      
-      
+let build_recursive l b =
+  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+    match g, l with
+	[(n, CWfRec r)], [((id,_,bl,typ,def),ntn)] ->
+	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false)
+
+      | [(n, CMeasureRec r)], [((id,_,bl,typ,def),ntn)] ->
+	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false)
+
+      | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
+	  let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> 
+	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l 
+	  in interp_recursive (Command.IsFixpoint g) fixl b
+      | _, _ -> 
+	  errorlabstrm "Subtac_command.build_recursive"
+	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+
+let build_corecursive l b =
+  let fixl = List.map (fun ((id,bl,typ,def),ntn) -> 
+    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
+    l in
+  interp_recursive Command.IsCoFixpoint fixl b
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 6de45d17fe..27520867fe 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -20,12 +20,12 @@ val interp_gen :
 val interp_constr :
   evar_defs ref ->
   env -> constr_expr -> constr
-val interp_type :
+val interp_type_evars :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
   constr_expr -> constr
-val interp_casted_constr :
+val interp_casted_constr_evars :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
@@ -38,5 +38,12 @@ val interp_constr_judgment :
   constr_expr -> unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
 
+val interp_binder :     Evd.evar_defs ref ->
+    Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
+
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
+
+val build_corecursive :
+  (cofixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 05bebf0f56..b7777e6222 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,6 +1,7 @@
 open Printf
 open Pp
 open Subtac_utils
+open Command
 
 open Term
 open Names
@@ -35,14 +36,17 @@ type obligation =
 
 type obligations = (obligation array * int)
 
+type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+
 type program_info = {
   prg_name: identifier;
   prg_body: constr;
   prg_type: constr;
   prg_obligations: obligations;
   prg_deps : identifier list;
-  prg_nvrec : int array;
+  prg_fixkind : Command.fixpoint_kind option ;
   prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
+  prg_notations : notations ;
   prg_kind : definition_object_kind;
   prg_hook : definition_hook;
 }
@@ -159,39 +163,50 @@ let declare_definition prg =
 open Pp
 open Ppconstr
 
+let compute_possible_guardness_evidences (n,_) fixtype =
+  match n with 
+  | Some n -> [n] 
+  | None -> 
+      (* If recursive argument was not given by user, we try all args.
+	 An earlier approach was to look only for inductive arguments,
+	 but doing it properly involves delta-reduction, and it finally 
+         doesn't seem to worth the effort (except for huge mutual 
+	 fixpoints ?) *)
+      let m = Term.nb_prod fixtype in
+      let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+	list_map_i (fun i _ -> i) 0 ctx
+
 let declare_mutual_definition l =
   let len = List.length l in
-  let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
-(*   let arrec =  *)
-(*     Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) *)
-(*   in *)
-  let recvec, arrec = 
-    let l, l' = 
-      List.split
-	(List.map (fun x -> 
-	  let subs, typ = (subst_body x) in
-	    snd (decompose_lam_n len subs), 
-	  snd (decompose_prod_n len typ)) l)
-    in
-      Array.of_list l, Array.of_list l'
-  in
-  let nvrec = (List.hd l).prg_nvrec in
-  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
-  let rec declare i fi =
-    (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
-		  my_print_constr (Global.env()) (recvec.(i)));
-     with _ -> ());
-    let ce = 
-      { const_entry_body = mkFix ((nvrec,i),recdecls); 
-        const_entry_type = Some arrec.(i);
-        const_entry_opaque = false;
-        const_entry_boxed = true} in
-      Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+  let fixdefs, fixtypes, fiximps = 
+    list_split3
+      (List.map (fun x -> 
+	let subs, typ = (subst_body x) in
+	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
-  let lrefrec = Array.mapi declare namerec in
-    print_message (recursive_message lrefrec);
-    lrefrec.(0)    
-         
+  let fixkind = Option.get (List.hd l).prg_fixkind in
+  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
+  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+  let boxed = true (* TODO *) in
+  let fixnames = (List.hd l).prg_deps in
+  let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
+  let indexes, fixdecls =
+    match fixkind with
+      | IsFixpoint wfl ->
+	  let possible_indexes =
+	    List.map2 compute_possible_guardness_evidences wfl fixtypes in
+	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
+      | IsCoFixpoint ->
+	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
+  in      
+  (* Declare the recursive definitions *)
+  let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
+    (* Declare notations *)
+    List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+    Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
+    (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+      
 let declare_obligation obl body =
   let ce = 
     { const_entry_body = body;
@@ -220,7 +235,7 @@ let try_tactics obls =
         
 let red = Reductionops.nf_betaiota
 
-let init_prog_info n b t deps nvrec obls impls kind hook =
+let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
     Array.mapi
       (fun i (n, t, o, d) ->
@@ -231,7 +246,8 @@ let init_prog_info n b t deps nvrec obls impls kind hook =
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
-      prg_deps = deps; prg_nvrec = nvrec; prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
+      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
+      prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
     
 let get_prog name =
   let prg_infos = !from_prg in
@@ -422,9 +438,15 @@ let show_obligations ?(msg=true) n =
 		    | Some _ -> ())
       obls
 
+let show_term n =
+  let prg = get_prog_err n in
+  let n = prg.prg_name in
+    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+	    ++ my_print_constr (Global.env ()) prg.prg_body)
+
 let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n b t [] (Array.make 0 0) obls implicits kind hook in
+  let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
     Flags.if_verbose ppnl (str ".");    
@@ -440,12 +462,12 @@ let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ())
 	  | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	  | _ -> res)
 	
-let add_mutual_definitions l ?(implicits=[]) ?(kind=Definition) nvrec =
-  let deps = List.map (fun (n, b, t, obls) -> n) l in
+let add_mutual_definitions l ?(kind=Definition) notations fixkind =
+  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
-      (fun acc (n, b, t, obls) ->
-	 let prg = init_prog_info n b t deps nvrec obls implicits kind (fun x -> ()) in
-	   ProgMap.add n prg acc)
+      (fun acc (n, b, t, imps, obls) ->
+	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in
+	  ProgMap.add n prg acc)
       !from_prg l
   in
     from_prg := upd;
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 30fbd02843..b026e59b23 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -19,11 +19,14 @@ val add_definition : Names.identifier ->  Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_object_kind ->
   ?hook:definition_hook -> obligation_info -> progress
 
+type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+
 val add_mutual_definitions : 
-  (Names.identifier * Term.constr * Term.types * obligation_info) list -> 
-  ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+  (Names.identifier * Term.constr * Term.types *
+      (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
   ?kind:Decl_kinds.definition_object_kind ->
-  int array -> unit
+  notations ->
+  Command.fixpoint_kind -> unit
 
 val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
 
@@ -40,6 +43,8 @@ val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : ?msg:bool -> Names.identifier option -> unit
 
+val show_term : Names.identifier option -> unit
+
 val admit_obligations : Names.identifier option -> unit
 
 exception NoObligations of Names.identifier option
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index c2ee4595d0..ac49ca96a4 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,10 +1,11 @@
 Require Import List.
+
 Program Fixpoint f a : { x : nat | x > 0 } := 
   match a with
   | 0 => 1
   | S a' => g a a'
   end
-with g a b { struct b } : { x : nat | x > 0 } := 
+with g a b : { x : nat | x > 0 } := 
   match b with
   | 0 => 1
   | S b' => f b'
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index a5a8b85f99..501aa79815 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,20 +1,17 @@
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import Coq.Arith.Compare_dec.
 Notation "( x & y )" := (existS _ x y) : core_scope.
   
+Require Import Omega.
+
 Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a}  :
   { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
   if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
   (S q' & r)
   else (O & a).
 
-Require Import Omega.
-
-Obligations.
-Solve Obligations using subtac_simpl ; omega.
-
 Next Obligation.
-  assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+  assert(b * S q' = b * q' + b) by auto with arith ; omega.
 Defined.
 
 Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
index 4764037d94..4f938f4f87 100644
--- a/contrib/subtac/test/measure.v
+++ b/contrib/subtac/test/measure.v
@@ -2,7 +2,7 @@ Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.
 Require Import Coq.Arith.Compare_dec.
 
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 
 Fixpoint size (a : nat) : nat :=
   match a with
@@ -10,15 +10,11 @@ Fixpoint size (a : nat) : nat :=
   | S n => S (size n)
   end.
 
-Program Fixpoint test_measure (a : nat) {measure a size}  : nat :=
+Program Fixpoint test_measure (a : nat) {measure size a}  : nat :=
   match a with
   | S (S n) => S (test_measure n)
-  | x => x
+  | 0 | S 0 => a
   end.
-subst.
-unfold n0.
-auto with arith.
-Qed.
 
 Check test_measure.
 Print test_measure.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
new file mode 100644
index 0000000000..6778831d85
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -0,0 +1,101 @@
+Require Import List.
+Require Import ZArith.
+Require String. Open Scope string_scope.
+Ltac Case s := let c := fresh "case" in set (c := s).
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Inductive sv : Set :=
+| I : Z -> sv
+| S : list sv -> sv.
+
+Section sv_induction.
+
+Variables
+  (VP: sv -> Prop)
+  (LP: list sv -> Prop)
+
+  (VPint: forall n, VP (I n))
+  (VPset: forall vs, LP vs -> VP (S vs))
+  (lpcons: forall v vs, VP v -> LP vs -> LP (v::vs))
+  (lpnil: LP nil).
+
+Fixpoint setl_value_indp (x:sv) {struct x}: VP x :=
+  match x as x return VP x with
+  | I n => VPint n
+  | S vs =>
+    VPset
+    ((fix values_indp (vs:list sv) {struct vs}: (LP vs) :=
+      match vs as vs return LP vs with
+      | nil => lpnil
+      | v::vs => lpcons (setl_value_indp v) (values_indp vs)
+      end) vs)
+  end.
+End sv_induction.
+
+Inductive slt : sv -> sv -> Prop :=
+| IC : forall z, slt (I z) (I z)
+| IS : forall vs vs', slist_in vs vs' -> slt (S vs) (S vs')
+
+with sin : sv ->  list sv -> Prop :=
+| Ihd : forall s s' sv', slt s s' -> sin s (s'::sv')
+| Itl : forall s s' sv', sin s sv' -> sin s (s'::sv')
+
+with slist_in : list sv -> list sv -> Prop :=
+| Inil : forall sv',
+  slist_in nil sv'
+| Icons : forall s sv sv',
+  sin s sv' ->
+  slist_in sv sv' ->
+  slist_in (s::sv) sv'.
+
+Hint Constructors sin slt slist_in.
+
+Require Import Program.
+
+Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
+  match x with
+    | I x => 
+      match y with
+        | I y => if (Z_eq_dec x y) then left else right
+        | S ys => right
+      end
+    | S xs => 
+      match y with
+        | I y => right
+        | S ys =>
+          let fix list_in (xs ys:list sv) {struct xs} : 
+            {slist_in xs ys} + {~slist_in xs ys} :=
+            match xs with
+              | nil => left
+              | x::xs =>
+                let fix elem_in (ys:list sv) : {sin x ys}+{~sin x ys} :=
+                  match ys with
+                    | nil => right
+                    | y::ys => if lt_dec x y then left else if elem_in
+                      ys then left else right
+                  end
+                in 
+                if elem_in ys then 
+                  if list_in xs ys then left else right
+                else right
+            end
+            in if list_in xs ys then left else right
+      end
+  end.
+
+Next Obligation. intro; apply H; inversion H0; subst; trivial. Defined.
+Next Obligation. intro; inversion H. Defined.
+Next Obligation. intro H; inversion H. Defined.
+Next Obligation. intro; inversion H; subst. Defined.
+Next Obligation.
+  contradict H. inversion H; subst. assumption. 
+  contradict H0; assumption. Defined.
+Next Obligation.
+  contradict H0. inversion H0; subst. assumption. Defined.
+Next Obligation.
+  contradict H. inversion H; subst. assumption. Defined.
+Next Obligation.
+  contradict H. inversion H; subst; auto. Defined.
+
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 6b15479d77..d587fabf77 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -43,6 +43,10 @@ val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool 
   ->unit
 
+val declare_interning_data : 'a * Constrintern.implicits_env ->
+    string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
+
+
 val compute_interning_datas :  Environ.env ->
     'a list ->
     'b list ->
@@ -58,9 +62,26 @@ val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 val declare_mutual_with_eliminations :
   bool -> Entries.mutual_inductive_entry -> mutual_inductive
 
-val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
+type fixpoint_kind =
+  | IsFixpoint of (int option * recursion_order_expr) list
+  | IsCoFixpoint
+
+type fixpoint_expr = {
+  fix_name : identifier;
+  fix_binders : local_binder list;
+  fix_body : constr_expr;
+  fix_type : constr_expr
+}
+
+val recursive_message : Decl_kinds.definition_object_kind ->
+  int array option -> Names.identifier list -> Pp.std_ppcmds
+  
+val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier ->
+  constr -> types -> Impargs.manual_explicitation list -> global_reference
+
+val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit
 
-val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
+val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit
 
 val build_scheme : (identifier located option * scheme ) list -> unit