From 940da8a791b8b1c704f28662fa2e6a8f3ddf040f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 Sep 2017 18:57:18 +0200
Subject: Adding quotations for the assert family of tactics.

---
 src/tac2stdlib.ml | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

(limited to 'src/tac2stdlib.ml')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 07b01b1174..5f61081a76 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -144,6 +144,17 @@ let to_induction_clause = function
 | _ ->
   assert false
 
+let to_assertion = function
+| ValBlk (0, [| ipat; t; tac |]) ->
+  let to_tac t = Proofview.tclIGNORE (thaw t) in
+  let ipat = Value.to_option to_intro_pattern ipat in
+  let t = Value.to_constr t in
+  let tac = Value.to_option to_tac tac in
+  AssertType (ipat, t, tac)
+| ValBlk (1, [| id; c |]) ->
+  AssertValue (Value.to_ident id, Value.to_constr c)
+| _ -> assert false
+
 let to_multi = function
 | ValBlk (0, [| n |]) -> Precisely (Value.to_int n)
 | ValBlk (1, [| n |]) -> UpTo (Value.to_int n)
@@ -256,12 +267,9 @@ let () = define_prim1 "tac_generalize" begin fun cl ->
   Tactics.new_generalize_gen cl
 end
 
-let () = define_prim3 "tac_assert" begin fun c tac ipat ->
-  let c = Value.to_constr c in
-  let of_tac t = Proofview.tclIGNORE (thaw t) in
-  let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
-  let ipat = Value.to_option to_intro_pattern ipat in
-  Tac2tactics.forward true tac ipat c
+let () = define_prim1 "tac_assert" begin fun ast ->
+  let ast = to_assertion ast in
+  Tac2tactics.assert_ ast
 end
 
 let () = define_prim3 "tac_enough" begin fun c tac ipat ->
-- 
cgit v1.2.3