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

5 files changed, 16 insertions, 13 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3dd..e59de34a48 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -67,6 +67,7 @@ let explore_tree pfs =
     | Move (bool, identifier, identifier') -> "Move"
     | Rename (identifier, identifier') -> "Rename"
     | Change_evars -> "Change_evars"
+    | Order _ -> "Order"
   in
   let pt = proof_of_pftreestate pfs in
     (* We expect 0 *)
@@ -280,8 +281,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacExact          c
     | TacExactNoCheck   c
     | TacVmCastNoCheck  c  -> depends_of_'constr c acc
-    | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
-    | TacApply (_, _, _) -> failwith "TODO"
+    | TacApply (_, _, [cb], None) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, _, _) -> failwith "TODO"
     | TacElim (_, cwb, cwbo) ->
 	depends_of_'constr_with_bindings cwb
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -420,6 +421,7 @@ and depends_of_prim_rule pr acc = match pr with
   | Move _                       -> acc
   | Rename _                     -> acc
   | Change_evars                 -> acc
+  | Order _                      -> acc
 
 let rec depends_of_pftree pt acc =
   match pt.ref with
diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml
index b1244d1582..a157ca9254 100644
--- a/contrib/interface/paths.ml
+++ b/contrib/interface/paths.ml
@@ -23,4 +23,4 @@ let rec lex_smaller p1 p2 = match p1,p2 with
   [], _ -> true
 | a::tl1, b::tl2 when a < b -> true
 | a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
-| _ -> false;;
\ No newline at end of file
+| _ -> false;;
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 65eadf13db..01747aa58f 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
   | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
+  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings],None))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4b9c1332a4..cf861642db 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,8 @@ let rec natural_ntree ig ntree =
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
+	  | TacApply (_,false,[c,_],None) ->
+              natural_apply ig lh g gs (snd c) ltree
 	  | TacExact c -> natural_exact ig lh g gs (snd c) ltree
 	  | TacCut c -> natural_cut ig lh g gs (snd c) ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8ec6cfb2f4..b404478ffb 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1163,12 +1163,12 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (true,false,[c,bindl]) ->
+    | TacApply (true,false,[c,bindl],None) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (true,true,[c,bindl]) ->
+    | TacApply (true,true,[c,bindl],None) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (_,_,_) ->
-	xlate_error "TODO: simple (e)apply and iterated apply"
+    | TacApply (_,_,_,_) ->
+	xlate_error "TODO: simple (e)apply and iterated apply and apply in"
     | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1256,13 +1256,13 @@ and xlate_tac =
 		     but the structures are different *)
 		  xlate_clause cl)
     | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
-    | TacAssert (None, (_,IntroIdentifier id), c) -> 
+    | TacAssert (None, Some (_,IntroIdentifier id), c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (None, (_,IntroAnonymous), c) -> 
+    | TacAssert (None, None, c) -> 
         CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
-    | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) -> 
+    | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) -> 
         CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (Some (TacId []), (_,IntroAnonymous), c) -> 
+    | TacAssert (Some (TacId []), None, c) -> 
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"