very minor bug correction and cleanning

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

2 files changed, 2 insertions, 242 deletions

diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 3969623006..c2c23f418b 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -30,7 +30,7 @@ let invalid_argument s = raise (Invalid_argument s)
 
 
 
-let fresh_id avoid s = Nameops.next_ident_away (id_of_string s) avoid
+let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
index a33f0f6c54..eea603e186 100644
--- a/contrib/funind/new_arg_principle.ml
+++ b/contrib/funind/new_arg_principle.ml
@@ -34,6 +34,7 @@ let tclTRYD tac =
   then tclTRY tac
   else tac
 
+
 type rewrite_dir =
   | LR
   | RL
@@ -951,244 +952,3 @@ let generate_new_structural_principle
 
 
 
-
-(*************************************************)
-let next_ident_away = Nameops.next_ident_away
-
-
-(* let base_leaf_eq eqs f_id g = *)
-(*   let ids = ids_of_named_context (pf_hyps g) in *)
-(*   let k = next_ident_away (id_of_string "k") ids in *)
-(*   let p = next_ident_away (id_of_string "p") (k::ids) in *)
-(*   let v = next_ident_away (id_of_string "v") (p::k::ids) in *)
-(*   let heq = next_ident_away (id_of_string "heq") (v::p::k::ids) in *)
-(*   let heq1 = next_ident_away (id_of_string "heq") (heq::v::p::k::ids) in *)
-(*   let hex = next_ident_away (id_of_string "hex") (heq1::heq::v::p::k::ids) in *)
-(*     tclTHENLIST [ *)
-(*       intros_using [v; hex]; *)
-(*       simplest_elim (mkVar hex); *)
-(*       intros_using [p;heq1]; *)
-(*       tclTRY *)
-(* 	(Equality.rewriteRL *)
-(* 	   (mkApp(mkVar heq1, *)
-(* 		  [|mkApp (Lazy.force Recdef.coq_S, [|mkVar p|]); *)
-(* 		    mkApp(Lazy.force Recdef.lt_n_Sn, [|mkVar p|]); f_id|]))); *)
-(*       Recdef.list_rewrite true eqs; *)
-(*       apply (Lazy.force refl_equal)] g;; *)
-
-(* let f_S t = mkApp(Lazy.force Recdef.coq_S, [|t|]);; *)
-
-(* let rec introduce_all_values_eq cont_tac f p heq1 pmax *)
-(*     bounds le_proofs eqs ids = *)
-(*   function *)
-(*       [] -> *)
-(* 	tclTHENLIST *)
-(* 	  [tclTHENS *)
-(* 	     (Equality.general_rewrite_bindings false *)
-(* 		(mkVar heq1, *)
-(* 		 Rawterm.ExplicitBindings[dummy_loc,Rawterm.NamedHyp (id_of_string "k"), *)
-(* 				  f_S(f_S(mkVar pmax)); *)
-(* 				  dummy_loc,Rawterm.NamedHyp (id_of_string "def"), *)
-(* 				  f])) *)
-(*    [tclTHENLIST *)
-(*    [Recdef.list_rewrite true eqs; cont_tac pmax le_proofs]; *)
-(*    tclTHENLIST[apply (Lazy.force Recdef.le_lt_SS); *)
-(* 			Recdef.compute_le_proofs le_proofs]]] *)
-(*     | arg::args -> *)
-(* 	let v' = next_ident_away (id_of_string "v") ids in *)
-(*         let ids = v'::ids in *)
-(* 	let hex' = next_ident_away Recdef.hex_id ids in *)
-(*         let ids = hex'::ids in *)
-(* 	let p' = next_ident_away Recdef.p_id ids in *)
-(*         let ids = p'::ids in *)
-(* 	let new_pmax = next_ident_away Recdef.pmax_id ids in *)
-(*         let ids = pmax::ids in *)
-(* 	let hle1 = next_ident_away Recdef.hle_id ids in *)
-(*         let ids = hle1::ids in *)
-(* 	let hle2 = next_ident_away Recdef.hle_id ids in *)
-(*         let ids = hle2::ids in *)
-(* 	let heq = next_ident_away Recdef.heq_id ids in *)
-(*         let ids = heq::ids in *)
-(* 	let heq2 = *)
-(* 	  next_ident_away Recdef.heq_id ids in *)
-(*         let ids = heq2::ids in *)
-(* 	tclTHENLIST *)
-(* 	  [Recdef.mkCaseEq(mkApp(termine, Array.of_list arg)); *)
-(* 	   intros_using [v'; hex']; *)
-(* 	   simplest_elim(mkVar hex'); *)
-(* 	   intros_using [p']; *)
-(* 	   simplest_elim(mkApp(Lazy.force max_constr, [|mkVar pmax; *)
-(* 							mkVar p'|])); *)
-(* 	   intros_using [new_pmax;hle1;hle2]; *)
-(*            introduce_all_values_eq *)
-(*               (fun pmax' le_proofs'-> *)
-(* 		tclTHENLIST *)
-(* 		  [cont_tac pmax' le_proofs'; *)
-(* 		   intros_using [heq;heq2]; *)
-(* 		   rewriteLR (mkVar heq2); *)
-(* 		   tclTHENS *)
-(* 		     (general_rewrite_bindings false *)
-(* 			(mkVar heq, *)
-(* 			 ExplicitBindings *)
-(* 			   [dummy_loc, NamedHyp k_id, *)
-(* 			    f_S(mkVar pmax'); *)
-(* 			    dummy_loc, NamedHyp def_id, f])) *)
-(* 		     [tclIDTAC; *)
-(* 		      tclTHENLIST *)
-(* 			[apply (Lazy.force le_lt_n_Sm); *)
-(* 			 compute_le_proofs le_proofs']]]) *)
-(* 	     functional termine f p heq1 new_pmax *)
-(* 	     (p'::bounds)((mkVar pmax)::le_proofs) eqs *)
-(*              (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args] *)
-  
-
-(* let rec_leaf_eq  f ids eqs expr fn args = *)
-(*   let p = next_ident_away (id_of_string "id") ids in *)
-(*   let ids = p::ids in *)
-(*   let v = next_ident_away (id_of_string "v") ids in *)
-(*   let ids = v::ids in *)
-(*   let hex = next_ident_away (id_of_string "hex") ids in *)
-(*   let ids = hex::ids in *)
-(*   let heq1 = next_ident_away (id_of_string "heq") ids in *)
-(*   let ids = heq1::ids in *)
-(*   let hle1 = next_ident_away (id_of_string "hle") ids in *)
-(*   let ids = hle1::ids in *)
-(*     tclTHENLIST *)
-(*       [intros_using [v;hex]; *)
-(*        simplest_elim (mkVar hex); *)
-(*        intros_using [p;heq1]; *)
-(*        generalize [mkApp(Lazy.force Recdef.le_n,[|mkVar p|])]; *)
-(*        intros_using [hle1]; *)
-(* (\*        introduce_all_values_eq (fun _ _ -> tclIDTAC) *\) *)
-(* (\* 	  f p heq1 p [] [] eqs ids args; *\) *)
-(* (\*        apply (Lazy.force refl_equal) *\)] *)
-
-open Libnames
-let rec nthtl = function
-    l, 0 -> l  | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];;
-let  mkCaseEq a =
-     (fun g ->
-(* commentaire de Yves: on pourra avoir des problemes si
-   a n'est pas bien type dans l'environnement du but *)
-       let type_of_a = pf_type_of g a in
-       (tclTHEN (generalize [mkApp(Lazy.force refl_equal, [| type_of_a; a|])])
-	  (tclTHEN 
-	     (fun g2 ->
-	       change_in_concl None 
-		 (Tacred.pattern_occs [([2], a)] (pf_env g2) Evd.empty (pf_concl g2))
-		 g2)
-	     (simplest_case a))) g);;
-
-let rec (find_call_occs:
-	   constr -> constr -> (constr list ->constr)*(constr  list list)) =
- fun f expr ->
-  match (kind_of_term expr) with
-    App (g, args) when g = f -> 
-      (* For now we suppose that the function takes only one argument. *)
-      (fun l -> List.hd l), [Array.to_list args]
-  | App (g, args) ->
-     let (largs: constr list) = Array.to_list args in
-     let rec find_aux = function
-	 []    -> (fun x -> []), []
-       | a::tl ->
-         (match find_aux tl with
-          (cf, ((arg1::args) as opt_args)) -> 
-           (match find_call_occs f a with
-             cf2, (_ :: _ as other_args) ->
-	       let len1 = List.length other_args in
-                 (fun l ->
-                   cf2 l::(cf (nthtl(l,len1)))), other_args@opt_args
-           | _, [] -> (fun x -> a::cf x), opt_args)
-	 | _, [] ->
-	   (match find_call_occs f a with
-	     cf, (arg1::args) -> (fun l -> cf l::tl), (arg1::args)
-	   | _, [] -> (fun x -> a::tl), [])) in
-     begin
-       match (find_aux largs) with
-	   cf, [] -> (fun l -> mkApp(g, args)), []
-	 | cf, args ->
-	     (fun l -> mkApp (g, Array.of_list (cf l))), args
-     end
-  | Rel(_) -> error "find_call_occs : Rel"
-  | Var(id) -> (fun l -> expr), []
-  | Meta(_) -> error "find_call_occs : Meta"
-  | Evar(_) -> error "find_call_occs : Evar"
-  | Sort(_)  -> error "find_call_occs : Sort"
-  | Cast(_,_,_) -> error "find_call_occs : cast"
-  | Prod(_,_,_) -> error "find_call_occs : Prod"
-  | Lambda(_,_,_) -> error "find_call_occs : Lambda"
-  | LetIn(_,_,_,_) -> error "find_call_occs : let in"
-  | Const(_) -> (fun l -> expr), []
-  | Ind(_) -> (fun l -> expr), []
-  | Construct (_, _) -> (fun l -> expr), []
-  | Case(i,t,a,r) ->
-      (match find_call_occs f a with
-	cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
-      | _ -> (fun l -> mkCase(i, t, a, r)),[])
-  | Fix(_) -> error "find_call_occs : Fix"
-  | CoFix(_) -> error "find_call_occs : CoFix";;
-
-let rec  mk_intros_and_continue (extra_eqn:bool)
-    cont_function (eqs:constr list) (expr:constr) g =
-  let ids=ids_of_named_context (pf_hyps g) in
-  match kind_of_term expr with
-      Lambda (n, _, b) -> 
-     	let n1 = (match n with
-      	              Name x -> x
-                    | Anonymous -> (id_of_string "anonymous") ) in
-     	let new_n = next_ident_away n1 ids in
-	  tclTHEN (intro_using new_n)
-	    (mk_intros_and_continue extra_eqn cont_function eqs 
-	       (subst1 (mkVar new_n) b)) g
-    | _ -> 
- 	if extra_eqn then
-	  let teq = next_ident_away (id_of_string "teq") ids in
-	    tclTHENSEQ
-	      [(intro_using teq); Equality.rewriteLR (mkVar teq); 
-	      (cont_function (mkVar teq::eqs) expr)] g
-	else
-	  cont_function eqs expr g;;
-
-let base_leaf_eq eqs f = tclTRY reflexivity 
-
-let rec_leaf_eq f ids eqs expr fn args = tclTRY reflexivity
-
-
-let rec prove_eq (f:constr)
-    (eqs:constr list)
-    (expr:constr) =
-  tclTRY
-    (match kind_of_term expr with
-	 Case(_,t,a,l) ->
-	   (match find_call_occs f a with
-		_,[] -> 
-		  tclTHENS(mkCaseEq a)(* (simplest_case a) *)
-	  	    (List.map
-		       (mk_intros_and_continue true
-			  (prove_eq  f) eqs)
-		       (Array.to_list l))
-	      | _,_::_ ->
-               	  (match find_call_occs f expr with
-		       _,[] -> base_leaf_eq eqs f
-		     | fn,args ->
-			 fun g ->
-			   let ids = pf_ids_of_hyps g in
-			   rec_leaf_eq f ids eqs expr fn args g
-		  )
-	   )
-       | _ -> 
-	   (match find_call_occs f expr with
-		_,[] -> base_leaf_eq eqs f
-	      | fn,args ->
-		  fun g ->
-		    let ids = pf_ids_of_hyps g in
-		    rec_leaf_eq f ids eqs expr fn args g
-	   )
-    )
-    
-
-let prove_eq f expr = 
-  let fname = destConst f in 
-  tclTHEN
-    (Tactics.unfold_constr (ConstRef fname))
-    (mk_intros_and_continue false (prove_eq f)  [] expr)