X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;h=41584d1d3803237b43639b8bce94118a83a6fc88;hp=b01f4259da6bf0a37aad09fc8970cfe7869b4825;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hpb=9ab5bcc58aa62e4ded71fd64cc5a4ea562195103

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index b01f4259d..41584d1d3 100644
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -43,11 +43,13 @@ let extract_first_goal_from_status status =
   let s = status#stack in
   match s with
   | [] -> fail (lazy "There's nothing to prove")
-  | (g1, _, k, tag1) :: tl ->
+  | (g1, _, k, tag1, _) :: tl ->
     let goals = filter_open g1 in
-    let (loc::tl) = goals in
-    let goal = goal_of_loc (loc) in
-    goal ;;
+    match goals with
+      [] -> fail (lazy "No goals under focus")
+    | loc::tl -> 
+      let goal = goal_of_loc (loc) in
+      goal ;;
 
 let extract_conclusion_type status goal =
   let gty = get_goalty status goal in
@@ -75,6 +77,23 @@ let are_convertible ty1 ty2 status goal =
   let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
   NTacStatus.are_convertible status ctx cicterm1 cicterm2
 
+let clear_volatile_params_tac status =
+  match status#stack with
+    [] -> fail (lazy "Empty stack")
+  | (g,t,k,tag,p)::tl -> 
+    let rec remove_volatile = function
+        [] -> []
+      | (k,v as hd')::tl' ->
+        let re = Str.regexp "volatile_.*" in
+        if Str.string_match re k 0 then
+          remove_volatile tl'
+        else
+          hd'::(remove_volatile tl')
+    in
+    let newp = remove_volatile p in
+    status#set_stack ((g,t,k,tag,newp)::tl)
+;;
+
 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
    the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
    \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
@@ -86,38 +105,36 @@ let lambda_abstract_tac id t1 t2 status goal =
       match t2 with
       | None ->
         let (_,_,t1) = t1 in
-        exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
-                                       `JustOne))) (*status*)
+        block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+                                                  `JustOne))); clear_volatile_params_tac] status
       | Some t2 ->
         let status,res = are_convertible t1 t2 status goal in
         if res then
           let (_,_,t2) = t2 in
-          exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
-                                         `JustOne))) (*status*)
+          block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
+                                                    `JustOne))); clear_volatile_params_tac] status
         else
           raise NotEquivalentTypes
     else
       raise FirstTypeWrong
   | _ -> raise NotAProduct
 
-let assume name ty eqty =
-  distribute_tac (fun status goal ->
-      try exec (lambda_abstract_tac name ty eqty status goal) status goal
-      with
-      | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
-      | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
-      | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
-    )
+let assume name ty eqty status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac name ty eqty status goal
+  with
+  | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
+  | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
+  | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
 ;;
 
-let suppose t1 id t2 =
-  distribute_tac (fun status goal ->
-      try exec (lambda_abstract_tac id t1 t2 status goal) status goal
-      with
-      | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
-      | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
-      | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
-    )
+let suppose t1 id t2 status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac id t1 t2 status goal
+  with
+  | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
+  | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
+  | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
 ;;
 
 let assert_tac t1 t2 status goal continuation =
@@ -133,26 +150,76 @@ let assert_tac t1 t2 status goal continuation =
   else
     raise FirstTypeWrong
 
-let mustdot status =
-  let s = status#stack in
-  match s with
-  | [] -> fail (lazy "No goals to dot")
-  | (_, _, k, _) :: tl ->
-    if List.length k > 0 then
-      true
+let branch_dot_tac status =
+  match status#stack with 
+    ([],t,k,tag,p) :: tl ->
+    if List.length t > 0 then
+      status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
     else
-      false
+      status
+  | _ -> status
+;;
+
+let status_parameter key status =
+  match status#stack with
+    [] -> ""
+  | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
+;;
+
+let beta_rewriting_step t status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx <> "beta_rewrite" then fail (lazy "Invalid use of 'or equivalently'")
+  else
+    change_tac ~where:("",0,(None,[],Some
+                               Ast.UserInput)) ~with_what:t status
+;;
+
+let done_continuation status =
+  let rec continuation l =
+    match l with
+      [] -> []
+    | (_,t,_,tag,p)::tl ->
+      if tag = `BranchTag then
+        if List.length t > 0 then
+          let continue =
+            let ctx =
+              try List.assoc "context" p
+              with Not_found -> ""
+            in
+              ctx <> "induction" && ctx <> "cases"
+          in
+          if continue then [clear_volatile_params_tac;branch_dot_tac] else
+            [clear_volatile_params_tac]
+        else 
+          [merge_tac] @ (continuation tl)
+      else
+        []
+  in
+    continuation status#stack
+;;
 
 let bydone just status =
   let goal = extract_first_goal_from_status status in
-  let mustdot = mustdot status in
-  let l = [mk_just status goal just] in
-  let l =
-    if mustdot then List.append l [dot_tac] else l
-  in
+  let continuation = done_continuation status in
+  let l = [mk_just status goal just] @ continuation in
   block_tac l status
 ;;
 
+let push_goals_tac status = 
+  match status#stack with
+    [] -> fail (lazy "Error pushing goals")
+  | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
+    if List.length g2 > 0 then
+      status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
+    else status (* Nothing to push *)
+  | _ -> status
+
+let add_parameter_tac key value status =
+  match status#stack with
+    [] -> status
+  | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
+;;
+
 let we_need_to_prove t id t1 status =
   let goal = extract_first_goal_from_status status in
   match id with
@@ -161,14 +228,17 @@ let we_need_to_prove t id t1 status =
       match t1 with
       | None ->  (* We need to prove t *)
         (
-          try assert_tac t None status goal (id_tac status)
+          try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
           with
           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
         )
       | Some t1 -> (* We need to prove t or equivalently t1 *)
         (
-          try assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some
-                                                                             Ast.UserInput)) ~with_what:t1 status)
+          try assert_tac t (Some t1) status goal (block_tac [change_tac ~where:("",0,(None,[],Some
+                                                                             Ast.UserInput))
+                                                               ~with_what:t1;
+                                                             add_parameter_tac "volatile_context"
+                                                               "beta_rewrite"] status)
           with
           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
           | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
@@ -178,14 +248,14 @@ let we_need_to_prove t id t1 status =
     (
       match t1 with
       (* We need to prove t (id) *)
-      | None -> block_tac [cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac;
-                           dot_tac
+      | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+                           push_goals_tac
                           ] status
       (* We need to prove t (id) or equivalently t1 *)
-      | Some t1 ->  block_tac [cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
+      | Some t1 ->  block_tac [clear_volatile_params_tac; cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
                                                                                   Ast.UserInput))
                                  ~with_what:t1; shift_tac; intro_tac id; merge_tac;
-                               dot_tac
+                               branch_tac; push_goals_tac
                               ]
                       status
     )
@@ -221,46 +291,47 @@ let by_just_we_proved just ty id ty' status =
   | Some id ->
     (
       match ty' with
-      | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac ] status
+      | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+                           clear_volatile_params_tac ] status
       | Some ty' -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; change_tac
                                  ~where:("",0,(None,[id,Ast.UserInput],None)) ~with_what:ty';
-                               merge_tac] status
+                               merge_tac; clear_volatile_params_tac] status
     )
 ;;
 
-let existselim just id1 t1 t2 id2 =
-  distribute_tac (fun status goal ->
-      let (_,_,t1) = t1 in
-      let (_,_,t2) = t2 in
-      let just = mk_just status goal just in
-      exec (block_tac [
-          cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
-                                                                                     (id1,None), Some t1),t2)]));
-          branch_tac ~force:false;
-          just;
-          shift_tac;
-          case1_tac "_";
-          intros_tac ~names_ref:(ref []) [id1;id2];
-          merge_tac
-        ]) status goal
-    )
+let existselim just id1 t1 t2 id2 status =
+  let goal = extract_first_goal_from_status status in
+  let (_,_,t1) = t1 in
+  let (_,_,t2) = t2 in
+  let just = mk_just status goal just in
+  (block_tac [
+      cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
+                                                                                 (id1,None), Some t1),t2)]));
+      branch_tac ~force:false;
+      just;
+      shift_tac;
+      case1_tac "_";
+      intros_tac ~names_ref:(ref []) [id1;id2];
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status
 ;;
 
-let andelim just t1 id1 t2 id2  =
-  distribute_tac (fun status goal ->
-      let (_,_,t1) = t1 in
-      let (_,_,t2) = t2 in
-      let just = mk_just status goal just in
-      exec (block_tac [
-          cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
-          branch_tac ~force:false;
-          just;
-          shift_tac;
-          case1_tac "_";
-          intros_tac ~names_ref:(ref []) [id1;id2];
-          merge_tac
-        ]) status goal
-    )
+let andelim just t1 id1 t2 id2 status =
+  let goal = extract_first_goal_from_status status in
+  let (_,_,t1) = t1 in
+  let (_,_,t2) = t2 in
+  let just = mk_just status goal just in
+  (block_tac [
+      cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
+      branch_tac ~force:false;
+      just;
+      shift_tac;
+      case1_tac "_";
+      intros_tac ~names_ref:(ref []) [id1;id2];
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status
 ;;
 
 let type_of_tactic_term status ctx t =
@@ -272,15 +343,15 @@ let swap_first_two_goals_tac status =
   let gstatus =
     match status#stack with
     | [] -> assert false
-    | (g,t,k,tag) :: s ->
+    | (g,t,k,tag,p) :: s ->
       match g with
       | (loc1) :: (loc2) :: tl ->
-        ([loc2;loc1] @+ tl,t,k,tag) :: s
+        ([loc2;loc1] @+ tl,t,k,tag,p) :: s
       | _ -> assert false
   in
   status#set_stack gstatus
 
-let thesisbecomes t1 t2 = we_need_to_prove t1 None t2
+let thesisbecomes t1 l = we_need_to_prove t1 None l
 ;;
 
 let obtain id t1 status =
@@ -293,72 +364,78 @@ let obtain id t1 status =
   block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
                                          `JustOne]));
               swap_first_two_goals_tac;
-              branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; dot_tac;
+              branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+              add_parameter_tac "volatile_context" "rewrite"
             ]
     status
 ;;
 
-let conclude t1 =
-  distribute_tac (fun status goal ->
-      let cicgty = get_goalty status goal in
-      let ctx = ctx_of cicgty in
-      let _,gty = term_of_cic_term status cicgty ctx in
-      match gty with
-        NCic.Appl [_;_;plhs;_] ->
-        if alpha_eq_tacterm_kerterm t1 plhs status goal then
-          exec id_tac status goal
-        else
-          fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
-      | _ -> fail (lazy "Your conclusion needs to be an equality")
-    )
-;;
-
-let rewritingstep rhs just last_step status =
+let conclude t1 status =
   let goal = extract_first_goal_from_status status in
   let cicgty = get_goalty status goal in
   let ctx = ctx_of cicgty in
   let _,gty = term_of_cic_term status cicgty ctx in
-  let cicty = type_of_tactic_term status ctx rhs in
-  let _,ty = term_of_cic_term status cicty ctx in
-  let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
-    match just with
-      `Auto (univ, params) ->
-      let params =
-        if not (List.mem_assoc "timeout" params) then
-          ("timeout","3")::params
-        else params
+  match gty with
+    NCic.Appl [_;_;plhs;_] ->
+    if alpha_eq_tacterm_kerterm t1 plhs status goal then
+      add_parameter_tac "volatile_context" "rewrite" status
+    else
+      fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+  | _ -> fail (lazy "Your conclusion needs to be an equality")
+;;
+
+let rewritingstep rhs just last_step status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx = "rewrite" then 
+    (
+      let goal = extract_first_goal_from_status status in
+      let cicgty = get_goalty status goal in
+      let ctx = ctx_of cicgty in
+      let _,gty = term_of_cic_term status cicgty ctx in
+      let cicty = type_of_tactic_term status ctx rhs in
+      let _,ty = term_of_cic_term status cicty ctx in
+      let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
+        match just with
+          `Auto (univ, params) ->
+          let params =
+            if not (List.mem_assoc "timeout" params) then
+              ("timeout","3")::params
+            else params
+          in
+          let params' =
+            if not (List.mem_assoc "paramodulation" params) then
+              ("paramodulation","1")::params
+            else params
+          in
+          if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
+          else
+            first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
+                         ~params:(univ, params') status goal]
+        | `Term just -> apply_tac just
+        | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
+        | `Proof -> id_tac
       in
-      let params' =
-        if not (List.mem_assoc "paramodulation" params) then
-          ("paramodulation","1")::params
-        else params
+      let plhs,prhs,prepare =
+        match gty with (* Extracting the lhs and rhs of the previous equality *)
+          NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+        | _ -> fail (lazy "You are not building an equaility chain")
       in
-      if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
-      else
-        first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
-                     ~params:(univ, params') status goal]
-    | `Term just -> apply_tac just
-    | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
-    | `Proof -> id_tac
-  in
-  let plhs,prhs,prepare =
-    match gty with (* Extracting the lhs and rhs of the previous equality *)
-      NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
-    | _ -> fail (lazy "You are not building an equaility chain")
-  in
-  let continuation =
-    if last_step then
-      (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
-      let todo = [just'] in
-      let todo = if mustdot status then List.append todo [dot_tac] else todo
+      let continuation =
+        if last_step then
+          (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
+          let todo = [just'] @ (done_continuation status) in
+          (*       let todo = if mustdot status then List.append todo [dot_tac] else todo *)
+          (*       in *)
+          block_tac todo
+        else
+          let (_,_,rhs) = rhs in
+          block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
+                                               rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
       in
-      block_tac todo
-    else
-      let (_,_,rhs) = rhs in
-      block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
-                                           rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
-  in
-  prepare continuation
+      prepare continuation
+    )
+  else
+    fail (lazy "You are not building an equality chain")
 ;;
 
 let rec pp_metasenv_names (metasenv:NCic.metasenv) =
@@ -382,24 +459,51 @@ let print_goals_names_tac s (status:#NTacStatus.tac_status) =
   let (_,_,metasenv,_,_) = status#obj in
   prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
 
+(* Useful as it does not change the order in the list *)
+let rec list_change_assoc k v = function
+    [] -> []
+  | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+;;
+
 let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
-  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
-  let rec remove_name_from_metaattrs mattrs =
-    match mattrs with
-      [] -> []
-    | hd :: tl ->
-      match hd with
-        `Name n -> remove_name_from_metaattrs tl
-      | _ as it -> it :: (remove_name_from_metaattrs tl)
+  let add_name_to_goal name goal metasenv =
+    let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in
+    let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+    let newconj = (mattrs,ctx,t) in
+    list_change_assoc goal newconj metasenv
+  in
+  let new_goals =
+    (* It's important that this tactic is called before branching and right after the creation of
+     * the new goals, when they are still under focus *)
+    match status#stack with
+      [] -> fail (lazy "Can not add names to an empty stack")
+    | (g,_,_,_,_) :: tl -> 
+      let rec sublist n = function
+          [] -> []
+        | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
+      in
+      List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+  in
+  let rec add_names_to_goals g cl metasenv =
+    match g,cl with
+      [],[] -> metasenv
+    | hd::tl, (_,consname,_)::tl' -> 
+      add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+    | _,_ -> fail (lazy "There are less goals than constructors")
   in
+  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+  let newmetasenv = add_names_to_goals new_goals !cl metasenv
+  in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+;;
+(*
+  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+  let remove_name_from_metaattrs =
+   List.filter (function `Name _ -> false | _ -> true) in
   let rec add_names_to_metasenv cl metasenv =
-    match cl with
-      [] -> metasenv
-    | hd :: tl ->
-      let _,consname,_ = hd
-      in match metasenv with
-        [] -> []
-      | mhd :: mtl ->
+    match cl,metasenv with
+      [],_ -> metasenv
+    | hd :: tl, mhd :: mtl ->
+      let _,consname,_ = hd in
         let gnum,conj = mhd in
         let mattrs,ctx,t = conj in
         let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
@@ -407,9 +511,17 @@ let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.ta
         let newconj = mattrs,ctx,t in
         let newmeta = gnum,newconj in
         newmeta :: (add_names_to_metasenv tl mtl)
+    | _,[] -> assert false
   in
   let newmetasenv = add_names_to_metasenv !cl metasenv in
   status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
+*)
+
+let unfocus_branch_tac status =
+  match status#stack with
+    [] -> status
+  | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
+;;
 
 let we_proceed_by_induction_on t1 t2 status =
   let goal = extract_first_goal_from_status status in
@@ -431,16 +543,22 @@ let we_proceed_by_induction_on t1 t2 status =
                     (match !sort with NCic.Sort x -> x | _ -> assert false))
            in
            let eliminator =
-             let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
-             (* Generating as many implicits as open goals *)
-             let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
+             let l = [Ast.Ident (name,None)] in
+             (* Generating an implicit for each argument of the inductive type, plus one the
+              * predicate, plus an implicit for each constructor of the inductive type *)
+             let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
              let _,_,t1 = t1 in
              let l = l @ [t1] in
              Ast.Appl l
            in
            cl := ity.cl;
            exact_tac ("",0,eliminator) status);
-        add_names_to_goals_tac cl; dot_tac] status)
+        add_names_to_goals_tac cl; 
+        branch_tac; 
+        push_goals_tac;
+        unfocus_branch_tac;
+        add_parameter_tac "context" "induction"
+      ] status)
   with
   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 ;;
@@ -455,14 +573,15 @@ let we_proceed_by_cases_on ((txt,len,ast1) as t1)  t2 status =
         analyze_indty_tac ~what:npt1 indtyinfo;
         cases_tac ~what:t1 ~where:("",0,(None,[],Some
                                            Ast.UserInput));
-        print_goals_names_tac "Pre Adding";
         (
           fun status ->
             let ity = HExtlib.unopt !indtyinfo in
             cl := ity.cl; add_names_to_goals_tac cl status
         );
-        print_goals_names_tac "Post Adding";
-        dot_tac] status)
+        branch_tac; push_goals_tac;
+        unfocus_branch_tac;
+        add_parameter_tac "context" "cases"
+      ] status)
   with
   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 ;;
@@ -491,8 +610,14 @@ let rec loc_of_goal goal l =
     else loc_of_goal goal tl
 ;;
 
+let has_focused_goal status =
+  match status#stack with
+    [] -> false
+  | ([],_,_,_,_) :: tl -> false
+  | _ -> true
+;;
+
 let focus_on_case_tac case status =
-  let goal = extract_first_goal_from_status status in
   let (_,_,metasenv,_,_) = status#obj in
   let rec goal_of_case case metasenv =
     match metasenv with
@@ -505,28 +630,52 @@ let focus_on_case_tac case status =
   let gstatus =
     match status#stack with
       [] -> fail (lazy "There is nothing to prove")
-    | (g,t,k,tag) :: s ->
-      let loc = loc_of_goal goal_to_focus k in
-      let curloc = loc_of_goal goal g in
-      (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s
-  in status#set_stack gstatus
+    | (g,t,k,tag,p) :: s ->
+      let loc = 
+        try 
+          loc_of_goal goal_to_focus t 
+        with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
+        context")
+      in
+      let curloc = if has_focused_goal status then 
+          let goal = extract_first_goal_from_status status in
+          [loc_of_goal goal g]
+        else []
+      in
+      (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
+  in 
+  status#set_stack gstatus
+;;
 
 let case id l status =
-  let goal = extract_first_goal_from_status status in
-  let (_,_,metasenv,_,_) = status#obj in
-  let conj = NCicUtils.lookup_meta goal metasenv in
-  let name = name_of_conj conj in
-  let continuation =
-    let rec aux l =
-      match l with
-        [] -> [id_tac]
-      | (id,ty)::tl ->
-        (try_tac (assume id ("",0,ty) None)) :: (aux tl)
-    in
-    aux l
-  in
-  if name = id then block_tac continuation status
-  else block_tac ([focus_on_case_tac id] @ continuation) status
+  let ctx = status_parameter "context" status in
+  if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
+  induction/cases analysis context")
+else
+  (
+    if has_focused_goal status then fail (lazy "Finish the current case before switching")
+    else
+      (
+(*
+        let goal = extract_first_goal_from_status status in
+        let (_,_,metasenv,_,_) = status#obj in
+        let conj = NCicUtils.lookup_meta goal metasenv in
+        let name = name_of_conj conj in
+*)
+        let continuation =
+          let rec aux l =
+            match l with
+              [] -> [id_tac]
+            | (id,ty)::tl ->
+              (try_tac (assume id ("",0,ty) None)) :: (aux tl)
+          in
+          aux l
+        in
+(*         if name = id then block_tac continuation status *)
+(*         else  *)
+          block_tac ([focus_on_case_tac id] @ continuation) status
+      )
+  )
 ;;
 
 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;