From 9a63fdf0cad004d21ff9e937b08e7758e304bcd3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 11:40:52 +0200
Subject: Adding "eassert", "eenough", "epose proof", which allow to state a
 goal with unresolved evars.

---
 plugins/ltac/pptactic.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2ba..22ecf61aa2 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 ->
-- 
cgit v1.2.3


From be73d7eccd3e3165ce719b36910920e05cf416bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 11:53:37 +0200
Subject: Adding "epose", "eset", "eremember" which allow to set terms with
 evars.

This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.

Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
---
 plugins/ltac/pptactic.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 22ecf61aa2..4e254ea766 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -786,11 +786,11 @@ type 'a extra_genarg_printer =
               pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
               l
           )
-        | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
-          hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
-        | TacLetTac (na,c,cl,b,e) ->
+        | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
+          hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+        | TacLetTac (ev,na,c,cl,b,e) ->
           hov 1 (
-            (if b then primitive "set" else primitive "remember") ++
+            primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
               (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
                 else pr_pose_as_style pr.pr_constr na c) ++
               pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
-- 
cgit v1.2.3