Adding "eassert", "eenough", "epose proof", which allow to state

a goal with unresolved evars.

6 files changed, 39 insertions, 24 deletions

diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1404b1c1f..c6a3beb89 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -552,24 +552,39 @@ GEXTEND Gram
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+	  c = lconstr; ")" ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "assert c as id by tac" *)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "enough c as id by tac" *)
       | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
+      | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c))
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c))
+      | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c))
       | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c))
+      | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
 
       | IDENT "generalize"; c = constr ->
 	  TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2b..22ecf61aa 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -768,15 +768,15 @@ type 'a extra_genarg_printer =
             primitive "cofix" ++ spc () ++ pr_id id ++ spc()
             ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
           )
-        | TacAssert (b,Some tac,ipat,c) ->
+        | TacAssert (ev,b,Some tac,ipat,c) ->
           hov 1 (
-            primitive (if b then "assert" else "enough") ++
+            primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
               pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
               pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
           )
-        | TacAssert (_,None,ipat,c) ->
+        | TacAssert (ev,_,None,ipat,c) ->
           hov 1 (
-            primitive "pose proof"
+            primitive (if ev then "epose proof" else "pose proof")
             ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
           )
         | TacGeneralize l ->
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index bf760e7bb..11e7278d9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -141,7 +141,7 @@ type 'a gen_atomic_tactic_expr =
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * 'tacexpr option option *
+      evars_flag * bool * 'tacexpr option option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e431a13bc..734ce46e4 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -489,8 +489,8 @@ let rec intern_atomic lf ist x =
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
-  | TacAssert (b,otac,ipat,c) ->
-      TacAssert (b,Option.map (Option.map (intern_pure_tactic ist)) otac,
+  | TacAssert (ev,b,otac,ipat,c) ->
+      TacAssert (ev,b,Option.map (Option.map (intern_pure_tactic ist)) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
                  intern_constr_gen false (not (Option.is_empty otac)) ist c)
   | TacGeneralize cl ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d1..d4ed77015 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -672,10 +672,7 @@ let pure_open_constr_flags = {
   expand_evars = false }
 
 (* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
-  let flags =
-    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
-    else open_constr_use_classes_flags () in
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
   interp_gen expected_type ist false flags env sigma c
 
 let interp_pure_open_constr ist =
@@ -1727,18 +1724,21 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
-  | TacAssert (b,t,ipat,c) ->
+  | TacAssert (ev,b,t,ipat,c) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
-        let (sigma,c) = 
-          (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
+        let (sigma,c) =
+          let expected_type =
+            if Option.is_empty t then WithoutTypeConstraint else IsType in
+          let flags = open_constr_use_classes_flags () in
+          interp_open_constr ~expected_type ~flags ist env sigma c
         in
         let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
         let tac = Option.map (Option.map (interp_tactic ist)) t in
-        Tacticals.New.tclWITHHOLES false
+        Tacticals.New.tclWITHHOLES ev
         (name_atomic ~env
-          (TacAssert(b,Option.map (Option.map ignore) t,ipat,c))
+          (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c))
           (Tactics.forward b tac ipat' c)) sigma
       end }
   | TacGeneralize cl ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4390ff08b..1ae792971 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
-  | TacAssert (b,otac,na,c) ->
-      TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na,
+  | TacAssert (ev,b,otac,na,c) ->
+      TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na,
                  subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)