Ajout "simple apply" et "simple eapply" pour apply sans unfold

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

3 files changed, 7 insertions, 6 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index be99bdde0a..0680cc23e5 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 NoBindings)
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (false,(make_var h,NoBindings)))
+  | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
   | 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 e3f6572020..20c1cc04f5 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,7 @@ 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,_)) -> 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 0e57982106..f442bf75ff 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1143,10 +1143,11 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (false,(c,bindl)) ->
+    | TacApply (true,false,(c,bindl)) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (true,(c,bindl)) ->
+    | TacApply (true,true,(c,bindl)) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
+    | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
     | TacConstructor (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)
@@ -1984,7 +1985,7 @@ let rec xlate_vernac =
    | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
    | VernacSyntacticDefinition (id, ([],c), false, _) ->
        CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
-   | VernacSyntacticDefinition (id, _, true, _) ->
+   | VernacSyntacticDefinition (id, _, _, _) ->
        xlate_error"TODO: Local abbreviations and abbreviations with parameters"
   (* Modules and Module Types *)
    | VernacInclude (_) -> xlate_error "TODO : Include "
@@ -2202,7 +2203,7 @@ let rec xlate_vernac =
      VernacMemOption (_, _)|VernacRemoveOption (_, _)
   | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
     VernacSolveExistential (_, _)|VernacCanonical _ |
-     VernacTacticNotation _)
+     VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _)
     -> xlate_error "TODO: vernac";;
 
 let rec xlate_vernac_list =