Remove some more "open" and dead code thanks to OCaml4 warnings

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

8 files changed, 3 insertions, 191 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3505c4d9b8..52b4d881a3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -134,19 +134,6 @@ let refine c =
 let thin l =
   Tacmach.thin_no_check l
 
-
-let cut_replacing id t tac :tactic=
-  tclTHENS (cut t)
-    [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
-      tac
-    ]
-
-let intro_erasing id = tclTHEN (thin [id]) (introduction id)
-
-
-
-let rec_hyp_id = id_of_string "rec_hyp"
-
 let is_trivial_eq t =
   let res =   try
     begin
@@ -367,7 +354,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     new_ctxt,new_end_of_type,simpl_eq_tac
 
 
-let is_property ptes_info t_x full_type_of_hyp =
+let is_property (ptes_info:ptes_info) t_x full_type_of_hyp =
   if isApp t_x
   then
     let pte,args = destApp t_x in
@@ -563,7 +550,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
     thin [hyp_id],[]
 
 
-let clean_goal_with_heq ptes_infos continue_tac dyn_infos  =
+let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) =
   fun g ->
     let env = pf_env g
     and sigma = project g
@@ -894,13 +881,6 @@ let build_proof
 
 
 (* Proof of principles from structural functions *)
-let is_pte_type t =
-  isSort ((strip_prod t))
-
-let is_pte (_,_,t) = is_pte_type t
-
-
-
 
 type static_fix_info =
     {
@@ -932,9 +912,6 @@ let prove_rec_hyp fix_info  =
     is_valid = fun _ -> true
   }
 
-
-exception Not_Rec
-
 let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in
@@ -1427,17 +1404,6 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     backtrack gls
 
 
-
-let build_clause eqs =
-  {
-    Locus.onhyps =
-      Some (List.map
-	      (fun id -> (Locus.AllOccurrences, id), Locus.InHyp)
-	      eqs
-	   );
-    Locus.concl_occs = Locus.NoOccurrences
-  }
-
 let rec rewrite_eqs_in_eqs eqs =
   match eqs with
     | [] -> tclIDTAC
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b97fc48f1d..a14b473936 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -289,22 +289,6 @@ let change_property_sort toSort princ princName =
 let pp_dur time time' =
   str (string_of_float (System.time_difference time time'))
 
-(* let qed () = save_named true  *)
-let defined () =
-  try
-    Lemmas.save_named false
-  with
-    | UserError("extract_proof",msg) ->
-	Errors.errorlabstrm
-	  "defined"
-	  ((try
-	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
-	    with _ -> mt ()
-	   ) ++msg)
-    | e -> raise e
-
-
-
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index dccbfa3b56..77c6dc4938 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -14,9 +14,7 @@ open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
-open Pcoq
 open Tacticals
-open Constr
 open Misctypes
 open Miscops
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b820489f53..61390bb1ad 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -288,10 +288,6 @@ let make_discr_match brl =
 	   make_discr_match_el el,
 	   make_discr_match_brl i brl)
 
-let pr_name = function
-  | Name id -> Ppconstr.pr_id id
-  | Anonymous -> str "_"
-
 (**********************************************************************)
 (*  functions used to build case expression from lettuple and if ones *)
 (**********************************************************************)
@@ -326,40 +322,6 @@ let build_constructors_of_type ind' argl =
 	     )
     ind.Declarations.mind_consnames
 
-(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
-let rec find_type_of nb b =
-  let f,_ = glob_decompose_app b in
-  match f with
-    | GRef(_,ref) ->
-	begin
-	  let ind_type  =
-	    match ref with
-	      | VarRef _ | ConstRef _ ->
-		  let constr_of_ref = constr_of_global ref in
-		  let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in
-		  let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in
-		  let ret_type,_ = decompose_app ret_type in
-		  if not (isInd ret_type) then
-		    begin
-(* 		      Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *)
-		      raise (Invalid_argument "not an inductive")
-		    end;
-		  destInd ret_type
-	      | IndRef ind -> ind
-	      | ConstructRef c -> fst c
-	  in
-	  let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in
-	  if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
-	  then raise (Invalid_argument "find_type_of : not a valid inductive");
-	  ind_type
-	end
-    | GCast(_,b,_) -> find_type_of nb b
-    | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *)
-    | _ -> raise (Invalid_argument "not a ref")
-
-
-
-
 (******************)
 (* Main functions *)
 (******************)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index edc727a48f..48ed144730 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -21,7 +21,7 @@ let is_rec_info scheme_info =
       Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
-  Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+  List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
 let choose_dest_or_ind scheme_info =
     if is_rec_info scheme_info
@@ -496,64 +496,6 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 let map_option f = function 
   | None -> None 
   | Some v -> Some (f v)
-    
-let decompose_lambda_n_assum_constr_expr = 
-  let rec decompose_lambda_n_assum_constr_expr acc n e = 
-  if n = 0 then (List.rev acc,e)
-  else
-    match e with 
-      | Constrexpr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e'
-      | Constrexpr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
-	let nal_length = List.length nal in 
-	if nal_length <= n 
-	then
-	  decompose_lambda_n_assum_constr_expr 
-	    (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
-	    (n - nal_length) 
-	    (Constrexpr.CLambdaN(lambda_loc,bl,e'))
-  	else
-	  let nal_keep,nal_expr = List.chop n nal in 
-	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
-	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
-	  )
-      | Constrexpr.CLetIn(_, na,nav,e') ->
-	decompose_lambda_n_assum_constr_expr 
-	  (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
-      | _ -> error "Not enough product or assumption"
-  in
-  decompose_lambda_n_assum_constr_expr []
-
-let decompose_prod_n_assum_constr_expr = 
-  let rec decompose_prod_n_assum_constr_expr acc n e = 
-    (* Pp.msgnl (str "n := " ++ int n ++ fnl ()++ *)
-    (* 		str "e := " ++ Ppconstr.pr_lconstr_expr e); *)
-  if n = 0 then 
-    (* let _ = Pp.msgnl (str "return_type := " ++ Ppconstr.pr_lconstr_expr e) in  *)
-      (List.rev acc,e)
-  else
-    match e with 
-      | Constrexpr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e'
-      | Constrexpr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
-	let nal_length = List.length nal in 
-	if nal_length <= n 
-	then
-	  (* let _ = Pp.msgnl (str "first case") in  *)
-	  decompose_prod_n_assum_constr_expr 
-	    (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
-	    (n - nal_length) 
-	    (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
-  	else
-	  (* let _ = Pp.msgnl (str "second case") in  *)
-	  let nal_keep,nal_expr = List.chop n nal in 
-	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
-	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
-	  )
-      | Constrexpr.CLetIn(_, na,nav,e') ->
-	decompose_prod_n_assum_constr_expr 
-	  (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
-      | _ -> error "Not enough product or assumption"
-  in
-  decompose_prod_n_assum_constr_expr []
 
 open Constrexpr
 open Topconstr
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2817c549dd..fb9116cc2d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -131,12 +131,6 @@ let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
-let constant sl s =
-  constr_of_global
-    (Nametab.locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
-
 let find_reference sl s =
     (Nametab.locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
@@ -277,7 +271,6 @@ let cache_Function (_,finfos) =
 
 
 let load_Function _  = cache_Function
-let open_Function _ = cache_Function
 let subst_Function (subst,finfos) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
@@ -508,12 +501,6 @@ let jmeq () =
      init_constant ["Logic";"JMeq"] "JMeq")
   with e -> raise (ToShow e)
 
-let jmeq_rec () =
-  try
-    Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-	  init_constant ["Logic";"JMeq"] "JMeq_rec"
-  with e -> raise (ToShow e)
-
 let jmeq_refl () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 5410e724a2..a811b29b84 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -853,17 +853,6 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
   lident , bindlist , Some cstr_expr , lcstor_expr
 
 
-
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
-  match rdecl with
-    | (nme,None,t) ->
-        let traw = Detyping.detype false [] [] t in
-        GProd (Loc.ghost,nme,Explicit,traw,t2)
-    | (_,Some _,_) -> assert false
-
-
-
-
 let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ec1994cd0c..a2f16dc6d8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -18,7 +18,6 @@ open Globnames
 open Nameops
 open Errors
 open Util
-open Closure
 open Tacticals
 open Tacmach
 open Tactics
@@ -50,10 +49,6 @@ let coq_base_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
     (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
 
-let coq_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition"
-    (Coqlib.init_modules @ Coqlib.arith_modules) s;;
-
 let find_reference sl s =
     (locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
@@ -126,7 +121,6 @@ let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
     (pf_type_of gls c)
 let h'_id = id_of_string "h'"
-let heq_id = id_of_string "Heq"
 let teq_id = id_of_string "teq"
 let ano_id = id_of_string "anonymous"
 let x_id = id_of_string "x"
@@ -154,18 +148,12 @@ let le_n = function () -> (coq_base_constant "le_n")
 let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
 let coq_O = function () -> (coq_base_constant "O")
 let coq_S = function () -> (coq_base_constant "S")
-let gt_antirefl = function () -> (coq_constant "gt_irrefl")
 let lt_n_O = function () -> (coq_base_constant "lt_n_O")
-let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn")
-let f_equal = function () -> (coq_constant "f_equal")
-let well_founded_induction = function () -> (coq_constant "well_founded_induction")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
 let max_constr = function () -> (constr_of_global (delayed_force max_ref))
 let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
 
 let f_S t = mkApp(delayed_force coq_S, [|t|]);;
-let make_refl_eq constructor type_of_t t  =
-  mkApp(constructor,[|type_of_t;t|])
 
 let rec n_x_id ids n =
   if n = 0 then []
@@ -960,10 +948,6 @@ let equation_others _ expr_info continuation_tac infos =
       (intros_values_eq expr_info [])
   else continuation_tac infos
 
-let equation_letin (na,b,t,e) expr_info continuation_tac info = 
-  let new_e = subst1 info.info e in 
-  continuation_tac {info with info = new_e;} 
-
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
     then intros_values_eq expr_info []