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/funind/functional_principles_proofs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7f0db547d3..aba93de479 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -448,7 +448,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (Proofview.V82.of_tactic (assert_tac (Name rec_pte_id) t_x))
+		       (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x))
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
-- 
cgit v1.2.3