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

1 files changed, 12 insertions, 11 deletions

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)