Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'appliquer au but; appel optionnel de Intros Until sur certaines tactiques

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

4 files changed, 71 insertions, 63 deletions

diff --git a/tactics/Equality.v b/tactics/Equality.v
index a6e138857d..317e114745 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -13,14 +13,14 @@ Declare ML Module "equality".
 Grammar tactic simple_tactic: ast :=
   replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
 
-| deqhyp   [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)]
+| deqhyp   [ "Simplify_eq" ident_or_numarg($id) ] -> [(DEqHyp $id)]
 | deqconcl [ "Simplify_eq" ] -> [(DEqConcl)]
 
-| discr_id [ "Discriminate" identarg($id) ] -> [(DiscrHyp $id)]
+| discr_id [ "Discriminate" ident_or_numarg($id) ] -> [(DiscrHyp $id)]
 | discr    [ "Discriminate" ] -> [(Discr)]
 
 | inj    [ "Injection" ] -> [(Inj)]
-| inj_id [ "Injection" identarg($id) ] -> [(InjHyp $id)]
+| inj_id [ "Injection" ident_or_numarg($id) ] -> [(InjHyp $id)]
 
 | rewriteLR [ "Rewrite" "->" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
 | rewriteRL [ "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))]
diff --git a/tactics/Inv.v b/tactics/Inv.v
index 36316ec811..12633311df 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -34,16 +34,16 @@ Syntax tactic level 0:
 
 
 Grammar tactic simple_tactic: ast :=
-  inversion    [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
+  inversion    [ inversion_com($ic) ident_or_numarg($id) ] -> [(Inv $ic $id)]
 | inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
       -> [(InvIn $ic $id ($LIST $l))]
-| dep_inv   [ "Dependent" inversion_com($ic) identarg($id) ]
+| dep_inv   [ "Dependent" inversion_com($ic) ident_or_numarg($id) ]
      -> [(DInv $ic $id)]
 | dep_inv_with
-   [ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ]
+   [ "Dependent" inversion_com($ic) ident_or_numarg($id) "with" constrarg($c) ]
      -> [(DInvWith $ic $id $c) ]
 
-| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
+| inv_using [ inversion_com($ic) ident_or_numarg($id) "using" constrarg($c) ]
      -> case [$ic] of
           Inversion -> [(UseInversionLemma $id $c)]
         esac
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 1c4990143a..4e0c39ab26 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -195,7 +195,7 @@ let rec dependent_hyps id idlist sign =
 
 let generalizeRewriteIntros tac depids id gls = 
   let dids = dependent_hyps id depids (pf_env gls) in
-  (tclTHEN (bring_hyps (List.map in_some dids))
+  (tclTHEN (bring_hyps dids)
      (tclTHEN tac
 	(introsReplacing dids)))
   gls
@@ -222,39 +222,39 @@ let dest_eq gls t =
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
 
-let projectAndApply thin cls depids gls =
-  let subst_hyp_LR cls = tclTRY(hypSubst (out_some cls)  None) in
-  let subst_hyp_RL cls = tclTRY(revHypSubst (out_some cls) None) in
+let projectAndApply thin id depids gls =
+  let subst_hyp_LR id = tclTRY(hypSubst id None) in
+  let subst_hyp_RL id = tclTRY(revHypSubst id None) in
   let subst_hyp gls = 
-    let orient_rule cls = 
-      let (t,t1,t2) = dest_eq gls (clause_type cls gls) in
+    let orient_rule id = 
+      let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id) in
       match (kind_of_term (strip_outer_cast t1),
 	     kind_of_term (strip_outer_cast t2)) with
-        | IsVar id1, _ -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1
-        | _, IsVar id2 -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2
-        | _ -> subst_hyp_RL cls
+        | IsVar id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1
+        | _, IsVar id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2
+        | _ -> subst_hyp_RL id
     in 
     onLastHyp orient_rule gls 
   in
-  let (t,t1,t2) = dest_eq gls (clause_type cls gls)  in
+  let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id)  in
   match (thin, kind_of_term (strip_outer_cast t1), kind_of_term (strip_outer_cast t2)) with
     | (true, IsVar id1,  _) -> generalizeRewriteIntros
-          (tclTHEN (subst_hyp_LR cls) (clear_clause cls)) depids id1 gls
+          (tclTHEN (subst_hyp_LR id) (clear_clause id)) depids id1 gls
     | (false, IsVar id1,  _) ->
-        generalizeRewriteIntros (subst_hyp_LR cls) depids id1 gls
+        generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
     | (true, _ , IsVar id2) -> generalizeRewriteIntros
-          (tclTHEN (subst_hyp_RL cls) (clear_clause cls)) depids id2 gls
+          (tclTHEN (subst_hyp_RL id) (clear_clause id)) depids id2 gls
     | (false, _ , IsVar id2) ->
-        generalizeRewriteIntros (subst_hyp_RL cls) depids id2 gls
+        generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
     | (true, _, _) ->
         let deq_trailer neqns =
           tclDO neqns
             (tclTHEN intro (tclTHEN subst_hyp (onLastHyp clear_clause)))
         in 
-	(tclTHEN (tclTRY (dEqThen deq_trailer cls)) (clear_clause cls)) gls
+	(tclTHEN (tclTRY (dEqThen deq_trailer (Some id))) (clear_one id)) gls
     | (false, _, _) -> 
         let deq_trailer neqns = tclDO neqns (tclTHEN intro subst_hyp) in 
-	(tclTHEN (dEqThen deq_trailer cls) (clear_clause cls)) gls
+	(tclTHEN (dEqThen deq_trailer (Some id)) (clear_one id)) gls
 
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
@@ -269,24 +269,23 @@ let case_trailer_gene othin neqns ba gl =
                   (tclDO neqns
                      (tclTHEN intro
                         (onLastHyp
-                           (fun cls ->
-                              tclTRY (projectAndApply thin cls depids)))))
+                           (fun id ->
+                              tclTRY (projectAndApply thin id depids)))))
 		  (tclTHEN
-                     (onCL (compose List.rev (afterHyp (out_some last))) 
-			bring_hyps)
-                     (onCL (afterHyp (out_some last)) clear_clauses))))
+                     (onHyps (compose List.rev (afterHyp last)) bring_hyps)
+                     (onHyps (afterHyp last) clear))))
       | None -> tclIDTAC
   in
   (tclTHEN (tclDO neqns intro)
-     (tclTHEN (bring_hyps (List.map in_some nodepids))
-	(tclTHEN (clear_clauses (List.map in_some nodepids))
-	   (tclTHEN (onCL (compose List.rev (nLastHyps neqns)) bring_hyps)
-	      (tclTHEN (onCL (nLastHyps neqns) clear_clauses)
+     (tclTHEN (bring_hyps nodepids)
+	(tclTHEN (clear_clauses nodepids)
+	   (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
+	      (tclTHEN (onHyps (nLastHyps neqns) clear_clauses)
 		 (tclTHEN rewrite_eqns
 		    (tclMAP (fun id ->
-			       (tclORELSE (clear_clause (Some id))
-				  (tclTHEN (bring_hyps [Some id])
-				     (clear_clause (Some id)))))
+			       (tclORELSE (clear_clause id)
+				  (tclTHEN (bring_hyps [id])
+				     (clear_one id))))
 		       depids)))))))
   gl
 
@@ -300,22 +299,22 @@ let case_trailer othin neqns ba gl =
   let rewrite_eqns =
     match othin with
       | Some thin ->
-          (tclTHEN (onCL (compose List.rev (nLastHyps neqns)) bring_hyps)
-             (tclTHEN (onCL (nLastHyps neqns) clear_clauses)
+          (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
+             (tclTHEN (onHyps (nLastHyps neqns) clear_clauses)
 		(tclTHEN
 		   (tclDO neqns
                       (tclTHEN intro
 			 (onLastHyp
-			    (fun cls -> 
-			       tclTRY (projectAndApply thin cls depids)))))
+			    (fun id -> 
+			       tclTRY (projectAndApply thin id depids)))))
 		   (tclTHEN (tclDO (List.length nodepids) intro)
 		      (tclMAP (fun id -> 
-				 tclTRY (clear_clause (Some id))) depids)))))
+				 tclTRY (clear_clause id)) depids)))))
       | None -> tclIDTAC
   in
   (tclTHEN (tclDO neqns intro)
-     (tclTHEN (bring_hyps (List.map in_some nodepids))
-	(tclTHEN (clear_clauses (List.map in_some nodepids))
+     (tclTHEN (bring_hyps nodepids)
+	(tclTHEN (clear_clauses nodepids)
 	   rewrite_eqns)))
   gl
 
@@ -365,9 +364,9 @@ let res_case_then gene thin indbinding id status gl =
   (tclTHENS
      (cut_intro cut_concl)
      [onLastHyp
-        (fun cls->
+        (fun id ->
            (tclTHEN (applyUsing
-                       (applist(mkVar (out_some cls),
+                       (applist(mkVar id,
                                 list_tabulate
                                   (fun _ -> mkMeta(Clenv.new_meta())) neqns)))
               Auto.default_auto));
@@ -408,7 +407,7 @@ let inv gene com status id =
   let inv_tac = res_case_then gene com [] id status in
   let tac =
     if com = Some true (* if Inversion_clear, clear the hypothesis *) then 
-      tclTHEN inv_tac (tclTRY (clear_clause (Some id)))
+      tclTHEN inv_tac (tclTRY (clear_clause id))
     else 
       inv_tac
   in 
@@ -428,13 +427,15 @@ let (half_inv_tac, inv_tac, inv_clear_tac) =
   let gentac =
     hide_tactic "Inv"
       (function
-	 | [ic; Identifier id] -> inv false (com_of_id ic) NoDep id
+	 | ic :: [id_or_num] ->
+	     tactic_try_intros_until (inv false (com_of_id ic) NoDep) id_or_num
 	 | l -> bad_tactic_args "Inv" l)
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
    (fun id -> gentac [inv_kind; Identifier id]),
    (fun id -> gentac [invclr_kind; Identifier id]))
 
+
 (* Inversion without intros. No vernac entry yet! *)
 let named_inv =
   let gentac =
@@ -450,7 +451,9 @@ let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
   let gentac =
     hide_tactic "DInv"
       (function
-	 | [ic; Identifier id] -> inv false (com_of_id ic) (Dep None) id
+	 | ic :: [id_or_num] ->
+	     tactic_try_intros_until (inv false (com_of_id ic) (Dep None))
+	       id_or_num
 	 | l -> bad_tactic_args "DInv" l)
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
@@ -462,12 +465,16 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
   let gentac =
     hide_tactic "DInvWith"
       (function
-	 | [ic; Identifier id; Command com] ->
-             fun gls -> 
-	       inv false (com_of_id ic)
-		 (Dep (Some (pf_interp_constr gls com))) id gls
-	 | [ic; Identifier id; Constr c] ->
-             fun gls -> inv false (com_of_id ic) (Dep (Some c)) id gls
+	 | [ic; id_or_num; Command com] ->
+	     tactic_try_intros_until
+               (fun id gls -> 
+		  inv false (com_of_id ic)
+		    (Dep (Some (pf_interp_constr gls com))) id gls)
+	       id_or_num
+	 | [ic; id_or_num; Constr c] ->
+	     tactic_try_intros_until
+               (fun id gls -> inv false (com_of_id ic) (Dep (Some c)) id gls)
+	       id_or_num
 	 | l -> bad_tactic_args "DInvWith" l)
   in
   ((fun id c -> gentac [hinv_kind; Identifier id; Constr c]),
@@ -490,7 +497,7 @@ let invIn com id ids gls =
       (tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids)) gls
   in
   try 
-    (tclTHEN (bring_hyps (List.map in_some ids))
+    (tclTHEN (bring_hyps ids)
        (tclTHEN (inv false com NoDep id)
           (intros_replace_ids)))
     gls
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e168287afd..f7bf462dc7 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -209,9 +209,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   *)
   let invSign = named_context invEnv in
   let pfs = mk_pftreestate (mk_goal (mt_ctxt Intset.empty) invSign invGoal) in
-  let pfs =
-    solve_pftreestate (tclTHEN intro 
-			 (onLastHyp (compose inv_op out_some))) pfs in
+  let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
   let global_named_context = Global.named_context () in
   let ownSign =
@@ -352,10 +350,14 @@ let useInversionLemma =
   let gentac =
     hide_tactic "UseInversionLemma"
       (function
-	 | [Identifier id; Command com] ->
-             fun gls -> lemInv id (pf_interp_constr gls com) gls
-	 | [Identifier id; Constr c] ->
-             fun gls -> lemInv id c gls
+	 | [id_or_num; Command com] ->
+	     tactic_try_intros_until
+               (fun id gls -> lemInv id (pf_interp_constr gls com) gls)
+	       id_or_num
+	 | [id_or_num; Constr c] ->
+	     tactic_try_intros_until
+               (fun id gls -> lemInv id c gls)
+	       id_or_num
 	 | l  -> bad_vernac_args "useInversionLemma" l)
   in 
   fun id c -> gentac [Identifier id;Constr c]
@@ -369,8 +371,7 @@ let lemInvIn id c ids gls =
       (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) gls
   in 
 (*  try *)
-    ((tclTHEN (tclTHEN (bring_hyps (List.map in_some ids))
-		 (lemInv id c))
+    ((tclTHEN (tclTHEN (bring_hyps ids) (lemInv id c))
         (intros_replace_ids)) gls)
 (*  with Not_found -> errorlabstrm "LemInvIn" (not_found_message ids)
     |  UserError(a,b) -> errorlabstrm "LemInvIn" b