Corrects the way conjunctions, existential quantifications, and arrows are

treated in eliminations for proof-by-pointing.


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

1 files changed, 38 insertions, 21 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 6676d29ee..4fb3fbe38 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -21,6 +21,8 @@ open Topconstr;;
 
 let zz = (0,0);;
 
+let hyp_radix = id_of_string "H";;
+
 (* get_hyp_by_name : goal sigma -> string -> constr,
    looks up for an hypothesis (or a global constant), from its name *)
 let get_hyp_by_name g name =
@@ -122,7 +124,7 @@ let (forall_intro: pbp_rule) = function
 let (imply_intro2: pbp_rule) = function
   avoid, clear_names,
   clear_flag, None, Prod(Anonymous, _, body), 2::path, f ->
-   let h' = next_global_ident_away (id_of_string "H") avoid in
+   let h' = next_global_ident_away hyp_radix avoid in
      Some(chain_tactics [make_named_intro h']
           (f (h'::avoid) clear_names clear_flag None (kind_of_term body) path))
   | _ -> None;;
@@ -131,7 +133,7 @@ let (imply_intro2: pbp_rule) = function
 let (imply_intro1: pbp_rule) = function
   avoid, clear_names,
   clear_flag, None, Prod(Anonymous, prem, body), 1::path, f ->
-   let h' = next_global_ident_away (id_of_string "H") avoid in
+   let h' = next_global_ident_away hyp_radix avoid in
    let str_h' = h' in
      Some(chain_tactics [make_named_intro str_h']
             (f (h'::avoid) clear_names clear_flag (Some str_h') 
@@ -186,7 +188,7 @@ let rec make_pbp_tactic = function
 let (forall_elim: pbp_rule) = function
   avoid, clear_names, clear_flag, 
   Some h, Prod(Name x, _, body), 2::path, f ->
-  let h' = next_global_ident_away (id_of_string "H") avoid in
+  let h' = next_global_ident_away hyp_radix avoid in
   let clear_names' = if clear_flag then h::clear_names else clear_names in
     Some
      (chain_tactics [PbpGeneralize (h,[x]); make_named_intro h']
@@ -198,12 +200,11 @@ let (imply_elim1: pbp_rule) = function
   avoid, clear_names, clear_flag,
   Some h, Prod(Anonymous, prem, body), 1::path, f ->
   let clear_names' = if clear_flag then h::clear_names else clear_names in
-  let h' = next_global_ident_away (id_of_string "H") avoid in
+  let h' = next_global_ident_away hyp_radix avoid in
   let str_h' = (string_of_id h') in
   Some(PbpThens
 	  ([PbpLApply h],
-	   [PbpThen [PbpIntros [h']];
-            make_clears (h::clear_names);
+	   [chain_tactics [PbpIntros [h']] (make_clears (h::clear_names));
 	    f avoid clear_names' false None (kind_of_term prem) path]))
   | _ -> None;;
 
@@ -212,7 +213,7 @@ let (imply_elim2: pbp_rule) = function
   avoid, clear_names, clear_flag,
   Some h, Prod(Anonymous, prem, body), 2::path, f ->
   let clear_names' = if clear_flag then h::clear_names else clear_names in
-  let h' = next_global_ident_away (id_of_string "H") avoid in
+  let h' = next_global_ident_away hyp_radix avoid in
   Some(PbpThens
 	 ([PbpLApply h],
           [chain_tactics [PbpIntros [h']]
@@ -315,7 +316,7 @@ let (not_intro: pbp_rule) = function
     App(not_oper, [|c1|]), 2::1::path, f ->
       if(is_matching_local (notconstr ()) not_oper) or 
 	(is_matching_local (notTconstr ()) not_oper) then
-	let h' = next_global_ident_away (id_of_string "H") avoid in
+	let h' = next_global_ident_away hyp_radix avoid in
 	Some(chain_tactics [PbpReduce;make_named_intro h']
 	       (f (h'::avoid) clear_names false (Some h') 
 		  (kind_of_term c1) path))
@@ -435,26 +436,42 @@ let (head_tactic_patt: pbp_rule) = function
        App(oper, [|c1; c2|]), 2::a::path) 
       when ((is_matching_local (andconstr()) oper) or
 	    (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
-	let h1 = next_global_ident_away (id_of_string "H") avoid in
-	let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in
+	let h1 = next_global_ident_away hyp_radix avoid in
+	let h2 = next_global_ident_away hyp_radix (h1::avoid) in
 	Some(PbpThens
-                  ([elim_with_bindings h str_list;
-		    make_named_intro h1;
-		    make_named_intro h2],
+                  ([elim_with_bindings h str_list],
 		    let cont_body = 
 		      if a = 1 then c1 else c2 in
 		    let cont_tac = 
 		      f (h2::h1::avoid) (h::clear_names) 
                         false (Some (if 1 = a then h1 else h2))
                         (kind_of_term cont_body) path in
-		    cont_tac::(auxiliary_goals
-					clear_names clear_flag
-					h nprems)))
+		      (chain_tactics 
+			 [make_named_intro h1; make_named_intro h2]
+			 cont_tac)::
+	       (auxiliary_goals clear_names clear_flag h nprems)))
+    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
+      when ((is_matching_local (exTconstr()) oper) && a = 2) or
+	    (((is_matching_local (exconstr ()) oper) or
+	      (is_matching_local (sigconstr ()) oper)) && a = 3) ->
+		   (match (kind_of_term c2) with
+		     Lambda(Name x, _,body) ->
+		       Some(PbpThens
+		    		 ([elim_with_bindings h str_list],
+				   let x' = next_global_ident_away x avoid in
+				   let cont_body =
+				     Prod(Name x', c1,
+					    mkProd(Anonymous, body, 
+						   mkVar(dummy_id))) in
+				   let cont_tac 
+				       = f avoid (h::clear_names) false None
+				       cont_body (2::1::path) in
+				   cont_tac::(auxiliary_goals
+						       clear_names clear_flag
+						       h nprems)))
+		     | _ -> None)
     | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
-      when ((is_matching_local (exconstr ()) oper) or
-	    (is_matching_local (exTconstr ()) oper) or
-	    (is_matching_local (sigconstr ()) oper) or
-	    (is_matching_local (sigTconstr()) oper)) & a = 2 ->
+      when ((is_matching_local (sigTconstr()) oper)) & a = 2 ->
 		   (match (kind_of_term c2),path with
 		     Lambda(Name x, _,body), (2::path) ->
 		       Some(PbpThens
@@ -481,7 +498,7 @@ let (head_tactic_patt: pbp_rule) = function
 		      let cont_body =
 			if a = 1 then c1 else c2 in
                       (* h' is the name for the new intro *)
-		      let h' = next_global_ident_away (id_of_string "H") avoid in
+		      let h' = next_global_ident_away hyp_radix avoid in
 		      let cont_tac =
                         chain_tactics 
 			  [make_named_intro h']