adding an option Function_raw_tcc to Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11508 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 30 insertions, 17 deletions

diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index a3c169b7ec..4892128a06 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -508,5 +508,19 @@ let do_observe () =
       
       
     
+let strict_tcc = ref false
+let is_strict_tcc () = !strict_tcc 
+let strict_tcc_sig =
+  {
+    optsync = false;
+    optname = "Raw Function Tcc";
+    optkey =  PrimaryTable("Function_raw_tcc");
+    optread = (fun () -> !strict_tcc);
+    optwrite = (fun b -> strict_tcc := b)
+  }
+
+let _ = declare_bool_option strict_tcc_sig
+
+
 exception Building_graph of exn 
 exception Defining_principle of exn
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 7da1d6f0b4..2d741f0b35 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -115,3 +115,4 @@ val do_observe : unit -> bool
 exception Building_graph of exn 
 exception Defining_principle of exn
 
+val is_strict_tcc : unit -> bool
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 6227f92d72..8161e890dc 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -962,11 +962,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		       let ids' = pf_ids_of_hyps g in 
 		       lid := List.rev (list_subtract ids' ids);
 		       if !lid = [] then lid := [hid];
-(* 		       list_iter_i  *)
-(* 			 (fun i v ->  *)
-(* 			    msgnl (str "hyp" ++ int i ++ str " " ++  *)
-(* 				     Nameops.pr_id v ++ fnl () ++ fnl())) *)
-(* 			      !lid; *)
 		       tclIDTAC g
 		    )
 		    g
@@ -991,22 +986,25 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     sign
     gls_type 
     hook ;
-  by (
+  if Indfun_common.is_strict_tcc  ()
+  then
+    by (tclIDTAC) 
+  else by (
     fun g -> 
       tclTHEN 
 	(decompose_and_tac)
 	(tclORELSE 
-	(tclFIRST 
-	   (List.map
-	      (fun c -> 
-		 tclTHENSEQ
-		   [intros; 
-		    h_simplest_apply (interp_constr Evd.empty (Global.env()) c); 
-		    tclCOMPLETE Auto.default_auto
-		   ]
-	      )
-	      using_lemmas)
-	) tclIDTAC)
+	   (tclFIRST 
+	      (List.map
+		 (fun c -> 
+		    tclTHENSEQ
+		      [intros; 
+		       h_simplest_apply (interp_constr Evd.empty (Global.env()) c); 
+		       tclCOMPLETE Auto.default_auto
+		      ]
+		 )
+		 using_lemmas)
+	   ) tclIDTAC)
 	g);
   try
     by tclIDTAC; (* raises UserError _ if the proof is complete *)