1 files changed, 203 insertions, 186 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 86139039..5bff6ad1 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
@@ -53,22 +55,24 @@ let evar_nf isevars c =
   Evarutil.nf_isevar !isevars c
 
 let interp_gen kind isevars env 
-               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
-(*     (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *)
+  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
-    
+
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c 
 
-let interp_type isevars env ?(impls=([],[])) c =
+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,26 +96,31 @@ 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)
-      
-
-let interp_context sigma env params = 
-  List.fold_left
-    (fun (env,params) d -> match d with
-      | LocalRawAssum ([_,na],(CHole _ as t)) ->
-	  let t = interp_binder sigma env na t in
-	  let d = (na,None,t) in
-	  (push_rel d env, d::params)
-      | LocalRawAssum (nal,t) ->
-	  let t = interp_type sigma env t in
-	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	  let ctx = List.rev ctx in
-	  (push_rel_context ctx env, ctx@params)
-      | LocalRawDef ((_,na),c) ->
-	  let c = interp_constr_judgment sigma env c in
-	  let d = (na, Some c.uj_val, c.uj_type) in
-	  (push_rel d env,d::params))
-    (env,[]) params
+    SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+
+let interp_context_evars evdref env params = 
+  let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in
+  let (env, par, _, impls) =
+    List.fold_left
+      (fun (env,params,n,impls) (na, k, b, t) ->
+	match b with
+	    None ->
+	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
+	      let d = (na,None,t) in
+	      let impls = 
+		if k = Implicit then
+		  let na = match na with Name n -> Some n | Anonymous -> None in
+		    (ExplByPos (n, na), (true, true)) :: impls
+		else impls
+	      in
+		(push_rel d env, d::params, succ n, impls)
+	  | Some b ->
+	      let c = SPretyping.understand_judgment_tcc evdref env b in
+	      let d = (na, Some c.uj_val, c.uj_type) in
+		(push_rel d env,d::params, succ n, impls))
+      (env,[],1,[]) (List.rev bl)
+  in (env, par), impls
 
 (* try to find non recursive definitions *)
 
@@ -126,7 +135,7 @@ let collect_non_rec env =
       let i = 
         list_try_find_i
           (fun i f ->
-             if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec
+             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
              then i else failwith "try_find_i")
           0 lnamerec 
       in
@@ -152,14 +161,14 @@ let collect_non_rec env =
 let list_of_local_binders l = 
   let rec aux acc = function
       Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
-    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
+    | Topconstr.LocalRawAssum (nl, k, c) :: tl -> 
 	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
     | [] -> List.rev acc
   in aux [] l
 
 let lift_binders k n l =
   let rec aux n = function
-    | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+    | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
     | [] -> []
   in aux n l
 
@@ -172,11 +181,10 @@ let split_args n rel = match list_chop ((List.length rel) - n) rel with
   | _ -> assert(false)
 
 let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+  Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
-  let nc = named_context env in
-  let nc_len = named_context_length nc in
   let pr c = my_print_constr env c in
   let prr = Printer.pr_rel_context env in
   let _prn = Printer.pr_named_context env in
@@ -188,8 +196,10 @@ 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 after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
+  let (env', binders_rel), impls = interp_context_evars isevars env bl in
+  let after, ((argname, _, argtyp) as arg), before = 
+    let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in
+      split_args idx 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
   let liftafter = lift_binders 1 after_length after in
@@ -226,11 +236,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		     (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1))))
   in
   let top_bl = after @ (arg :: before) in
-  let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in
-    (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ());
   let top_env = push_rel_context top_bl env 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 top_arity = interp_type isevars top_env arityc in
   let proj = (Lazy.force sig_).Coqlib.proj1 in
   let projection = 
     mkApp (proj, [| argtyp ;
@@ -240,29 +249,21 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		 |])
   in
   let intern_arity = it_mkProd_or_LetIn top_arity after in
-    (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity);
-       trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ());
-  (* Top arity is in top_env = after :: arg :: before *)
-(*   let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *)
-(*       (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *)
-(* 	 trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *)
-  let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *)
-  (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ());
-(*   let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *)
-(*   (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *)
+  (* Intern arity is in top_env = arg :: before *)
+  let intern_arity = liftn 2 2 intern_arity in
+(*     trace (str "After lifting arity: " ++  *)
+(* 	      my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *)
+(* 	      intern_arity); *)
+  (* arity is now in something :: wfarg :: arg :: before 
+     where what refered to arg now refers to something *)
+  let intern_arity = substl [projection] intern_arity in
+  (* substitute the projection of wfarg for something *)
   let intern_before_env = push_rel_context before env in
-(*   let intern_fun_bl = liftafter @ [wfarg 1]  in (\* FixMe dependencies *\) *)
-(*   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
-  (try trace (str "Intern arity: " ++
-		  my_print_constr _intern_env intern_arity) with _ -> ());
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
-  (try trace (str "Intern fun arity product: " ++
-		  my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ());
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
   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 _ =
@@ -274,161 +275,177 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (* 		   str "Intern body " ++ pr intern_body_lam) *)
     with _ -> ()
   in
-  let _impl = 
-    if Impargs.is_implicit_args()
-    then Impargs.compute_implicits top_env top_arity
-    else [] 
-  in
   let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+    (* Lift to get to constant arguments *)
+  let lift_cst = List.length after + 1 in
   let fix_def =
     match measure_fn with
 	None ->
-	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
+	  mkApp (constr_of_global (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
-		    make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ;
-		    prop ;
-		    intern_body_lam |])
+		    make_existential dummy_loc ~opaque:false env isevars wf_proof ;
+		    lift lift_cst prop ;
+		    lift lift_cst intern_body_lam |])
       | Some f ->
-	  lift (succ after_length) 
-	    (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
-		    [| argtyp ; 
-		       f ;
-		       prop ;
-		       intern_body_lam |]))
+	  mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
+		[| lift lift_cst argtyp ; 
+		   lift lift_cst f ;
+		   lift lift_cst prop ;
+		   lift lift_cst intern_body_lam |])
   in
   let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
   let def = it_mkLambda_or_LetIn def_appl binders_rel in
   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 = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some 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 fullctyp evars
+  let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
+    Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls 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
+    (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
-let build_mutrec l boxed = 
-  let sigma = Evd.empty and env = Global.env () in 
-  let nc = named_context env in
-  let nc_len = named_context_length nc in
-  let lnameargsardef =
-    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*)
-    l
-  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 rel_index n ctx = 
+  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
+
+let rec unfold f b =
+  match f b with
+    | Some (x, b') -> x :: unfold f b'
+    | None -> []
+
+let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
+  match n with 
+  | Some (loc, n) -> [rel_index n fixctx]
+  | 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 len = List.length fixctx in
+	unfold (function x when x = len -> None 
+	  | n -> Some (n, succ n)) 0
+
+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 fixctxs, fiximps = List.split (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
-    (* 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 isevars = ref (Evd.create_evar_defs sigma) in	  
-	 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', (isevars, None, arity)::arl))
-      ([],env,[],[]) 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 env_rec = push_named_context rec_sign env in
+
+  (* Get interpretation metadatas *)
+  let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps 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 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 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 = 
-      try
-	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
-	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
-	List.map2
-	  (fun ((_,_,bl,_,def),_) (isevars, info, arity) ->
-	     match info with
-		 None ->
-		   let def = abstract_constr_expr def bl in
-		     isevars, info, interp_casted_constr isevars rec_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 isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
-          lnameargsardef arityl
-      with e ->
-	States.unfreeze fs; raise e in
-    States.unfreeze fs; def 
-  in
-  let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
-    collect_non_rec env lrecnames recdef arityl nv in
-  let recdefs = Array.length defrec in
-    (* Solve remaining evars *)
-  let rec collect_evars i acc = 
-    if i < recdefs then
-      let (isevars, info, def) = defrec.(i) in
-	(*       let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *)
-      let def = evar_nf isevars def in
-      let x, y, typ = arrec.(i) in
-      let typ = evar_nf isevars typ in
-      arrec.(i) <- (x, y, typ);
-      let rec_sign = nf_evar_context !isevars rec_sign in
-      let isevars = Evd.undefined_evars !isevars in
-	(*       let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *)
-      let evm = Evd.evars_of isevars 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 evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in
-	collect_evars (succ i) ((id, def, typ, evars) :: acc)
-    else acc
+      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_map3 compute_possible_guardness_evidences wfl fixctxs 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 (List.rev 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) :: [] -> 
-	build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
-    | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> 
-	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
-	  
-      
-      
+  | None -> raise Not_found
+
+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