removes several warnings in contrib/interface

Modifies the behavior of Recursive definition to produce goals instead of
established theorems


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

8 files changed, 49 insertions, 44 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index f7f6674e87..0fcb0ec7b2 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -175,7 +175,7 @@ and e_my_find_search db_list local_db hdc concl =
       list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
   in 
   let tac_of_hint = 
-    fun ({pri=b; pat = p; code=t} as patac) -> 
+    fun ({pri=b; pat = p; code=t} as _patac) -> 
       (b, 
        let tac =
 	 match t with
@@ -357,7 +357,7 @@ let full_eauto debug n gl =
   let dbnames = stringmap_dom !searchtable in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-  let local_db = make_local_hint_db gl in
+  let _local_db = make_local_hint_db gl in
   tclTRY (e_search_auto debug n db_list) gl
 
 let my_full_eauto n gl = full_eauto false (n,0) gl
@@ -393,7 +393,7 @@ and my_find_search db_list local_db hdc concl =
       	(local_db::db_list)
   in
   List.map 
-    (fun ({pri=b; pat=p; code=t} as patac) -> 
+    (fun ({pri=b; pat=p; code=t} as _patac) -> 
        (b,
 	match t with
 	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
@@ -564,7 +564,7 @@ let blast gls =
       open_subgoals = 1;
       goal = g;
       ref = None } in
-     try (let (sgl,v) as res = !blast_tactic gls in
+     try (let (sgl,v) as _res = !blast_tactic gls in
 	  let {it=lg} = sgl in
           if lg = [] 
           then (let pf = v (List.map leaf (sig_it sgl)) in
@@ -586,7 +586,7 @@ let blast gls =
 ;;
 
 let blast_tac display_function = function 
-          | (n::_) as l -> 
+          | (n::_) as _l -> 
                  (function g ->
                     let exp_ast = (blast g) in
                      (display_function exp_ast;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 81e175232f..cb43a45ed9 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -342,12 +342,13 @@ let debug_tac2_pcoq tac =
 	let the_ast = ref tac in
 	let the_path = ref ([] : int list) in
 	try
-	  let result = report_error tac the_goal the_ast the_path [] g in
+	  let _result = report_error tac the_goal the_ast the_path [] g in
 	  (errorlabstrm "DEBUG TACTIC"
 	     (str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++
 	      fnl () ++ str "the tactic is" ++ fnl () ++
-	      Pptactic.pr_glob_tactic (Global.env()) tac);
-	   result)
+	      Pptactic.pr_glob_tactic (Global.env()) tac) (*
+Caution, this is in the middle of what looks like dead code. ;
+	   result *))
 	with
 	  e ->
 	    match !the_goal with
@@ -553,7 +554,7 @@ let pcoq_search s l =
 
 (* Check sequentially whether the pattern is one of the premises *)
 let rec hyp_pattern_filter pat name a c =
-  let c1 = strip_outer_cast c in
+  let _c1 = strip_outer_cast c in
     match kind_of_term c with
       | Prod(_, hyp, c2) -> 
 	  (try
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 97f2602d8b..50c8a0fa1a 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -220,7 +220,7 @@ let name_to_ast ref =
 		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
-	      let sp = Nametab.locate_syntactic_definition qid in
+	      let _sp = Nametab.locate_syntactic_definition qid in
 		errorlabstrm "print"
       		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index f8328f21d2..bc789fd0dc 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -203,7 +203,7 @@ let (imply_elim1: pbp_rule) = function
   Some h, Prod(Anonymous, prem, body), 1::path, f ->
   let clear_names' = if clear_flag then h::clear_names else clear_names in
   let h' = next_global_ident hyp_radix avoid in
-  let str_h' = (string_of_id h') in
+  let _str_h' = (string_of_id h') in
   Some(PbpThens
 	  ([PbpLApply h],
 	   [chain_tactics [make_named_intro h'] (make_clears (h::clear_names));
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 3ada7cb6db..b7da5c1b76 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -197,7 +197,7 @@ let fill_unproved nt l =
 let new_sign osign sign =
     let res=ref [] in
     List.iter (fun (id,c,ty) ->
-		   try (let  (_,_,ty1)= (lookup_named id osign) in
+		   try (let  (_,_,_ty1)= (lookup_named id osign) in
 			())
 		   with Not_found -> res:=(id,c,ty)::(!res))
               sign;
@@ -756,7 +756,7 @@ let rec group_lhyp lh =
 let natural_ghyp (sort,ln,lt) intro =
   let t=List.hd lt in
   let nh=List.length ln in
-  let ns=List.hd ln in
+  let _ns=List.hd ln in
   match sort with
     Nprop -> soit_A_une_proposition nh ln t
   | Ntype -> soit_X_un_element_de_T nh ln t
@@ -1206,7 +1206,7 @@ let rec natural_ntree ig ntree =
 	  | TacExact c -> natural_exact ig lh g gs c ltree
 	  | TacCut c -> natural_cut ig lh g gs c ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
-	      let c = out_gen wit_constr a in
+	      let _c = out_gen wit_constr a in
 	      natural_cutintro ig lh g gs a ltree
 	  | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
 	  | TacExtend (_,"CaseIntro",[a]) ->
@@ -1430,7 +1430,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
 	 if with_intros
          then (arity_of_constr_of_mind env indf 1)
 	 else 0 in
-       let ici= 1 in
+       let _ici= 1 in
        sph[ (natural_ntree  
                {ihsg=
                  (match (nsort targ1) with
@@ -1459,7 +1459,7 @@ and prod_list_var t =
 and  hd_is_mind t ti =
     try (let env = Global.env() in
          let IndType (indf,targ) = find_rectype env Evd.empty t in
-	 let ncti= Array.length(get_constructors env indf) in
+	 let _ncti= Array.length(get_constructors env indf) in
 	 let (ind,_) = dest_ind_family indf in
          let (mib,mip) = lookup_mind_specif env ind in
 	 (string_of_id mip.mind_typename) = ti)
@@ -1468,7 +1468,7 @@ and mind_ind_info_hyp_constr indf c =
   let env = Global.env() in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
-  let p = mib.mind_nparams in
+  let _p = mib.mind_nparams in
   let a = arity_of_constr_of_mind env indf c in
   let lp=ref (get_constructors env indf).(c).cs_args in
   let lr=ref [] in
@@ -1498,8 +1498,8 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
  let ncti= Array.length(get_constructors env indf) in
  let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
- let ti =(string_of_id mip.mind_typename) in
- let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
+ let _ti =(string_of_id mip.mind_typename) in
+ let _type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
   spv
          [  (natural_lhyp lh ig.ihsg);
              (show_goal2 lh ig g gs "");
@@ -1542,11 +1542,11 @@ and natural_induction ig lh g gs ge arg2 ltree with_intros=
  let arg1= mkVar arg2 in
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors env indf) in
+ let _ncti= Array.length(get_constructors env indf) in
  let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
- let ti =(string_of_id mip.mind_typename) in
- let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
+ let _ti =(string_of_id mip.mind_typename) in
+ let _type_arg= targ1(*List.nth targ (mis_index dmi)*) in
 
  let lh1= hyps (List.hd ltree) in (* la liste des hyp jusqu'a n *)
  (* on les enleve des hypotheses des sous-buts *)
@@ -1631,8 +1631,8 @@ and natural_reduce ig lh g gs ge mode la ltree =
 and natural_split ig lh g gs ge la ltree =
   match la with
     [arg] -> 
-      let env= (gLOB ge) in
-      let arg1= (*dbize env*) arg in
+      let _env= (gLOB ge) in
+      let arg1= (*dbize _env*) arg in
       spv
       	[ (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
@@ -1652,9 +1652,9 @@ and natural_split ig lh g gs ge la ltree =
 and natural_generalize ig lh g gs ge la ltree =
   match la with
     [arg] ->
-      let env= (gLOB ge) in
+      let _env= (gLOB ge) in
       let arg1= (*dbize env*) arg in
-      let type_arg=type_of (Global.env()) Evd.empty arg in
+      let _type_arg=type_of (Global.env()) Evd.empty arg in
 (*      let type_arg=type_of_ast ge arg in*)
       spv
       	[ (natural_lhyp lh ig.ihsg);
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index 07ac73b6aa..dd7f455d79 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -135,7 +135,7 @@ let rec sp_print x =
 		   CT_text_path (CT_signed_int_list p);
 		   CT_coerce_ID_to_TEXT (CT_ident "goal");
 		   g] ->
-      let p=(List.map (fun y -> match y with
+      let _p=(List.map (fun y -> match y with
 	                 (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
@@ -148,7 +148,7 @@ let rec sp_print x =
 	      CT_text_path (CT_signed_int_list p);
 	      CT_coerce_ID_to_TEXT (CT_ident hyp);
               g]  ->
-      let p=(List.map (fun y -> match y with
+      let _p=(List.map (fun y -> match y with
 	                  (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
@@ -158,7 +158,7 @@ let rec sp_print x =
 	      CT_text_path (CT_signed_int_list p);
 	      CT_coerce_ID_to_TEXT (CT_ident hyp);
               g]  ->
-      let p=(List.map (fun y -> match y with
+      let _p=(List.map (fun y -> match y with
                          (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 9f25ce38a4..65d8331b2d 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -6,6 +6,6 @@ open Term;;
 
 val translate_goal : goal -> ct_RULE;;
 (* The boolean argument indicates whether names from the environment should *)
-(*  be avoided (same interpretation as for pr_lconstr_env and ast_of_constr)    *)
+(*  be avoided (same interpretation as for prterm_env and ast_of_constr)    *)
 val translate_constr : bool -> env -> constr -> ct_FORMULA;;
 val translate_path : int list -> ct_SIGNED_INT_LIST;;
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index e67dc1fa02..12dc575881 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -176,7 +176,7 @@ let coq_sig = lazy(coq_constant "sig")
 let coq_O = lazy(coq_constant "O")
 let coq_S = lazy(coq_constant "S")
 
-let gt_antirefl = lazy(coq_constant "gt_antirefl")
+let gt_antirefl = lazy(coq_constant "gt_irrefl")
 let lt_n_O = lazy(coq_constant "lt_n_O")
 let lt_n_Sn = lazy(coq_constant "lt_n_Sn")
 
@@ -376,8 +376,8 @@ let rec introduce_all_values func context_fn
 	    (tclTHENS
 	   (simplest_elim (mkApp(mkVar hrec, [|arg|])))
 	   [tclTHENLIST [intros_using [rec_res; hspec];
-			 tac];
-	    tclTHENLIST
+			 tac]; tclIDTAC
+(*	    tclTHENLIST
 	      [list_rewrite true eqs;
 	       List.fold_right
                  (fun proof tac ->
@@ -390,7 +390,8 @@ let rec introduce_all_values func context_fn
                  proofs
                  (fun g ->
                    (msgnl (str "complete proof failed for decreasing call");
-                    msgnl (Printer.pr_goal (sig_it g)); tclFAIL 0 "" g))]]) g)
+                    msgnl (Printer.pr_goal (sig_it g)); tclFAIL 0 "" g))]*)
+]) g)
        
 	   
 let rec_leaf hrec proofs (func:global_reference) eqs expr =
@@ -501,24 +502,26 @@ let whole_start func input_type relation wf_thm proofs =
 	 | Anonymous -> assert false in
      let tac, hrec = (start n_id input_type relation wf_thm g) in
        tclTHEN tac
-           (proveterminate hrec proofs (mkVar f_id) func []
-	     (instantiate_lambda func_body [mkVar f_id;mkVar n_id])) g in
+           (* (observe_tac "debug" *)
+             (fun g ->  try 
+               (proveterminate hrec proofs (mkVar f_id) func []
+	        (instantiate_lambda func_body [mkVar f_id;mkVar n_id])) g with
+               e -> (msgnl (str "debug : found an exception");raise e))(* ) *)g in
 (*     let _ = msgnl(str "exiting whole start") in *)
        v);;
 
 let com_terminate fonctional_ref input_type relation_ast wf_thm_ast
-    thm_name proofs =
+    thm_name proofs hook =
   let (evmap, env) = Command.get_current_context() in
   let (relation:constr)= interp_constr evmap env relation_ast in
   let (wf_thm:constr) = interp_constr evmap env wf_thm_ast in
   let (proofs_constr:constr list) =
       List.map (fun x -> interp_constr evmap env x) proofs in
     (start_proof thm_name
-       (IsGlobal (Proof Lemma)) (Environ.named_context_val env) (hyp_terminates fonctional_ref)
-       (fun _ _ -> ());
+       (IsGlobal (Proof Lemma)) (Environ.named_context_val env)
+         (hyp_terminates fonctional_ref) hook;
      by (whole_start fonctional_ref
-	   input_type relation wf_thm proofs_constr);
-     Command.save_named true);;
+	   input_type relation wf_thm proofs_constr));;
 
 let ind_of_ref = function 
   | IndRef (ind,i) -> (ind,i)
@@ -740,11 +743,12 @@ let recursive_definition f type_of_f r wf proofs eq =
   let functional_id =  add_suffix f "_F" in
   let term_id = add_suffix f "_terminate" in
   let functional_ref = declare_fun functional_id IsDefinition res in
-  let _ = com_terminate functional_ref input_type r wf term_id proofs in
-  let term_ref = Nametab.locate (make_short_qualid term_id) in
+  let hook _ _ =   let term_ref = Nametab.locate (make_short_qualid term_id) in
   let f_ref = declare_f f (IsProof Lemma) input_type term_ref in
 (*  let _ = message "start second proof" in *)
-    com_eqn equation_id functional_ref f_ref term_ref eq;;
+    com_eqn equation_id functional_ref f_ref term_ref eq in
+  com_terminate functional_ref input_type r wf term_id proofs hook
+;;
 
 VERNAC COMMAND EXTEND RecursiveDefinition
   [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)