Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 472 insertions, 523 deletions

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index a34446d8..895b97fe 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_proof_instr.ml 11072 2008-06-08 16:13:37Z herbelin $ *)
 
 open Util
 open Pp
@@ -22,6 +22,7 @@ open Decl_mode
 open Decl_interp
 open Rawterm
 open Names
+open Nameops
 open Declarations
 open Tactics
 open Tacticals
@@ -30,6 +31,7 @@ open Termops
 open Reductionops
 open Goptions
 
+
 (* Strictness option *)
 
 let get_its_info gls = get_info gls.it
@@ -81,42 +83,34 @@ let check_not_per pts =
 Please \"suppose\" something or \"end\" it now."
       | _ -> ()
 
-let get_thesis gls0 = 
- let info = get_its_info gls0 in  
-    match info.pm_subgoals with
-	[m,thesis] -> thesis
-      | _ -> error "Thesis is split"
-
 let mk_evd metalist gls =
-  let evd0= create_evar_defs (sig_sig gls) in
+  let evd0= create_goal_evar_defs (sig_sig gls) in
   let add_one (meta,typ) evd = 
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
 
-let set_last cpl gls = 
-  let info = get_its_info gls in
-    tclTHEN 
-      begin 
-	match info.pm_last with 
-	    Some (lid,false) when 
-	      not (occur_id [] lid info.pm_partial_goal) -> 
-		tclTRY (clear [lid])
-	  | _ -> tclIDTAC
-      end
-      begin
-	tcl_change_info 
-	  {info with 
-	    pm_last=Some cpl }
-      end gls
-	  
+let is_tmp id = (string_of_id id).[0] = '_'    
+
+let tmp_ids gls = 
+  let ctx = pf_hyps gls in
+    match ctx with 
+	[] -> []
+      | _::q -> List.filter is_tmp (ids_of_named_context q) 
+
+let clean_tmp gls = 
+  let clean_id id0 gls0 = 
+      tclTRY (clear [id0]) gls0 in
+  let rec clean_all = function
+      [] -> tclIDTAC
+    | id :: rest -> tclTHEN (clean_id id) (clean_all rest)
+  in
+    clean_all (tmp_ids gls) gls
+
 (* start a proof *)
 
 let start_proof_tac gls=
   let gl=sig_it gls in
-  let info={pm_last=None;
-	    pm_partial_goal=mkMeta 1; 
-	    pm_subgoals= [1,gl.evar_concl];
-	    pm_stack=[]} in
+  let info={pm_stack=[]} in
     {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, 
   function 
       [pftree] ->
@@ -267,7 +261,8 @@ let add_justification_hyps keep items gls =
       | _ -> 
 	  let id=pf_get_new_id local_hyp_prefix gls in 
 	    keep:=Idset.add id !keep; 
-	    letin_tac false (Names.Name id) c Tacexpr.nowhere gls in 
+	    tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere)
+              (thin_body [id]) gls in 
     tclMAP add_aux items gls   
 
 let prepare_goal items gls =
@@ -292,14 +287,36 @@ let justification tac gls=
 	   error "insufficient justification" 
 	 else
 	   begin
-	     msgnl (str "Warning: insufficient justification");  
+	     msg_warning (str "insufficient justification");  
 	     daimon_tac gls
 	   end) gls
 
 let default_justification elems gls=
   justification (tclTHEN (prepare_goal elems) automation_tac) gls
 
-(* code for have/then/thus/hence *)
+(* code for conclusion refining *)
+
+let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s)
+
+let _and       = constant ["Init";"Logic"] "and"
+
+let _and_rect  = constant ["Init";"Logic"] "and_rect"
+
+let _prod      = constant ["Init";"Datatypes"] "prod"
+
+let _prod_rect = constant ["Init";"Datatypes"] "prod_rect"
+
+let _ex        = constant ["Init";"Logic"] "ex"
+
+let _ex_ind    = constant ["Init";"Logic"] "ex_ind"
+
+let _sig       = constant ["Init";"Specif"] "sig"
+
+let _sig_rect  = constant ["Init";"Specif"] "sig_rect"
+
+let _sigT      = constant ["Init";"Specif"] "sigT"
+
+let _sigT_rect = constant ["Init";"Specif"] "sigT_rect"
 
 type stackd_elt =
 {se_meta:metavariable;
@@ -336,7 +353,8 @@ let enstack_subsubgoals env se stack gls=
 	    let (nlast,holes,nmetas) = 
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
-	    let evd = meta_assign se.se_meta refiner se.se_evd in
+	    let evd = meta_assign se.se_meta 
+              (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in
 	    let ncreated = replace_in_list 
 	      se.se_meta nmetas se.se_meta_list in
 	    let evd0 = List.fold_left 
@@ -352,19 +370,28 @@ let enstack_subsubgoals env se stack gls=
 	    Array.iteri process gentypes
       | _ -> ()
 
-let find_subsubgoal env c ctyp skip evd metas submetas gls =
+let rec nf_list evd = 
+  function
+      [] -> []  
+    | (m,typ)::others -> 
+	if meta_defined evd m then 
+	    nf_list evd others
+	else
+	  (m,nf_meta evd typ)::nf_list evd others
+
+let find_subsubgoal c ctyp skip submetas gls =
+  let env= pf_env gls in
+  let concl = pf_concl gls in
+  let evd = mk_evd ((0,concl)::submetas) gls in
   let stack = Stack.create () in
   let max_meta = 
-    let tmp = List.fold_left (fun a (m,_) -> max a m) 0 metas in
-      List.fold_left (fun a (m,_) -> max a m) tmp submetas in
-  let _ = 
-    List.iter (fun (m,typ) -> 
-		 Stack.push 
-		   {se_meta=m;
-		    se_type=typ;
-		    se_last_meta=max_meta;
-		    se_meta_list=metas;
-		    se_evd=evd} stack) (List.rev metas) in
+      List.fold_left (fun a (m,_) -> max a m) 0 submetas in
+  let _ = Stack.push 
+		{se_meta=0;
+		 se_type=concl;
+		 se_last_meta=max_meta;
+		 se_meta_list=[0,concl];
+		 se_evd=evd} stack  in
   let rec dfs n = 
     let se = Stack.pop stack in
       try 
@@ -372,10 +399,11 @@ let find_subsubgoal env c ctyp skip evd metas submetas gls =
 	  Unification.w_unify true env Reduction.CUMUL 
 	    ctyp se.se_type se.se_evd in
 	  if n <= 0 then 
-	    {se with 
-	       se_evd=meta_assign se.se_meta c unifier;
-	       se_meta_list=replace_in_list 
-		se.se_meta submetas se.se_meta_list}
+	      {se with 
+		 se_evd=meta_assign se.se_meta
+                  (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier;
+	         se_meta_list=replace_in_list 
+		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
       with _ -> 
@@ -384,85 +412,86 @@ let find_subsubgoal env c ctyp skip evd metas submetas gls =
 	  dfs n
 	end in
   let nse= try dfs skip with Stack.Empty -> raise Not_found in
-    nse.se_meta_list,nse.se_evd
-
-let rec nf_list evd = 
-  function
-      [] -> []  
-    | (m,typ)::others -> 
-	if meta_defined evd m then 
-	    nf_list evd others
-	else
-	  (m,nf_meta evd typ)::nf_list evd others
-
-let rec max_linear_context meta_one c =
-  if !meta_one = None then
-     if isMeta c then
-       	begin
-	  meta_one:= Some c;
-          mkMeta 1
-	end
-     else
-       try
-	 map_constr (max_linear_context meta_one) c
-       with Not_found -> 
-	 begin
-	   meta_one:= Some c;
-           mkMeta 1
-	 end
-  else   
-    if isMeta c then 
-      raise Not_found
-    else
-      map_constr (max_linear_context meta_one) c
+    nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0)
+
+let concl_refiner metas body gls =
+  let concl = pf_concl gls in
+  let evd = sig_sig gls in
+  let env = pf_env gls in
+  let sort = family_of_sort (Typing.sort_of env evd concl) in  
+  let rec aux env avoid subst = function
+      [] -> anomaly "concl_refiner: cannot happen"
+    | (n,typ)::rest ->
+	let _A = subst_meta subst typ in 
+	let x = id_of_name_using_hdchar env _A Anonymous in 
+	let _x = fresh_id avoid x gls in
+	let nenv = Environ.push_named (_x,None,_A) env in
+	let asort = family_of_sort (Typing.sort_of nenv evd _A) in
+	let nsubst = (n,mkVar _x)::subst in
+	  if rest = [] then 
+	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
+	  else
+	    let bsort,_B,nbody = 
+	      aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in
+	    let body = mkNamedLambda _x _A nbody in
+	      if occur_term (mkVar _x) _B then
+	        begin
+		  let _P = mkNamedLambda _x _A _B in
+		    match bsort,sort with
+			InProp,InProp ->
+			  let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in
+			    InProp,_AxB,
+			  mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|])
+		    | InProp,_ ->
+			let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in
+			let _P0 = mkLambda(Anonymous,_AxB,concl) in
+			  InType,_AxB,
+			mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|])
+		    | _,_ -> 
+			let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in
+			let _P0 = mkLambda(Anonymous,_AxB,concl) in
+			  InType,_AxB,
+			mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|])
+		end
+	      else
+		begin
+		  match asort,bsort with
+		      InProp,InProp ->
+			let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in
+			  InProp,_AxB,
+		     mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|])
+		    |_,_ ->
+		       let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in
+		       let _P0 = mkLambda(Anonymous,_AxB,concl) in
+			 InType,_AxB,
+			mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|])
+		end
+  in
+  let (_,_,prf) = aux env [] [] metas in
+    mkApp(prf,[|mkMeta 1|])
 
 let thus_tac c ctyp submetas gls =  
-  let info = get_its_info gls in
-  let evd0 = mk_evd (info.pm_subgoals@submetas) gls in
-  let list,evd = 
+  let list,proof = 
     try
-      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals submetas gls
+      find_subsubgoal c ctyp 0 submetas gls
     with Not_found -> 
       error "I could not relate this statement to the thesis" in
-  let nflist = nf_list evd list in
-  let nfgoal = nf_meta evd info.pm_partial_goal in
-(*  let _ = msgnl (str "Partial goal : " ++ 
-		   print_constr_env (pf_env gls) nfgoal) in *)
-  let rgl = ref None in
-  let refiner = max_linear_context rgl nfgoal in
-    match !rgl with
-	None -> exact_check refiner gls
-      | Some pgl when not (isMeta refiner) ->
-	  let ninfo={info with
-		       pm_partial_goal = pgl;
-		       pm_subgoals = nflist} in
-	    tclTHEN
-	      (Tactics.refine refiner)
-	      (tcl_change_info ninfo) 
-	      gls
-      | _ -> 
-	  let ninfo={info with
-		       pm_partial_goal = nfgoal;
-		       pm_subgoals = nflist} in
-	    tcl_change_info ninfo gls
+  if list = [] then
+    exact_check proof gls 
+  else
+    let refiner = concl_refiner list proof gls in
+      Tactics.refine refiner gls
 
-let anon_id_base = id_of_string "__" 
+(* general forward step *)
 
 
-let mk_stat_or_thesis info = function  
+let anon_id_base = id_of_string "__" 
+
+let mk_stat_or_thesis info gls = function  
     This c -> c
   | Thesis (For _ ) -> 
       error "\"thesis for ...\" is not applicable here" 
-  | Thesis (Sub n) ->
-      begin
-	try List.assoc n info.pm_subgoals 
-	with Not_found -> error "No such part in thesis."
-      end
-  | Thesis Plain ->   
-      match info.pm_subgoals with
-	  [_,c] -> c
-	| _ -> error 
-	    "\"thesis\" is split, please specify which part you refer to."
+  | Thesis Plain -> pf_concl gls
 
 let just_tac _then cut info gls0 =
   let items_tac gls =
@@ -470,11 +499,10 @@ let just_tac _then cut info gls0 =
 	None -> tclIDTAC gls
       | Some items -> 
 	  let items_ = 
-	    if _then then
-	      match info.pm_last with
-		  None -> error "no previous statement to use"
-		| Some (id,_) -> (mkVar id)::items
-	    else items
+	    if _then then 
+	      let last_id = get_last (pf_env gls) in
+		(mkVar last_id)::items
+	    else items 
 	  in prepare_goal items_ gls in
   let method_tac gls = 
     match cut.cut_using with
@@ -487,23 +515,23 @@ let just_tac _then cut info gls0 =
 let instr_cut mkstat _thus _then cut gls0 = 
   let info = get_its_info gls0 in 
   let stat = cut.cut_stat in
-  let (c_id,_) as cpl = match stat.st_label with 
+  let (c_id,_) = match stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_fact") gls0,false 
     | Name id -> id,true in
-  let c_stat = mkstat info stat.st_it in
+  let c_stat = mkstat info gls0 stat.st_it in
   let thus_tac gls= 
     if _thus then 
       thus_tac (mkVar c_id) c_stat [] gls
     else tclIDTAC gls in
     tclTHENS (internal_cut c_id c_stat) 
       [tclTHEN tcl_erase_info (just_tac _then cut info);
-       tclTHEN (set_last cpl) thus_tac] gls0
+       thus_tac] gls0
 
 
 
 (* iterated equality *)
-let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+let _eq = Libnames.constr_of_global (Coqlib.glob_eq)
 
 let decompose_eq id gls =
   let typ = pf_get_hyp_typ gls id in
@@ -518,11 +546,8 @@ let decompose_eq id gls =
       | _ -> error "previous step is not an equality"
 	  
 let instr_rew _thus rew_side cut gls0 = 
-  let info = get_its_info gls0 in
-  let last_id = 	    
-    match info.pm_last with
-	None -> error "no previous equality"
-      | Some (id,_) -> id in
+  let last_id = 
+    try get_last (pf_env gls0) with _ -> error "no previous equality" in
   let typ,lhs,rhs = decompose_eq last_id gls0 in  
   let items_tac gls =
     match cut.cut_by with
@@ -536,7 +561,7 @@ let instr_rew _thus rew_side cut gls0 =
 	  (Tacinterp.eval_tactic tac) gls in
   let just_tac gls =
     justification (tclTHEN items_tac method_tac) gls in
-  let (c_id,_) as cpl = match cut.cut_stat.st_label with 
+  let (c_id,_) = match cut.cut_stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_eq") gls0,false 
     | Name id -> id,true in
@@ -551,14 +576,14 @@ let instr_rew _thus rew_side cut gls0 =
 	      [tclTHEN tcl_erase_info 
 		 (tclTHENS (transitivity lhs) 
 		    [just_tac;exact_check (mkVar last_id)]);
-	       tclTHEN (set_last cpl) (thus_tac new_eq)] gls0
+	       thus_tac new_eq] gls0
       | Rhs ->
 	  let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
 	    tclTHENS (internal_cut c_id new_eq) 
 	      [tclTHEN tcl_erase_info 
 		 (tclTHENS (transitivity rhs) 
 		    [exact_check (mkVar last_id);just_tac]);
-	       tclTHEN (set_last cpl) (thus_tac new_eq)] gls0
+	       thus_tac new_eq] gls0
 	      
 
 
@@ -566,48 +591,29 @@ let instr_rew _thus rew_side cut gls0 =
 
 let instr_claim _thus st gls0 = 
   let info = get_its_info gls0 in  
-  let (id,_) as cpl = match st.st_label with 
+  let (id,_) = match st.st_label with 
       Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false 
     | Name id -> id,true in
   let thus_tac gls= 
     if _thus then 
       thus_tac (mkVar id) st.st_it [] gls
     else tclIDTAC gls in
-  let ninfo1 = {info with 
-		  pm_stack=
-      (if _thus then Focus_claim else Claim)::info.pm_stack;
-		  pm_partial_goal=mkMeta 1;
-	          pm_subgoals = [1,st.st_it]} in
+  let ninfo1 = {pm_stack=
+      (if _thus then Focus_claim else Claim)::info.pm_stack} in
     tclTHENS (internal_cut id st.st_it) 
       [tcl_change_info ninfo1;
-       tclTHEN (set_last cpl) thus_tac] gls0
+       thus_tac] gls0
 
 (* tactics for assume *)
 
-let reset_concl gls =
-  let info = get_its_info gls in
-    tcl_change_info 
-      {info with 
-	 pm_partial_goal=mkMeta 1;
-	 pm_subgoals= [1,gls.it.evar_concl]} gls
-
-
-let intro_pm id gls=
-  let info = get_its_info gls in
-    match info.pm_subgoals with
-	[(_,typ)] -> 
-	  tclTHEN (intro_mustbe_force id) reset_concl gls
-      | _ -> error "Goal is split"
-
 let push_intro_tac coerce nam gls = 
-      let (hid,_) as cpl =
+      let (hid,_) =
 	match nam with 
 	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false 
 	  | Name id -> id,true in
 	tclTHENLIST 
-	  [intro_pm hid;
-	   coerce hid;
-	   set_last cpl]
+	  [intro_mustbe_force hid;
+	   coerce hid]
 	  gls 
 
 let assume_tac hyps gls = 
@@ -652,10 +658,6 @@ let assume_st_letin hyps gls =
 
 (* suffices *)
 
-let free_meta info = 
-  let max_next (i,_) j  = if j <= i then succ i else j in
-  List.fold_right max_next info.pm_subgoals 1
-
 let rec metas_from n hyps = 
   match hyps with
       _ :: q -> n :: metas_from (succ n) q
@@ -683,31 +685,21 @@ let instr_suffices _then cut gls0 =
   let info = get_its_info gls0 in 
   let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in 
   let ctx,hd = cut.cut_stat in
-  let c_stat = build_product ctx (mk_stat_or_thesis info hd) in
-  let metas = metas_from (free_meta info) ctx in
+  let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in
+  let metas = metas_from 1 ctx in
   let c_ctx,c_head = build_applist c_stat metas in
   let c_term = applist (mkVar c_id,List.map mkMeta metas) in  
   let thus_tac gls= 
     thus_tac c_term c_head c_ctx gls in
    tclTHENS (internal_cut c_id c_stat) 
      [tclTHENLIST 
-	 [ tcl_change_info 
-	     {info with 
-	       pm_partial_goal=mkMeta 1;
-	       pm_subgoals=[1,c_stat]};
-	   assume_tac ctx;   
+	 [ assume_tac ctx;   
 	   tcl_erase_info;
 	   just_tac _then cut info];
-      tclTHEN (set_last (c_id,false)) thus_tac] gls0
+      thus_tac] gls0
 
 (* tactics for consider/given *)
 
-let update_goal_info gls =
-  let info = get_its_info gls in
-    match info.pm_subgoals with
-	[m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls
-      | _ -> error "thesis is split"
-
 let conjunction_arity id gls =
   let typ = pf_get_hyp_typ gls id  in
   let hd,params = decompose_app (special_whd gls typ) in
@@ -726,30 +718,18 @@ let conjunction_arity id gls =
 
 let rec intron_then n ids ltac gls = 
   if n<=0 then 
-    tclTHEN
-    (fun gls -> 
-       if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids  then 
-	 update_goal_info gls
-       else 
-	 tclIDTAC gls)
-    (ltac ids)
-      gls
+    ltac ids gls
   else  
     let id = pf_get_new_id (id_of_string "_tmp") gls in 
       tclTHEN 
 	(intro_mustbe_force id) 
 	(intron_then (pred n) (id::ids) ltac) gls 
 
-let pm_rename_hyp id hid gls =
-  if occur_id [] id (pf_concl gls) then
-    tclTHEN (rename_hyp id hid) update_goal_info gls
-  else
-    rename_hyp id hid gls 
 
 let rec consider_match may_intro introduced available expected gls =
   match available,expected with 
       [],[] ->
-	  set_last (List.hd introduced) gls
+	  tclIDTAC gls
     | _,[] -> error "last statements do not match a complete hypothesis" 
 	(* should tell which ones *)
     | [],hyps -> 
@@ -757,7 +737,7 @@ let rec consider_match may_intro introduced available expected gls =
 	  begin
  	    let id = pf_get_new_id (id_of_string "_tmp") gls in
 	      tclIFTHENELSE 
-		(intro_pm id)
+		(intro_mustbe_force id)
 		(consider_match true [] [id] hyps) 
 		(fun _ -> 
 		   error "not enough sub-hypotheses to match statements")
@@ -774,7 +754,7 @@ let rec consider_match may_intro introduced available expected gls =
 		  consider_match may_intro ((id,false)::introduced) rest_ids rest
 	      | Name hid -> 
 		  tclTHENLIST 
-		    [pm_rename_hyp id hid;
+		    [rename_hyp [id,hid];
 		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
 	  end
 	  begin
@@ -783,7 +763,7 @@ let rec consider_match may_intro introduced available expected gls =
 		 try conjunction_arity id gls with 
 		     Not_found -> error "matching hypothesis not found" in 
 		 tclTHENLIST 
-		   [general_case_analysis (mkVar id,NoBindings);
+		   [general_case_analysis false (mkVar id,NoBindings);
 		    intron_then nhyps []
 		      (fun l -> consider_match may_intro introduced 
 			 (List.rev_append l rest_ids) expected)] gls)
@@ -828,49 +808,74 @@ let rec build_function args body =
 
 let define_tac id args body gls =
   let t = build_function args body in
-    letin_tac true (Name id) t Tacexpr.nowhere gls
+    letin_tac None (Name id) t Tacexpr.nowhere gls
 
 (* tactics for reconsider *)
 
 let cast_tac id_or_thesis typ gls = 
-  let info = get_its_info gls in
   match id_or_thesis with
       This id ->
 	let (_,body,_) = pf_get_hyp gls id in
 	  convert_hyp (id,body,typ) gls
     | Thesis (For _ ) -> 
 	error "\"thesis for ...\" is not applicable here" 
-    | Thesis (Sub n) ->
-	begin
-	  let old_typ = 
-	    try List.assoc n info.pm_subgoals 
-	    with Not_found -> error "No such part in thesis." in
-	  if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then
-	    let new_sg = List.merge  
-	      (fun (n,_) (p,_) -> Pervasives.compare n p) 
-	      [n,typ] (List.remove_assoc n info.pm_subgoals) in
-	      tcl_change_info {info with pm_subgoals=new_sg} gls
-	  else 
-	    error "not convertible"
-	end
-    | Thesis Plain ->   
-	match info.pm_subgoals with 
-	    [m,c] -> 
-	      tclTHEN 
-		(convert_concl typ DEFAULTcast) 
-	        (tcl_change_info {info with pm_subgoals= [m,typ]}) gls
-	  | _ -> error 
-	      "\"thesis\" is split, please specify which part you refer to."
-  
+    | Thesis Plain ->    
+          convert_concl typ DEFAULTcast gls
       
 (* per cases *)
 
-let start_tree env ind = 
-  let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in
-    Split (Idset.empty,ind,Array.map (fun _ -> None) constrs)
+let is_rec_pos (main_ind,wft) =
+  match main_ind with
+      None -> false
+    | Some index -> 
+	match fst (Rtree.dest_node wft) with
+	    Mrec i when i = index -> true
+	  | _ -> false
+
+let rec constr_trees (main_ind,wft) ind =
+    match Rtree.dest_node wft with
+      Norec,_ -> 
+	let itree = 
+	  (snd (Global.lookup_inductive ind)).mind_recargs in 
+	  constr_trees (None,itree) ind
+    | _,constrs -> main_ind,constrs
+
+let constr_args rp constr =
+  let main_ind,constrs = constr_trees rp (fst constr) in
+  let ctree = constrs.(pred (snd constr)) in
+    array_map_to_list (fun t -> main_ind,t) 
+      (snd (Rtree.dest_node ctree))
+
+let ind_args rp ind =
+    let main_ind,constrs = constr_trees rp ind in
+    let args ctree =     
+      Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in
+      Array.map args constrs
+
+let init_tree ids ind rp nexti =
+  let indargs = ind_args rp ind in
+  let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in
+    Split_patt (ids,ind,Array.mapi do_i indargs)
+
+let map_tree_rp rp id_fun mapi = function
+    Split_patt (ids,ind,branches) ->
+  let indargs = ind_args rp ind in 
+  let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in
+    Split_patt (id_fun ids,ind,Array.mapi do_i branches)
+  | _ -> failwith "map_tree_rp: not a splitting node"
+
+let map_tree id_fun mapi = function
+    Split_patt (ids,ind,branches) ->
+  let do_i i (recargs,bri) = recargs,mapi i bri in
+    Split_patt (id_fun ids,ind,Array.mapi do_i branches)
+  | _ -> failwith "map_tree: not a splitting node"
+
+
+let start_tree env ind rp = 
+  init_tree Idset.empty ind rp (fun _ _ -> None)
 
 let build_per_info etype casee gls = 
-  let concl=get_thesis gls in
+  let concl=pf_concl gls in
   let env=pf_env gls in
   let ctyp=pf_type_of gls casee in
   let is_dep = dependent casee concl in 
@@ -880,11 +885,11 @@ let build_per_info etype casee gls =
       destInd hd 
     with _ -> 
       error "Case analysis must be done on an inductive object" in
-  let nparams =
-    let mind = fst (Global.lookup_inductive ind) in
-     match etype with
-	 ET_Induction -> mind.mind_nparams_rec
-       | _ -> mind.mind_nparams in
+  let mind,oind = Global.lookup_inductive ind in
+  let nparams,index =
+    match etype with
+	ET_Induction -> mind.mind_nparams_rec,Some (snd ind)
+      | _ -> mind.mind_nparams,None in
   let params,real_args = list_chop nparams args in
   let abstract_obj c body = 
     let typ=pf_type_of gls c in 
@@ -898,7 +903,8 @@ let build_per_info etype casee gls =
    per_pred=pred;
    per_args=real_args;
    per_params=params;
-   per_nparams=nparams}
+   per_nparams=nparams;   
+   per_wf=index,oind.mind_recargs}
 
 let per_tac etype casee gls=
   let env=pf_env gls in
@@ -908,25 +914,24 @@ let per_tac etype casee gls=
 	  let is_dep,per_info = build_per_info etype c gls in
 	  let ek = 
 	    if is_dep then
-	      EK_dep (start_tree env per_info.per_ind)
+	      EK_dep (start_tree env per_info.per_ind per_info.per_wf)
 	    else EK_unknown in
 	    tcl_change_info 
-	      {info with 
-		 pm_stack=
+	      {pm_stack=
 		  Per(etype,per_info,ek,[])::info.pm_stack} gls
       | Virtual cut ->
 	  assert (cut.cut_stat.st_label=Anonymous);
-	  let id = pf_get_new_id (id_of_string "_matched") gls in
+	  let id = pf_get_new_id (id_of_string "anonymous_matched") gls in
 	  let c = mkVar id in
 	  let modified_cut = 
 	    {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
 	    tclTHEN 
-	      (instr_cut (fun _ c -> c) false false modified_cut)
+	      (instr_cut (fun _ _ c -> c) false false modified_cut)
 	      (fun gls0 ->
 		 let is_dep,per_info = build_per_info etype c gls0 in
 		   assert (not is_dep);
 		   tcl_change_info 
-		     {info with pm_stack=
+		     {pm_stack=
 			 Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
 	      gls
 
@@ -944,16 +949,12 @@ let register_nodep_subcase id= function
 
 let suppose_tac hyps gls0 = 
   let info = get_its_info gls0 in
-  let thesis = get_thesis gls0 in
-  let id = pf_get_new_id (id_of_string "_subcase") gls0 in
+  let thesis = pf_concl gls0 in
+  let id = pf_get_new_id (id_of_string "subcase_") gls0 in
   let clause = build_product hyps thesis in
-  let ninfo1 = {info with 
-		  pm_stack=Suppose_case::info.pm_stack;
-		  pm_partial_goal=mkMeta 1;
-		  pm_subgoals = [1,clause]} in
+  let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let old_clauses,stack = register_nodep_subcase id info.pm_stack in
-  let ninfo2 = {info with 
-		  pm_stack=stack} in
+  let ninfo2 = {pm_stack=stack} in
     tclTHENS (internal_cut id clause) 
       [tclTHENLIST [tcl_change_info ninfo1;
 		    assume_tac hyps;
@@ -964,120 +965,109 @@ let suppose_tac hyps gls0 =
 
 (* pattern matching compiling *)
 
-let rec nb_prod_after n c=
-  match kind_of_term c with
-    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
-	1+(nb_prod_after 0 b)
-    | _ -> 0
-
-let constructor_arities env ind =
-  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
-  let constr_types = Inductiveops.arities_of_constructors env ind in 
-  let hyp = nb_prod_after nparams in	
-    Array.map hyp constr_types
-
-let rec n_push rest ids n = 
-  if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) 
-
-let explode_branches ids env ind rest=
-  Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind)
+let rec skip_args rest ids n =
+  if n <= 0 then
+    Close_patt rest
+  else
+    Skip_patt (ids,skip_args rest ids (pred n))
 
-let rec tree_of_pats env ((id,_) as cpl) pats =
+let rec tree_of_pats ((id,_) as cpl) pats =
   match pats with 
-      [] -> End_of_branch cpl
+      [] -> End_patt cpl
     | args::stack ->
 	match args with
-	    [] -> Pop (tree_of_pats env cpl stack)
-	  | patt :: rest_args ->
+	    [] -> Close_patt (tree_of_pats cpl stack)
+	  | (patt,rp) :: rest_args ->
 	      match patt with
 		  PatVar (_,v) -> 
-		    Push (Idset.singleton id,
-			  tree_of_pats env cpl (rest_args::stack))
-		|  PatCstr (_,(ind,cnum),args,nam) ->
-		     let _,mind = Inductive.lookup_mind_specif env ind in
-		     let br= Array.map (fun _ -> None) mind.mind_consnames in
-		       br.(pred cnum) <- 
-			 Some (Idset.singleton id,
-			       tree_of_pats env cpl (args::rest_args::stack));
-		       Split(Idset.empty,ind,br)
-
-let rec add_branch env ((id,_) as cpl) pats tree=
+		    Skip_patt (Idset.singleton id,
+			       tree_of_pats cpl (rest_args::stack))
+		| PatCstr (_,(ind,cnum),args,nam) ->
+		    let nexti i ati =
+		      if i = pred cnum then 
+			let nargs = 
+			  list_map_i (fun j a -> (a,ati.(j))) 0 args in
+			  Some (Idset.singleton id,
+				tree_of_pats cpl (nargs::rest_args::stack))
+		      else None
+		      in init_tree Idset.empty ind rp nexti
+
+let rec add_branch ((id,_) as cpl) pats tree=
   match pats with 
       [] -> 
 	begin
 	  match tree with
-	      End_of_branch cpl0 -> End_of_branch cpl0 
-		(* this ensures precedence *) 
+	      End_patt cpl0 -> End_patt cpl0 
+		(* this ensures precedence for overlapping patterns *) 
 	    | _ -> anomaly "tree is expected to end here"
 	end
     | args::stack ->
 	match args with 
 	    [] ->
 	      begin
-		match tree with 
-		    Pop t -> Pop (add_branch env cpl stack t)
+		match tree with
+		   Close_patt t -> 
+		     Close_patt (add_branch cpl stack t)
 		  | _ -> anomaly "we should pop here" 
 	      end
-	  | patt :: rest_args ->
+	  | (patt,rp) :: rest_args ->
 	      match patt with
 		  PatVar (_,v) ->
 		    begin
 		      match tree with 
-			  Push (ids,t) -> 
-			    Push (Idset.add id ids,
-				  add_branch env cpl (rest_args::stack) t)
-			| Split (ids,ind,br) ->
-			    Split (Idset.add id ids,
-				   ind,array_map2 
-				     (append_branch env cpl 1 
-					(rest_args::stack)) 
-				     (constructor_arities env ind) br)
+			  Skip_patt (ids,t) -> 
+			    Skip_patt (Idset.add id ids,
+				       add_branch cpl (rest_args::stack) t)
+			| Split_patt (_,_,_) ->
+			    map_tree (Idset.add id)
+			      (fun i bri ->  
+				 append_branch cpl 1 (rest_args::stack) bri) 
+			      tree
 			| _ -> anomaly "No pop/stop expected here"  
 		    end
 		| PatCstr (_,(ind,cnum),args,nam) ->
-		    match tree with
-			Push (ids,t) ->
-			  let br = explode_branches ids env ind t in
-			  let _ =
-			    br.(pred cnum)<- 
-			      option_map
-			      (fun (ids,tree) -> 
-				 Idset.add id ids,
-				 add_branch env cpl 
-				   (args::rest_args::stack) tree) 
-			      br.(pred cnum) in
-			    Split (ids,ind,br)
-		      | Split (ids,ind0,br0) ->
+		      match tree with
+			Skip_patt (ids,t) ->
+			  let nexti i ati =
+			    if i = pred cnum then 
+			      let nargs = 
+				list_map_i (fun j a -> (a,ati.(j))) 0 args in
+				Some (Idset.add id ids,
+				      add_branch cpl (nargs::rest_args::stack)
+					(skip_args t ids (Array.length ati)))
+			    else 
+			      Some (ids,
+				    skip_args t ids (Array.length ati))
+			  in init_tree ids ind rp nexti
+		      | Split_patt (_,ind0,_) ->
 			  if (ind <> ind0) then error
 			    (* this can happen with coercions *)
-	                      "Case pattern belongs to wrong inductive type";
-			  let br=Array.copy br0 in
-			  let ca = constructor_arities env ind in
-			  let _= br.(pred cnum)<-
-			    append_branch env cpl 0 (args::rest_args::stack) 
-			    ca.(pred cnum) br.(pred cnum) in 
-			    Split (ids,ind,br)
+	                    "Case pattern belongs to wrong inductive type";
+			  let mapi i ati bri =
+			    if i = pred cnum then 
+			      let nargs = 
+				list_map_i (fun j a -> (a,ati.(j))) 0 args in
+				append_branch cpl 0 
+				  (nargs::rest_args::stack) bri
+			    else bri in
+			    map_tree_rp rp (fun ids -> ids) mapi tree
 		      | _ -> anomaly "No pop/stop expected here"
-and append_branch env ((id,_) as cpl) depth pats nargs = function
+and append_branch ((id,_) as cpl) depth pats = function
     Some (ids,tree) -> 
-      Some (Idset.add id ids,append_tree env cpl depth pats tree)
+      Some (Idset.add id ids,append_tree cpl depth pats tree)
   | None ->
-      Some (* (n_push (tree_of_pats env cpl pats) 
-	      (Idset.singleton id) nargs) *)
-	   (Idset.singleton id,tree_of_pats env cpl pats)
-and append_tree env ((id,_) as cpl) depth pats tree =
-  if depth<=0 then add_branch env cpl pats tree
+      Some (Idset.singleton id,tree_of_pats cpl pats)
+and append_tree ((id,_) as cpl) depth pats tree =
+  if depth<=0 then add_branch cpl pats tree
   else match tree with
-      Pop t -> Pop (append_tree env cpl (pred depth) pats t)
-    | Push (ids,t) -> Push (Idset.add id ids,
-				   append_tree env cpl depth pats t)
-    | End_of_branch _ -> anomaly "Premature end of branch"
-    | Split (ids,ind,branches) -> 
-	Split (Idset.add id ids,ind,
-	       array_map2 
-		 (append_branch env cpl (succ depth) pats) 
-		 (constructor_arities env ind)
-		 branches)
+      Close_patt t -> 
+	Close_patt (append_tree cpl (pred depth) pats t)
+    | Skip_patt (ids,t) -> 
+	Skip_patt (Idset.add id ids,append_tree cpl depth pats t)
+    | End_patt _ -> anomaly "Premature end of branch"
+    | Split_patt (_,_,_) -> 
+	map_tree (Idset.add id) 
+	  (fun i bri -> append_branch cpl (succ depth) pats bri) tree 
 
 (* suppose it is *)
 
@@ -1129,8 +1119,7 @@ let rec build_product_dep pat_info per_info args body gls =
 		  with Not_found -> 
 		    snd (st_assoc (Name id) pat_info.pat_aliases) in
 		  thesis_for obj typ per_info (pf_env gls)
-	    | Plain -> get_thesis gls 
-	    | Sub n -> anomaly "Subthesis in cases" in
+	    | Plain -> pf_concl gls in
 	  mkProd (st.st_label,ptyp,lbody)
     | [] -> body 
 
@@ -1156,26 +1145,22 @@ let rec register_dep_subcase id env per_info pat = function
     EK_nodep -> error  "Only \"suppose it is\" can be used here."
   | EK_unknown -> 
       register_dep_subcase id env per_info pat
-	(EK_dep (start_tree env per_info.per_ind))
-  | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree)
+	(EK_dep (start_tree env per_info.per_ind per_info.per_wf))
+  | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
   
 let case_tac params pat_info hyps gls0 =
   let info = get_its_info gls0 in
-  let id = pf_get_new_id (id_of_string "_subcase") gls0 in
+  let id = pf_get_new_id (id_of_string "subcase_") gls0 in
   let et,per_info,ek,old_clauses,rest =
     match info.pm_stack with
 	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) 
       | _ -> anomaly "wrong place for cases" in
   let clause = build_dep_clause params pat_info per_info hyps gls0 in
-  let ninfo1 = {info with 
-		  pm_stack=Suppose_case::info.pm_stack;
-		  pm_partial_goal=mkMeta 1;
-		  pm_subgoals = [1,clause]} in
+  let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let nek = 
     register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info 
       pat_info.pat_pat ek in  
-  let ninfo2 = {info with 
-		  pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
+  let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
     tclTHENS (internal_cut id clause) 
       [tclTHENLIST 
 	 [tcl_change_info ninfo1; 
@@ -1188,181 +1173,152 @@ let case_tac params pat_info hyps gls0 =
 (* end cases *)
 
 type instance_stack =
-    (constr option*bool*(constr list) list) list
+    (constr option*(constr list) list) list
 
 let initial_instance_stack ids =
-  List.map (fun id -> id,[None,false,[]]) ids
+  List.map (fun id -> id,[None,[]]) ids
 
 let push_one_arg arg = function 
     [] -> anomaly "impossible"
-  | (head,is_rec,args) :: ctx -> 
-      ((head,is_rec,(arg::args)) :: ctx)
+  | (head,args) :: ctx -> 
+      ((head,(arg::args)) :: ctx)
 
 let push_arg arg stacks =
   List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks
   
 
-let push_one_head c is_rec ids (id,stack) = 
+let push_one_head c ids (id,stack) = 
   let head = if Idset.mem id ids then Some c else None in
-    id,(head,is_rec,[]) :: stack
+    id,(head,[]) :: stack
 
-let push_head c is_rec ids stacks =
-  List.map (push_one_head c is_rec ids) stacks
+let push_head c ids stacks =
+  List.map (push_one_head c ids) stacks
 
-let pop_one rec_flag (id,stack) =  
+let pop_one (id,stack) =  
   let nstack=
     match stack with
 	[] -> anomaly "impossible"
       | [c] as l -> l
-      | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx ->
+      | (Some head,args)::(head0,args0)::ctx ->
 	  let arg = applist (head,(List.rev args)) in
-	    rec_flag:= !rec_flag || is_rec;
-	    (head0,is_rec0,(arg::args0))::ctx
-     | (None,is_rec,args)::(head0,is_rec0,args0)::ctx ->
-	 rec_flag:= !rec_flag || is_rec;
-	 (head0,is_rec0,(args@args0))::ctx
+	    (head0,(arg::args0))::ctx
+     | (None,args)::(head0,args0)::ctx ->
+	 (head0,(args@args0))::ctx
   in id,nstack
 
 let pop_stacks stacks =
-  let rec_flag= ref false in 
-  let nstacks = List.map (pop_one rec_flag) stacks in
-    !rec_flag , nstacks
+  List.map pop_one stacks
 
 let patvar_base = id_of_string "__"
 
-let test_fun (str:string) = ()
-
-let hrec_for obj_id fix_id per_info gls=
+let hrec_for fix_id per_info gls obj_id =
   let obj=mkVar obj_id in
   let typ=pf_get_hyp_typ gls obj_id in
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
-    match kind_of_term cind with
-	Ind ind when ind=per_info.per_ind ->
-	  let params,args= list_chop per_info.per_nparams all_args in 
-	    if try 
-	      (List.for_all2 eq_constr params per_info.per_params)
-	    with Invalid_argument _ -> false then
-	      let hd2 = applist (mkVar fix_id,args@[obj]) in
-		Some (compose_lam rc (whd_beta hd2))
-	    else None
-      | _ -> None
-
-
-(* custom elim performs the case analysis of hypothesis id from the local 
-context, 
-
-- generalizing hypotheses below id
-- computing the elimination predicate (abstract inductive predicate) 
-- build case analysis term 
-- generalize rec_calls (use wf_paths)
-- vector of introduced identifiers per branch 
-
-match id in t return p with
- C1 ... => ?1 
-|C2 ... => ?2
-...
-end*)
-
-
-    
-
-
-
-
-
-
-let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
-	      match tree with
-      Pop t ->  
-	let is_rec,nstacks =  pop_stacks stacks in
-	  if is_rec then
-	    let _ = test_fun "is_rec=true" in
-	     let c_id = pf_get_new_id (id_of_string "_hrec") gls in
-	       tclTHEN 
-		 (intro_mustbe_force c_id)
-		 (execute_cases false fix_name per_info kont0 nstacks t) gls
-	  else
-	    execute_cases false fix_name per_info kont0 nstacks t gls
-    | Push (_,t) -> 
-	let id = pf_get_new_id patvar_base gls in
-	let nstacks = push_arg (mkVar id) stacks in
-	let kont = execute_cases false fix_name per_info kont0 nstacks t in
-	  tclTHEN
-	    (intro_mustbe_force id)
-	    begin
-	      match fix_name with
-		  Anonymous -> kont
-		| Name fix_id ->  
-		    (fun gls -> 
-		       if at_top then
-			 kont gls
-		       else
-			 match hrec_for id fix_id per_info gls with
-			     None -> kont gls
-			   | Some c_obj ->
-			       let c_id = 
-				 pf_get_new_id (id_of_string "_hrec") gls in
-				 tclTHENLIST 
-				   [generalize [c_obj];
-				    intro_mustbe_force c_id;
-				    kont] gls)
-	    end gls
-    | Split(ids,ind,br) ->
-	let (_,typ,_)= 
-	  try destProd (pf_concl gls) with Invalid_argument _ ->
-  	    anomaly "Sub-object not found." in
-	let hd,args=decompose_app (special_whd gls typ) in
-	  if try ind <> destInd hd with Invalid_argument _ -> true then
-	      (* argument of an inductive family : intro + discard *)
-	      tclTHEN intro
-  		(execute_cases at_top fix_name per_info kont0 stacks tree) gls
-	    else
-	      begin
-		let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
-		let params = list_firstn nparams args in
-		let constr i =applist (mkConstruct(ind,succ i),params) in
-		let next_tac is_rec i = function
-		    Some (sub_ids,tree) ->
-		      let br_stacks =
-			List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in
-		      let p_stacks = 
-			push_head (constr i) is_rec ids br_stacks in
-			execute_cases false fix_name per_info kont0 p_stacks tree 
-		  | None -> 
-		      msgnl (str "Warning : missing case");
-		      kont0 (mkMeta 1) 
-		in
-		let id = pf_get_new_id patvar_base gls in
-		let kont is_rec = 			
-		  tclTHENSV
-		    (general_case_analysis (mkVar id,NoBindings))
-		    (Array.mapi (next_tac is_rec) br) in
-		  tclTHEN 
-		    (intro_mustbe_force id)
-		    begin
-		      match fix_name with
-			  Anonymous -> kont false
-			| Name fix_id ->  
-			    (fun gls -> 
-			      if at_top then
-				kont false gls
-			    else
-				match hrec_for id fix_id per_info gls with
-				    None -> kont false gls
-				  | Some c_obj ->
-				      tclTHENLIST 
-					[generalize [c_obj];
-					 kont true] gls)
-		    end gls
-	      end
-    | End_of_branch (id,nhyps) -> 
-	match List.assoc id stacks with
-	    [None,_,args] -> 
-	      let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in
-		kont0 (applist (mkVar id,List.rev_append args metas)) gls
-	  | _ -> anomaly "wrong stack size"
-
+  let ind = destInd cind in assert (ind=per_info.per_ind);
+  let params,args= list_chop per_info.per_nparams all_args in 
+  assert begin
+    try List.for_all2 eq_constr params per_info.per_params with 
+        Invalid_argument _ -> false end;
+  let hd2 = applist (mkVar fix_id,args@[obj]) in 
+    compose_lam rc (whd_beta hd2)
+
+let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
+  match tree, objs  with
+      Close_patt t,_ ->  
+	let args0 = pop_stacks args in	
+	  execute_cases fix_name per_info tacnext args0 objs nhrec t gls
+    | Skip_patt (_,t),skipped::next_objs -> 
+	let args0 = push_arg skipped args in
+	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
+    | End_patt (id,nhyps),[] -> 
+	begin
+	  match List.assoc id args with
+	      [None,br_args] -> 
+		let metas = 
+		  list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+		  tclTHEN
+		    (tclDO nhrec introf)
+		    (tacnext 
+		       (applist (mkVar id,List.rev_append br_args metas))) gls
+	    | _ -> anomaly "wrong stack size"
+	end
+    | Split_patt (ids,ind,br), casee::next_objs ->
+	let (mind,oind) as spec = Global.lookup_inductive ind in
+	let nparams = mind.mind_nparams in
+	let concl=pf_concl gls in
+	let env=pf_env gls in
+	let ctyp=pf_type_of gls casee in
+	let hd,all_args = decompose_app (special_whd gls ctyp) in
+	let _ = assert (destInd hd = ind) in (* just in case *)
+	let params,real_args = list_chop nparams all_args in
+	let abstract_obj c body = 
+	  let typ=pf_type_of gls c in 
+	    lambda_create env (typ,subst_term c body) in
+	let elim_pred = List.fold_right abstract_obj    
+	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
+	let case_info = Inductiveops.make_case_info env ind RegularStyle in
+	let gen_arities = Inductive.arities_of_constructors ind spec in
+	let f_ids typ = 
+	  let sign = 
+	    fst (Sign.decompose_prod_assum (Term.prod_applist typ params)) in
+	    find_intro_names sign gls in
+	let constr_args_ids = Array.map f_ids gen_arities in
+	let case_term =	 
+	  mkCase(case_info,elim_pred,casee,
+		 Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in
+	let branch_tac i (recargs,bro) gls0 =
+	  let args_ids = constr_args_ids.(i) in
+	  let rec aux n = function
+	      [] -> 
+		assert (n=Array.length recargs); 
+		next_objs,[],nhrec
+	    | id :: q -> 
+		let objs,recs,nrec = aux (succ n) q in
+		  if recargs.(n) 
+		  then (mkVar id::objs),(id::recs),succ nrec 
+		  else (mkVar id::objs),recs,nrec in
+	  let objs,recs,nhrec = aux 0 args_ids in
+	    tclTHENLIST
+	      [tclMAP intro_mustbe_force args_ids;
+	       begin
+		 fun gls1 -> 
+		   let hrecs = 
+		     List.map 
+		       (fun id -> 
+			  hrec_for (out_name fix_name) per_info gls1 id) 
+		       recs in
+		     generalize hrecs gls1
+	       end;
+	       match bro with
+		   None -> 
+		     msg_warning (str "missing case");
+		     tacnext (mkMeta 1)
+		 | Some (sub_ids,tree) ->
+		     let br_args =
+		       List.filter 
+			 (fun (id,_) -> Idset.mem id sub_ids) args in 
+		     let construct = 
+		       applist (mkConstruct(ind,succ i),params) in
+		     let p_args = 
+		       push_head construct ids br_args in
+		       execute_cases fix_name per_info tacnext 
+			 p_args objs nhrec tree] gls0 in
+	  tclTHENSV 
+	    (refine case_term)
+	    (Array.mapi branch_tac br) gls
+    | Split_patt (_, _, _) , [] -> 
+	anomaly "execute_cases : Nothing to split"
+    | Skip_patt _ , [] -> 
+	anomaly "execute_cases : Nothing to skip"
+    | End_patt (_,_) , _ :: _  -> 
+	anomaly "execute_cases : End of branch with garbage left"
+
+
+
+(* end focus/claim *)
+		
 let end_tac et2 gls =
   let info = get_its_info gls in
   let et1,pi,ek,clauses = 
@@ -1392,7 +1348,7 @@ let end_tac et2 gls =
 	      tclSOLVE [simplest_elim pi.per_casee]	
 	  | ET_Case_analysis,EK_nodep ->
 	      tclTHEN 
-		(general_case_analysis (pi.per_casee,NoBindings))
+		(general_case_analysis false (pi.per_casee,NoBindings))
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
@@ -1400,31 +1356,35 @@ let end_tac et2 gls =
 		 simple_induct (AnonHyp (succ (List.length pi.per_args)));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
-	      tclTHENLIST 
-		[generalize (pi.per_args@[pi.per_casee]);
-		 execute_cases true Anonymous pi 
+		 execute_cases Anonymous pi 
 		   (fun c -> tclTHENLIST 
 		      [refine c;
 		       clear clauses;
 		       justification assumption])
-		   (initial_instance_stack clauses) tree]	
+		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
 	  | ET_Induction,EK_dep tree ->
-	      tclTHEN (generalize (pi.per_args@[pi.per_casee]))
-		begin
-		  fun gls0 -> 
-		    let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in
-		      tclTHEN 
-			(fix (Some fix_id) (succ (List.length pi.per_args))) 
-			(execute_cases true (Name fix_id) pi 
-			   (fun c ->
-			      tclTHENLIST 
-				[clear [fix_id];
-				 refine c;
-				 clear clauses;
-				 justification assumption
-				 (* justification automation_tac *)])
-			   (initial_instance_stack clauses) tree) gls0
-		end	
+	      let nargs = (List.length pi.per_args) in
+		tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+		  begin
+		    fun gls0 -> 
+		      let fix_id = 
+			pf_get_new_id (id_of_string "_fix") gls0 in
+		      let c_id = 
+			pf_get_new_id (id_of_string "_main_arg") gls0 in
+			tclTHENLIST
+			  [fix (Some fix_id) (succ nargs);
+			   tclDO nargs introf;
+			   intro_mustbe_force c_id;
+			   execute_cases (Name fix_id) pi 
+			     (fun c ->
+				tclTHENLIST 
+				  [clear [fix_id];
+				   refine c;
+				   clear clauses;
+				   justification assumption])
+			     (initial_instance_stack clauses) 
+			     [mkVar c_id]  0 tree] gls0
+		  end	
       end gls
 
 (* escape *)
@@ -1432,25 +1392,13 @@ let end_tac et2 gls =
 let rec abstract_metas n avoid head = function
     [] -> 1,head,[]
   | (meta,typ)::rest -> 
-      let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in
+      let id = next_ident_away (id_of_string "_sbgl") avoid in
       let p,term,args = abstract_metas (succ n) (id::avoid) head rest in 
 	succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term),
       (mkMeta n)::args 
 
-let build_refining_context gls =
-  let info = get_its_info gls in
-  let avoid=pf_ids_of_hyps gls in
-  let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in
-    applist (fn,args)
     
-let escape_command pts =
-  let pts1 = nth_unproven 1 pts in
-  let gls = top_goal_of_pftreestate pts1 in
-  let term = build_refining_context gls in
-  let tac = tclTHEN 
-    (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info)
-    (Tactics.refine term) in
-    traverse 1 (solve_pftreestate tac pts1)
+let escape_tac gls =  tcl_erase_info gls
 
 (* General instruction engine *)
 
@@ -1485,7 +1433,8 @@ let rec do_proof_instr_gen _thus _then instr =
     | Psuppose hyps      -> suppose_tac hyps
     | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
     | Pend (B_elim et) -> end_tac et
-    | Pend _ | Pescape -> anomaly "Not applicable"
+    | Pend _ -> anomaly "Not applicable"
+    | Pescape -> escape_tac
  
 let eval_instr {instr=instr} =
   do_proof_instr_gen false false instr   
@@ -1500,7 +1449,7 @@ let rec preprocess pts instr =
       true,pts
   | Pescape -> 
       check_not_per pts;
-      false,pts
+      true,pts
   | Pcase _ | Psuppose _ | Pend (B_elim _) -> 
       true,close_previous_case pts
   | Pend bt -> 
@@ -1511,8 +1460,8 @@ let rec postprocess pts instr =
       Phence i | Pthus i | Pthen i -> postprocess pts i
     | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
-    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
-    | Pescape -> escape_command pts
+    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ 
+    | Pescape -> nth_unproven 1 pts
     | Pend (B_elim ET_Induction) ->
   	begin
 	  let pf = proof_of_pftreestate pts in
@@ -1523,7 +1472,7 @@ let rec postprocess pts instr =
 	      goto_current_focus_or_top (mark_as_done pts)
  	    with 
 		Type_errors.TypeError(env,
-				      Type_errors.IllFormedRecBody(_,_,_)) ->
+				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
 		  anomaly "\"end induction\" generated an ill-formed fixpoint"
 	end
     | Pend _ -> 
@@ -1544,7 +1493,7 @@ let do_instr raw_instr pts =
       let lock_focus = is_focussing_instr instr.instr in
       let marker= Proof_instr (lock_focus,instr) in
 	solve_nth_pftreestate 1 
-	  (abstract_operation marker (eval_instr instr)) pts1
+	  (abstract_operation marker (tclTHEN (eval_instr instr) clean_tmp)) pts1
     else pts1 in
       postprocess pts2 raw_instr.instr