About "apply in":

- Added "simple apply in" (cf wish 1917) + conversion and descent
  under conjunction + contraction of useless beta-redex in "apply in"
  + support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
  is type-checked using a kernel conversion in the opposite side of what
  the proof indicated (hence leading to a potential unexpected penalty
  at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
  temporary evars as intermediate steps but this was too long to implement.

Smoother API in tactics.mli for assert_by/assert_as/pose_proof.



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

3 files changed, 39 insertions, 33 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 809e5bec35..1f4aa8b24f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -364,10 +364,14 @@ GEXTEND Gram
     [ [ "*"; occs = occs -> occs
       | -> no_occurrences_expr ] ]
   ;
-  simple_clause:
+  in_hyp_list:
     [ [ "in"; idl = LIST1 id_or_meta -> idl
       | -> [] ] ]
   ;
+  in_hyp_as:
+    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
+      | -> None ] ]
+  ;
   orient: 
     [ [ "->" -> true 
       | "<-" -> false
@@ -406,9 +410,9 @@ GEXTEND Gram
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
-  with_names:
-    [ [ "as"; ipat = simple_intropattern -> ipat
-      | -> dummy_loc,IntroAnonymous ] ]
+  as_ipat:
+    [ [ "as"; ipat = simple_intropattern -> Some ipat
+      | -> None ] ]
   ;
   with_inversion_names:
     [ [ "as"; ipat = disjunctive_intropattern -> Some ipat
@@ -473,13 +477,14 @@ GEXTEND Gram
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
       | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
-      | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," ->
-	  TacApply (true,false,cl)
-      | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," ->
-          TacApply (true,true,cl)
-      | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," 
-          -> TacApply (false,false,cl)
-      | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ","           -> TacApply (false,true,cl)
+      | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","; 
+          inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
+      | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ",";
+          inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp)
+      | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+          inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp)
+      | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP",";
+          inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp)
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (false,cl,el)
       | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
@@ -511,15 +516,15 @@ GEXTEND Gram
       (* Begin compatibility *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; 
 	  c = lconstr; ")" -> 
-	  TacAssert (None,(loc,IntroIdentifier id),c)
+	  TacAssert (None,Some (loc,IntroIdentifier id),c)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; 
 	  c = lconstr; ")"; tac=by_tactic -> 
-	  TacAssert (Some tac,(loc,IntroIdentifier id),c)
+	  TacAssert (Some tac,Some (loc,IntroIdentifier id),c)
       (* End compatibility *)
 
-      | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
+      | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
 	  TacAssert (Some tac,ipat,c)
-      | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = with_names ->
+      | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
 	  TacAssert (None,ipat,c)
 
       | IDENT "cut"; c = constr -> TacCut c
@@ -620,18 +625,18 @@ GEXTEND Gram
 	    TacInversion (DepInversion (k,co,ids),hyp)
       | IDENT "simple"; IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = with_inversion_names;
-	  cl = simple_clause ->
+	  cl = in_hyp_list ->
 	    TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
       | IDENT "inversion"; 
 	  hyp = quantified_hypothesis; ids = with_inversion_names;
-	  cl = simple_clause ->
+	  cl = in_hyp_list ->
 	    TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
       | IDENT "inversion_clear"; 
 	  hyp = quantified_hypothesis; ids = with_inversion_names; 
-	  cl = simple_clause ->
+	  cl = in_hyp_list ->
 	    TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
       | IDENT "inversion"; hyp = quantified_hypothesis; 
-	  "using"; c = constr; cl = simple_clause ->
+	  "using"; c = constr; cl = in_hyp_list ->
 	    TacInversion (InversionUsing (c,cl), hyp)
 
       (* Conversion *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 77eec5e609..78d5cc9267 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -123,10 +123,6 @@ let pr_with_constr prc = function
   | None -> mt ()
   | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
 
-let pr_with_names = function
-  | None -> mt ()
-  | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
-
 let rec pr_message_token prid = function
   | MsgString s -> qs s
   | MsgInt n -> int n
@@ -379,9 +375,9 @@ let pr_with_inversion_names = function
   | None -> mt ()
   | Some ipat -> pr_as_intro_pattern ipat
 
-let pr_with_names = function
-  | _,IntroAnonymous -> mt ()
-  | ipat -> pr_as_intro_pattern ipat
+let pr_as_ipat = function
+  | None -> mt ()
+  | Some ipat -> pr_as_intro_pattern ipat
 
 let pr_as_name = function
   | Anonymous -> mt ()
@@ -400,7 +396,7 @@ let pr_assertion _prlc prc ipat c = match ipat with
       spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
 *)
   | ipat ->
-      spc() ++ prc c ++ pr_with_names ipat
+      spc() ++ prc c ++ pr_as_ipat ipat
 
 let pr_assumption prlc prc ipat c = match ipat with
 (* Use this "optimisation" or use only the general case ?
@@ -408,7 +404,7 @@ let pr_assumption prlc prc ipat c = match ipat with
       spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
 *)
   | ipat ->
-      spc() ++ prc c ++ pr_with_names ipat
+      spc() ++ prc c ++ pr_as_ipat ipat
 
 let pr_by_tactic prt = function
   | TacId [] -> mt ()
@@ -429,6 +425,10 @@ let pr_simple_clause pr_id = function
   | [] -> mt ()
   | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
 
+let pr_in_hyp_as pr_id = function
+  | None -> mt ()
+  | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat
+
 let pr_clauses pr_id = function
   | { onhyps=None; concl_occs=occs } ->
       if occs = no_occurrences_expr then pr_in (str " * |-")
@@ -702,10 +702,11 @@ and pr_atom1 = function
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
   | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
-  | TacApply (a,ev,cb) ->
+  | TacApply (a,ev,cb,inhyp) ->
       hov 1 ((if a then mt() else str "simple ") ++
              str (with_evars ev "apply") ++ spc () ++ 
-             prlist_with_sep pr_coma pr_with_bindings cb)
+             prlist_with_sep pr_coma pr_with_bindings cb ++
+             pr_in_hyp_as pr_ident inhyp)
   | TacElim (ev,cb,cbo) ->
       hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ 
         pr_opt pr_eliminator cbo)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 9c1a10b0ec..fc5df1a6c4 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -308,8 +308,8 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacVmCastNoCheck c ->
       <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
-  | Tacexpr.TacApply (b,false,cb) ->
-      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >>
+  | Tacexpr.TacApply (b,false,cb,None) ->
+      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
   | Tacexpr.TacElim (false,cb,cbo) ->
       let cb = mlexpr_of_constr_with_binding cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
@@ -345,7 +345,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
   | Tacexpr.TacAssert (t,ipat,c) ->
-      let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in
+      let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
       <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ 
 	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->