From 30cf9c6711df3eb583dacad3cb98158adbbf1f5f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 6 Oct 2012 10:08:48 +0000
Subject: remove useless hidden_flag in TacMutual(Co)Fix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 52b4d881a3..f431e04d83 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1206,7 +1206,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    then
 	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
-	      h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
+	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos
 	| _ -> anomaly "Not a valid information"
     in
-- 
cgit v1.2.3