From edface9ff8462a8ecbffd03074e51f589861d88a Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Fri, 31 Mar 2017 21:12:17 +0200
Subject: Bad correction in previous commit

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

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 85084badd5..d6a67219ff 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1588,7 +1588,7 @@ let prove_principle_for_gen
     match !tcc_lemma_ref with
      | Undefined -> error "No tcc proof !!"
      | Value lemma -> lemma
-     | Not_needed -> Coqlib.build_coq_True ()
+     | Not_needed -> Coqlib.build_coq_I ()
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
-- 
cgit v1.2.3