From b6c3f54d04ce441ac68ffabfca69c18847707518 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Aug 2014 17:16:58 +0200
Subject: A reorganization of the "assert" tactics (hopefully uniform naming
 scheme, redundancies, possibility of chaining a tactic knowing the name of
 introduced hypothesis, new proof engine).

---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 702d554fc5..5e915228e4 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -109,7 +109,7 @@ let clean_tmp gls =
     clean_all (tmp_ids gls) gls
 
 let assert_postpone id t =
-  assert_tac (Name id) t
+  assert_before (Name id) t
 
 (* start a proof *)
 
-- 
cgit v1.2.3