Export eassumption

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

2 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4d1e687f0e..d9adabaf75 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,7 @@ Tactics
 - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
 - New introduction pattern "?" for letting Coq choose a name
+- Added "eassumption"
 
 Modules
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 232266e262..0a611e6552 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -40,6 +40,10 @@ let assumption id = e_give_exact (mkVar id)
 let e_assumption gl = 
   tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
 
+TACTIC EXTEND eassumption
+| [ "eassumption" ] -> [ e_assumption ]
+END
+
 let e_resolve_with_bindings_tac  (c,lbind) gl = 
   let t = pf_hnf_constr gl (pf_type_of gl c) in 
   let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in