+ ameliorating the tactic "functional induction"

+ bug correction in proof of structural principles
+ up do to date test-suite/success/Funind.v


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

8 files changed, 533 insertions, 419 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 119b155d0..f0e986fb9 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -810,14 +810,16 @@ type static_fix_info =
       idx : int;
       name : identifier;
       types : types;
-      nb_realargs : int
+      offset : int;
+      nb_realargs : int;
+      body_with_param : constr 
     }
 
 
 
 let prove_rec_hyp_for_struct fix_info = 
       (fun  eq_hyps -> tclTHEN 
-	(rewrite_until_var (fix_info.idx - 1) eq_hyps)
+	(rewrite_until_var (fix_info.idx) eq_hyps)
 	(fun g -> 
 	   let _,pte_args = destApp (pf_concl g) in 
 	   let rec_hyp_proof = 
@@ -849,282 +851,360 @@ let generalize_non_dep hyp g =
       else (hyp::clear,keep))
       ~init:([],[]) (pf_env g)
   in
-  observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert);
+(*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN 
     (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert)))
     (observe_tac "thin" (thin to_revert))
     g
   
-let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic =
-   fun goal ->
-(*      observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++  *)
-(* 		pr_lconstr (mkConst fnames.(fun_num))); *)
-     let princ_type = pf_concl goal in
-     let princ_info = compute_elim_sig princ_type in
-     let get_body const =
-       match (Global.lookup_constant const ).const_body with
-	 | Some b ->
+let id_of_decl (na,_,_) =  (Nameops.out_name na)
+let var_of_decl decl = mkVar (id_of_decl decl)
+let revert idl = 
+  tclTHEN 
+    (generalize (List.map mkVar idl)) 
+    (thin idl)
+
+
+let do_replace params rec_arg_num rev_args_id fun_to_replace body = 
+  fun g ->
+    let nb_intro_to_do = nb_prod (pf_concl g) in
+    tclTHEN
+      (tclDO nb_intro_to_do intro)
+      (
+	fun g' -> 
+	  let just_introduced = nLastHyps nb_intro_to_do g' in 
+	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in 
+	  let old_rev_args_id = rev_args_id in 
+	  let rev_args_id = just_introduced_id@rev_args_id in 
+	  let to_replace = 
+	    Reductionops.nf_betaiota (substl (List.map mkVar rev_args_id) fun_to_replace )
+	  and by = 
+	    Reductionops.nf_betaiota (applist(body,List.rev_map mkVar rev_args_id)) 
+	  in 
+(* 	  observe (str "to_replace := " ++ pr_lconstr_env (pf_env g') to_replace); *)
+(* 	  observe (str "by := " ++ pr_lconstr_env (pf_env g') by); *)
+	  let prove_replacement = 
+	    let rec_id = List.nth (List.rev old_rev_args_id) (rec_arg_num) in 
+	    observe_tac "prove_replacement"
+	      (tclTHENSEQ
+		 [ 
+		   revert just_introduced_id;
+		   keep ((List.map id_of_decl params)@ old_rev_args_id);
+		   generalize_non_dep rec_id;
+		   observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings)); 
+		   intros_reflexivity
+		 ]
+	      )
+	  in
+	  tclTHENS
+	    (observe_tac "replacement" (Equality.replace to_replace by))
+	    [ revert just_introduced_id;
+	     tclSOLVE [prove_replacement]]
+	    g'
+      )
+      g
+    
+
+
+let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
+  fun g -> 
+    let princ_type = pf_concl g in 
+    let princ_info = compute_elim_sig princ_type in 
+    let fresh_id = 
+      let avoid = ref (pf_ids_of_hyps g) in 
+      (fun na -> 
+	 let new_id = 
+	   match na with 
+	       Name id -> fresh_id !avoid (string_of_id id) 
+	     | Anonymous -> fresh_id !avoid "H"
+	 in
+	 avoid := new_id :: !avoid; 
+	 (Name new_id)
+      )
+    in
+    let fresh_decl = 
+      (fun (na,b,t) -> 
+	 (fresh_id na,b,t)
+      )
+    in
+    let princ_info : elim_scheme = 
+      { princ_info with 
+	  params = List.map fresh_decl princ_info.params;
+	  predicates = List.map fresh_decl princ_info.predicates; 
+	  branches = List.map fresh_decl princ_info.branches; 
+	  args = List.map fresh_decl princ_info.args
+      }
+    in
+    let get_body const =
+      match (Global.lookup_constant const ).const_body with
+	| Some b ->
 	     let body = force b in
 	     Tacred.cbv_norm_flags
 	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
 	       body
-	 | None -> error ( "Cannot define a principle over an axiom ")
-     in
-     let fbody = get_body fnames.(fun_num) in
-     let params : identifier list ref = ref [] in
-     let predicates : identifier list ref = ref [] in
-     let args : identifier list ref = ref [] in
-     let branches : identifier list ref = ref [] in
-     let pte_to_fix = ref Idmap.empty in
-     let fbody_with_params = ref None in
-     let intro_with_remembrance  ref number : tactic =
-       tclTHEN
-	 ( tclDO number intro )
-	 (fun g ->
-	    let last_n = list_chop number (pf_hyps g) in
-	    ref :=  List.map (fun (id,_,_) -> id) (fst last_n)@ !ref;
-	    tclIDTAC g
-	 )
-     in
-     let rec partial_combine body params =
-       match kind_of_term body,params with
-	 | Lambda (x,t,b),param::params ->
-	     partial_combine (subst1 param b) params
-	 | Fix(infos),_ ->
-	     body,params, Some (infos)
-	 | _ -> body,params,None
-     in
-     let build_pte_to_fix (offset:int) params predicates
-	 ((idxs,fix_num),(na,typearray,ca))  (avoid,_) =
-(*        let true_params,_ =  list_chop offset params  in  *)
-       let true_params = List.rev params in
-       let avoid = ref avoid in
-       let res = list_fold_left_i
-	 (fun i acc pte_id  ->
-	    let this_fix_id = fresh_id !avoid "fix___" in
-	    avoid := this_fix_id::!avoid;
-(* 	    let this_body = substl (List.rev fnames_as_constr) ca.(i) in  *)
-	    let realargs,_ = decompose_lam ca.(i) in 
-	    let n_realargs = List.length realargs - List.length params in 
-(* 	    observe (str "n_realargs := " ++ str (string_of_int n_realargs)); *)
-(* 	    observe (str "n_fix := " ++ str (string_of_int(Array.length ca))); *)
-(* 	    observe (str "body := " ++ pr_lconstr ca.(i)); *)
-
-	    let new_type = prod_applist typearray.(i) true_params in
-	    let new_type_args,_ = decompose_prod new_type in
-	    let nargs = List.length new_type_args in
-	    let pte_args =
-	      (* 	      let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in  *)
-	      let f = applist((* all_funs *)mkConst fnames.(i),true_params) in
-	      let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in
-	      (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f]
+	| None -> error ( "Cannot define a principle over an axiom ")
+    in
+    let fbody = get_body fnames.(fun_num) in
+    let f_ctxt,f_body = decompose_lam fbody in 
+    let f_ctxt_length = List.length f_ctxt in 
+    let diff_params = princ_info.nparams - f_ctxt_length in 
+    let full_params,princ_params,fbody_with_full_params = 
+      if diff_params > 0
+      then 
+	let princ_params,full_params = 
+	  list_chop  diff_params princ_info.params 
+	in 
+	(full_params, (* real params *)
+	 princ_params, (* the params of the principle which are not params of the function *)
+	 substl (* function instanciated with real params *)
+	   (List.map var_of_decl full_params)
+	   f_body
+	)
+      else
+	let f_ctxt_other,f_ctxt_params = 
+	  list_chop (- diff_params) f_ctxt in 
+	let f_body = compose_lam f_ctxt_other f_body in 
+	(princ_info.params, (* real params *)
+	 [],(* all params are full params *)
+	 substl (* function instanciated with real params *)
+	   (List.map var_of_decl princ_info.params)
+	   f_body
+	)
+    in
+(*     observe (str "full_params := " ++  *)
+(* 	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
+(* 	       full_params *)
+(* 	    );  *)
+(*     observe (str "princ_params := " ++  *)
+(* 	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
+(* 	       princ_params *)
+(* 	    );  *)
+(*     observe (str "fbody_with_full_params := " ++  *)
+(* 	       pr_lconstr fbody_with_full_params *)
+(* 	    );  *)
+    let all_funs_with_full_params = 
+      Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
+    in
+    let fix_offset = List.length princ_params in 
+    let ptes_to_fix,infos = 
+      match kind_of_term fbody_with_full_params with 
+	| Fix((idxs,i),(names,typess,bodies)) -> 
+	    let bodies_with_all_params = 
+	      Array.map 
+		(fun body -> 
+		   Reductionops.nf_betaiota 
+		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
+			      List.rev_map var_of_decl princ_params))
+		)
+		bodies
 	    in
-	    let app_pte = applist(mkVar pte_id,pte_args) in
-	    let new_type = compose_prod new_type_args app_pte in
-	    
-	    let fix_info = 
-	      {
-		idx = idxs.(i) - offset + 1;
-		name = this_fix_id; 
-		types = new_type;
-		nb_realargs = n_realargs
-	      }
+	    let info_array = 
+	      Array.mapi 
+		(fun i types -> 
+		   let types = prod_applist types (List.rev_map var_of_decl princ_params) in
+		   { idx = idxs.(i)  - fix_offset;
+		     name = Nameops.out_name (fresh_id names.(i));
+		     types = types; 
+		     offset = fix_offset;
+		     nb_realargs = 
+		       List.length 
+			 (fst (decompose_lam bodies.(i))) - fix_offset;
+		     body_with_param = bodies_with_all_params.(i)
+		   }
+		)
+		typess
 	    in
-	    pte_to_fix := Idmap.add  pte_id fix_info !pte_to_fix;
-	    fix_info::acc
-	 )
-	 0
-	 []
-	 predicates
-       in
-       !avoid,List.rev res
-     in
-     let mk_fixes : tactic =
-       fun g ->
-	 let body_p,params',fix_infos =
-	   partial_combine fbody (List.rev_map mkVar  !params)
-	 in
-	 fbody_with_params := Some body_p;
-	 let offset  = List.length params' in
-	 let not_real_param,true_params =
-	   list_chop
-	     ((List.length !params ) - offset)
-	     !params
-	 in
-	 params := true_params; args := not_real_param;
-(* 	 observe (str "mk_fixes : params are "++  *)
-(* 		    prlist_with_sep spc *)
-(* 		    (fun id -> pr_lconstr (mkVar id)) *)
-(* 		    !params *)
-(* 		 ); *)
-	 let new_avoid,infos =
-	   option_fold_right
-	     (build_pte_to_fix
-		offset
-		(List.map mkVar !params)
-		(List.rev !predicates)
-	     )
-	     fix_infos
-	     ((pf_ids_of_hyps g),[])
-	 in
-	 let pre_info,infos = list_chop fun_num infos in
-	 match pre_info,infos with
-	   | [],[] -> tclIDTAC g
-	   | _,this_fix_info::infos' ->
-	       let other_fix_info =
-		 List.map 
-		   (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types) 
-		   (pre_info@infos')
-	       in
-	       if other_fix_info = []
-		  then h_fix (Some this_fix_info.name) this_fix_info.idx g
-		  else h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info g
-	   | _,[] -> anomaly "Not a valid information"
-     in
-     let do_prove ptes_to_fixes args branches : tactic =
-       fun g ->
-	 let nb_intros_to_do = List.length (fst (Sign.decompose_prod_assum (pf_concl g))) in 
-(* 	 observe (str "nb_intros_to_do " ++ str (string_of_int nb_intros_to_do)); *)
-	 tclTHEN 
-	   (tclDO nb_intros_to_do intro)
-	   (fun g -> 
-	      match kind_of_term (pf_concl g) with
-		| App(pte,pte_args) when isVar pte ->
-		    begin
-		      let pte = destVar pte in
-		      try
-			if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec;
-			let nparams = List.length !params in
-			let args_as_constr = List.map mkVar args in
-			let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in 
-			let other_args_as_constr = List.map mkVar  other_args in 
-			let rec_num,new_body =
-			  let idx' = list_index pte (List.rev !predicates)  - 1 in
-			  let f = fnames.(idx') in
-			  let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly ""
-			  in
-			  let name_of_f = Name (id_of_label (con_label f)) in
-			  let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in
-			  let idx'' = list_index name_of_f (Array.to_list na) - 1 in
-			  let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in
-			  let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in
-			  rec_nums.(idx'') - nparams ,body
-			in
-			let applied_body_with_real_args =
-			  Reductionops.nf_betaiota
-			    (applist(new_body,List.rev args_as_constr))
-			in
-			let applied_body = 
-(* 			  Reductionops.nf_beta *)
-			  Reductionops.nf_betaiota 
-			    (applist(applied_body_with_real_args,List.rev other_args_as_constr))
-			in
-(* 			observe (str "applied_body_with_real_args := "++ pr_lconstr_env (pf_env g) applied_body_with_real_args); *)
-(* 			observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); *)
-			let do_prove branches applied_body =
-			  build_proof
-			       interactive_proof
-			       (Array.to_list fnames)
-			       (Idmap.map prove_rec_hyp ptes_to_fixes)
-			       branches
-			       applied_body
-			in
-			let replace_and_prove =
-			  tclTHENS
-			    (fun g -> (Equality.replace (array_last pte_args) applied_body) g)
-			    [
-			      tclTHENLIST 
-				[
-				  generalize other_args_as_constr;
-				  thin other_args;
-				  clean_goal_with_heq 
-				    (Idmap.map prove_rec_hyp ptes_to_fixes)
-				    do_prove 
-				    {
-				      nb_rec_hyps = List.length branches;
-				      rec_hyps = branches;
-				      info = applied_body_with_real_args;
-				      eq_hyps = [];
-				    } ];
-			      let id = 
-				try
-				  List.nth (List.rev args_as_constr) (rec_num) 
-				with _ -> anomaly ("Cannot find recursive argument of function ! ") 
-			      in
-			      (tclTHENSEQ
-				 [ 
-				   keep (!params@(List.map destVar args_as_constr));
-				   observe_tac "generalizing" (generalize_non_dep (destVar id));
-				   observe_tac "new_destruct" 
-				    (h_case (id,Rawterm.NoBindings));
-				  observe_tac "intros_reflexivity" intros_reflexivity
-				 ])
-			    ]
-			in
-			(observe_tac "doing replacement" ( replace_and_prove)) g
-		      with Not_Rec ->
-			let fname = destConst (fst (decompose_app (array_last pte_args))) in
-			tclTHEN
-		     (unfold_in_concl [([],Names.EvalConstRef fname)])
-			  (observe_tac "" 
-			     (fun g' ->
-				let body = array_last (snd (destApp (pf_concl g'))) in 
-				let dyn_infos = 
-				  { nb_rec_hyps = List.length branches;
-				    rec_hyps = branches;
-				    info = body;
-				    eq_hyps = []
-				  }
-				in
-				let do_prove = 
-				  build_proof
-				    interactive_proof
-				    (Array.to_list fnames)
-				    (Idmap.map prove_rec_hyp ptes_to_fixes)
-				in
-				clean_goal_with_heq (Idmap.map prove_rec_hyp ptes_to_fixes)
-				  do_prove dyn_infos g'
-			     )
-			  )
-			  g
-		    end
-		| _ -> assert false
-	   ) g
-     in
-     tclTHENSEQ
-       [
-	 (fun g -> observe_tac "introducing params" (intro_with_remembrance  params princ_info.nparams) g);
-	 (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates  princ_info.npredicates) g);
-	 (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g);
-	 (fun g -> observe_tac "declaring fix(es)" mk_fixes g);
-	 (fun g -> 
-	    let nb_real_args = 
-	      let pte_app = snd (Sign.decompose_prod_assum (pf_concl g)) in 
-	      let pte = fst (decompose_app pte_app) in
-	      try 
-		let fix_info = Idmap.find (destVar pte) !pte_to_fix in
-		fix_info.nb_realargs
-	      with Not_found -> (* Not a recursive function *) 
-		nb_lam (Util.out_some !fbody_with_params)
-(* 		nb_prod (pf_concl g) *)
+	    let pte_to_fix,rev_info = 
+	      list_fold_left_i 
+		(fun i (acc_map,acc_info) (pte,_,_) -> 
+		   let infos = info_array.(i) in 
+		   let type_args,_ = decompose_prod infos.types in 
+		   let nargs = List.length type_args in 
+		   let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in
+		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
+		   let app_f = mkApp(f,first_args) in
+		   let pte_args = (Array.to_list first_args)@[app_f] in 
+		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in 
+		   let body_with_param = 
+		     let body = get_body fnames.(i) in 
+		     let body_with_full_params = 
+		       Reductionops.nf_betaiota (
+			 applist(body,List.rev_map var_of_decl full_params))
+		     in
+		     match kind_of_term body_with_full_params with 
+		       | Fix((_,num),(_,_,bs)) -> 
+			       Reductionops.nf_betaiota
+				 (
+				   (applist
+				      (substl 
+					 (List.rev 
+					    (Array.to_list all_funs_with_full_params)) 
+					 bs.(num),
+				       List.rev_map var_of_decl princ_params))
+				 )
+			 | _ -> error "Not a mutual block"
+		   in
+		   let info = 
+		     {infos with 
+			types = compose_prod type_args app_pte;
+			 body_with_param = body_with_param
+		     }
+		   in 
+(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
+(* 			      str " to " ++ Ppconstr.pr_id info.name); *)
+		   (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   )
+		0 
+		(Idmap.empty,[]) 
+		(List.rev princ_info.predicates)
+	    in
+	    pte_to_fix,List.rev rev_info
+	| _ -> Idmap.empty,[]
+    in
+    let mk_fixes : tactic = 
+      let pre_info,infos = list_chop fun_num infos in 
+      match pre_info,infos with 
+	| [],[] -> tclIDTAC
+	| _, this_fix_info::others_infos -> 
+	    let other_fix_infos =
+	      List.map
+		(fun fi -> fi.name,fi.idx + 1 ,fi.types) 
+		(pre_info@others_infos)
 	    in 
-	    observe_tac "" (tclTHEN
-	      (tclDO nb_real_args (observe_tac "intro" intro)) 
-	      (fun g' -> 
-		 let realargs_ids = fst (list_chop ~msg:"args" nb_real_args (pf_ids_of_hyps g')) in 
-		 let do_prove_on_branches branches : tactic =
-		   observe_tac "proving" (do_prove !pte_to_fix ( realargs_ids) branches)
+	    if other_fix_infos = [] 
+	    then
+	      observe_tac ("h_fix") (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
+	    else
+	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+		other_fix_infos
+	| _ -> anomaly "Not a valid information"
+    in
+    let first_tac : tactic = (* every operations until fix creations *)
+      tclTHENSEQ 
+	[ observe_tac "introducing params" (intros_using (List.rev_map id_of_decl princ_info.params)); 
+	  observe_tac "introducing predictes" (intros_using (List.rev_map id_of_decl princ_info.predicates)); 
+	  observe_tac "introducing branches" (intros_using (List.rev_map id_of_decl princ_info.branches)); 
+	  observe_tac "building fixes" mk_fixes;
+	]
+    in
+    let intros_after_fixes : tactic = 
+      fun gl -> 
+	let ctxt,pte_app =  (Sign.decompose_prod_assum (pf_concl gl)) in
+	let pte,pte_args = (decompose_app pte_app) in
+	try
+	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in 
+	  let fix_info = Idmap.find  pte ptes_to_fix in
+	  let nb_args = fix_info.nb_realargs in 
+	  tclTHENSEQ
+	    [
+	      observe_tac ("introducing args") (tclDO nb_args intro);
+	      (fun g -> (* replacement of the function by its body *)
+		 let args = nLastHyps nb_args g in 
+		 let fix_body = fix_info.body_with_param in
+(* 		 observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
+		 let args_id = List.map (fun (id,_,_) -> id) args in
+		 let dyn_infos = 
+		   {
+		     nb_rec_hyps = -100;
+		     rec_hyps = [];
+		     info = 
+		       Reductionops.nf_betaiota 
+			 (applist(fix_body,List.rev_map mkVar args_id));
+		     eq_hyps = []
+		   }
 		 in
-		 observe_tac "instanciating rec hyps"
-		   (instanciate_hyps_with_args do_prove_on_branches !branches  (List.rev realargs_ids))
-		   g'
-	      ))
-	      g
-	 )
-       ]
-       goal
+		 tclTHENSEQ
+		   [
+		     observe_tac "do_replace" 
+		       (do_replace princ_info.params fix_info.idx args_id
+			  (List.hd (List.rev pte_args)) fix_body);
+		     let do_prove = 
+		       build_proof 
+			 interactive_proof
+			 (Array.to_list fnames) 
+			 (Idmap.map prove_rec_hyp ptes_to_fix)
+		     in
+		     let prove_tac branches  = 
+		       let dyn_infos = 
+			 {dyn_infos with 
+			    rec_hyps = branches;
+			    nb_rec_hyps = List.length branches
+			 }
+		       in
+		       clean_goal_with_heq
+			 (Idmap.map prove_rec_hyp ptes_to_fix) 
+			 do_prove 
+			 dyn_infos
+		     in
+(* 		     observe (str "branches := " ++  *)
+(* 				prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches); *)
+		     observe_tac "instancing" (instanciate_hyps_with_args prove_tac 
+		       (List.rev_map id_of_decl princ_info.branches) 
+		       (List.rev args_id))
+		   ]
+		   g
+	      );
+	    ] gl
+	with Not_found ->
+	  let nb_args = min (princ_info.nargs) (List.length ctxt) in
+	  tclTHENSEQ
+	    [
+	      tclDO nb_args intro;
+	      (fun g -> (* replacement of the function by its body *)
+		 let args = nLastHyps nb_args g in 
+		 let args_id = List.map (fun (id,_,_) -> id) args in
+		 let dyn_infos = 
+		   {
+		     nb_rec_hyps = -100;
+		     rec_hyps = [];
+		     info = 
+		       Reductionops.nf_betaiota 
+			 (applist(fbody_with_full_params,
+				  (List.rev_map var_of_decl princ_params)@
+				    (List.rev_map mkVar args_id)
+				 ));
+		     eq_hyps = []
+		   }
+		 in
+		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
+		 tclTHENSEQ
+		   [unfold_in_concl [([],Names.EvalConstRef fname)];
+		    let do_prove = 
+		      build_proof 
+			interactive_proof
+			(Array.to_list fnames) 
+			 (Idmap.map prove_rec_hyp ptes_to_fix)
+		    in
+		    let prove_tac branches  = 
+		      let dyn_infos = 
+			 {dyn_infos with 
+			    rec_hyps = branches;
+			    nb_rec_hyps = List.length branches
+			 }
+		      in
+		       clean_goal_with_heq
+			 (Idmap.map prove_rec_hyp ptes_to_fix) 
+			 do_prove 
+			 dyn_infos
+		    in
+		    instanciate_hyps_with_args prove_tac 
+		       (List.rev_map id_of_decl princ_info.branches) 
+		      (List.rev args_id)
+		   ]
+		   g
+	      )
+	    ] 
+	  gl
+    in
+    tclTHEN 
+      first_tac
+      intros_after_fixes
+      g
+	    
+
+
 
 
 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index bd48266a4..240869ae8 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -55,12 +55,14 @@ END
 
 
 let pr_intro_as_pat prc _ _ pat = 
-  str "as" ++ spc () ++ pr_intro_pattern pat
+  match pat with 
+    | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat
+    | None -> mt ()
 
 
-ARGUMENT EXTEND with_names TYPED AS intro_pattern PRINTED BY pr_intro_as_pat
-|   [ "as"  simple_intropattern(ipat) ] -> [ ipat ] 
-| []  ->[ IntroAnonymous ] 
+ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat
+|   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ] 
+| []  ->[ None ] 
 END
 
 
@@ -84,6 +86,11 @@ let choose_dest_or_ind scheme_info =
 TACTIC EXTEND newfunind
    ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
      [
+       let pat = 
+	 match pat with 
+	   | None -> IntroAnonymous
+	   | Some pat -> pat
+       in
        let c = match cl with 
 	 | [] -> assert false
 	 | [c] -> c 
@@ -120,11 +127,45 @@ TACTIC EXTEND newfunind
 	   List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) 
 	 in 
 	 let princ' = Some (princ,Rawterm.NoBindings) in 
-	 choose_dest_or_ind 
+	 let princ_vars = 
+	   List.fold_right 
+	     (fun a acc -> 
+		try Idset.add (destVar a) acc
+		with _ -> acc
+	     )
+	     args
+	     Idset.empty
+	 in
+	 let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in 
+	 let old_idl = Idset.diff old_idl princ_vars in 
+	 let subst_and_reduce g = 
+	   let idl = 
+	     Util.map_succeed 
+	       (fun id -> 
+		  if Idset.mem id old_idl then failwith "";
+		  id 
+	       )
+	       (Tacmach.pf_ids_of_hyps g)
+	   in 
+	   let flag = 
+	     Rawterm.Cbv
+	       {Rawterm.all_flags 
+		with Rawterm.rDelta = false; 		 
+	       }
+	   in
+	   Tacticals.tclTHEN
+	     (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
+	     (Hiddentac.h_reduce flag Tacticals.allClauses)
+	     g
+	 in
+	 Tacticals.tclTHEN
+	   (choose_dest_or_ind 
 	   princ_infos
 	   args_as_induction_constr
 	   princ'
-	   pat g
+	   pat)
+	   subst_and_reduce
+	   g
      ]
 END
 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index af8093fc6..c6406468a 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -130,7 +130,7 @@ let change_vars =
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
-      | RRec _ -> error "Not handled RRec"
+      | RRec _ -> error "Local (co)fixes are not supported"
       | RSort _ -> rt 
       | RHole _ -> rt 
       | RCast(loc,b,k,t) -> 
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 84a58a3ad..939d06c77 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -5,25 +5,17 @@ Definition iszero (n : nat) : bool :=
   | _ => false
   end.
 
- Functional Scheme iszer_ind := Induction for iszero.
+Functional Scheme iszero_ind := Induction for iszero Sort Prop.
  
 Lemma toto : forall n : nat, n = 0 -> iszero n = true.
 intros x eg.
  functional induction iszero x; simpl in |- *.
 trivial.
- subst x.
-inversion H_eq_.
+inversion eg.
 Qed.
 
-(* We can even reuse the proof as a scheme: *)
-
- Functional Scheme toto_ind := Induction for iszero.
-
-
-
-
  
-Definition ftest (n m : nat) : nat :=
+Function ftest (n m : nat) : nat :=
   match n with
   | O => match m with
          | O => 0
@@ -32,27 +24,25 @@ Definition ftest (n m : nat) : nat :=
   | S p => 0
   end.
 
- Functional Scheme ftest_ind := Induction for ftest. 
-
 Lemma test1 : forall n m : nat, ftest n m <= 2.
 intros n m.
  functional induction ftest n m; auto.
 Qed.
 
-
+Require Import Arith.
 Lemma test11 : forall m : nat, ftest 0 m <= 2.
 intros m.
  functional induction ftest 0 m.
 auto. 
-auto. 
+auto.
+auto with *. 
 Qed.
 
-
-Definition lamfix (m : nat) :=
-  fix trivfun (n : nat) : nat := match n with
-                                 | O => m
-                                 | S p => trivfun p
-                                 end.
+Function lamfix (m n : nat) {struct n } : nat :=
+  match n with
+    | O => m
+    | S p => lamfix m p
+  end.
 
 (* Parameter v1 v2 : nat. *)
 
@@ -68,12 +58,12 @@ Defined.
 (* polymorphic function *)
 Require Import List.
 
- Functional Scheme app_ind := Induction for app.
+Functional Scheme app_ind := Induction for app Sort Prop.
 
 Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
 intros A l l'.
  functional induction app A l l';  intuition.
- rewrite <- H1; trivial.
+ rewrite <- H0; trivial.
 Qed.
 
 
@@ -83,7 +73,7 @@ Qed.
 Require Export Arith.
 
 
-Fixpoint trivfun (n : nat) : nat :=
+Function trivfun (n : nat) : nat :=
   match n with
   | O => 0
   | S m => trivfun m
@@ -97,18 +87,16 @@ Parameter varessai : nat.
 Lemma first_try : trivfun varessai = 0.
  functional induction trivfun varessai.
 trivial.
-simpl in |- *.
 assumption.
 Defined.
  
 
- Functional Scheme triv_ind := Induction for trivfun.
+ Functional Scheme triv_ind := Induction for trivfun Sort Prop.
 
 Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
 intros n'.
  functional induction trivfun n'.
 trivial.
-simpl in |- *.
 assumption.
 Qed.
 
@@ -118,14 +106,14 @@ Qed.
 
 
 
-Fixpoint iseven (n : nat) : bool :=
+Function iseven (n : nat) : bool :=
   match n with
   | O => true
   | S (S m) => iseven m
   | _ => false
   end.
  
-Fixpoint funex (n : nat) : nat :=
+Function funex (n : nat) : nat :=
   match iseven n with
   | true => n
   | false => match n with
@@ -134,7 +122,7 @@ Fixpoint funex (n : nat) : nat :=
              end
   end.
  
-Fixpoint nat_equal_bool (n m : nat) {struct n} : bool :=
+Function nat_equal_bool (n m : nat) {struct n} : bool :=
   match n with
   | O => match m with
          | O => true
@@ -149,6 +137,7 @@ Fixpoint nat_equal_bool (n m : nat) {struct n} : bool :=
 
 Require Export Div2.
  
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
 Lemma div2_inf : forall n : nat, div2 n <= n.
 intros n.
  functional induction div2 n.
@@ -157,34 +146,27 @@ auto.
 
 apply le_S.
 apply le_n_S.
-exact H.
+exact IHn0.
 Qed.
 
 (* reuse this lemma as a scheme:*)
 
- Functional Scheme div2_ind := Induction for div2_inf.
 
-Fixpoint nested_lam (n : nat) : nat -> nat :=
+Function nested_lam (n : nat) : nat -> nat :=
   match n with
   | O => fun m : nat => 0
   | S n' => fun m : nat => m + nested_lam n' m
   end.
 
- Functional Scheme nested_lam_ind := Induction for nested_lam.
 
 Lemma nest : forall n m : nat, nested_lam n m = n * m.
 intros n m.
- functional induction nested_lam n m; auto.
-Qed.
-
-Lemma nest2 : forall n m : nat, nested_lam n m = n * m.
-intros n m. pattern n, m in |- *. 
-apply nested_lam_ind; simpl in |- *; intros; auto.
+ functional induction nested_lam n m; simpl;auto.
 Qed.
 
  
-Fixpoint essai (x : nat) (p : nat * nat) {struct x} : nat :=
-  let (n, m) := p in
+Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
+  let (n, m) := (p: nat*nat) in
   match n with
   | O => 0
   | S q => match x with
@@ -198,12 +180,12 @@ Lemma essai_essai :
 intros x p.
  functional induction essai x p; intros.
 inversion H.
-simpl in |- *; try abstract auto with arith.
-simpl in |- *; try abstract auto with arith.
+auto with arith.
+ auto with arith.
 Qed.
 
  
-Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat :=
+Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
   let x := nat_equal_bool m 5 in
   let y := 0 in
   match n with
@@ -218,21 +200,18 @@ Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat :=
  
 Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
 intros a b.
-unfold plus_x_not_five'' in |- *.
  functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
 Qed.
  
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
-unfold nat_equal_bool in |- *.
  functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
-inversion hyp.
+rewrite <- hyp in H1; simpl in H1;tauto. 
 inversion hyp.
 Qed.
  
 Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
 intros n m.
-unfold nat_equal_bool in |- *.
  functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
 inversion eg.
 inversion eg.
@@ -242,6 +221,8 @@ Qed.
 Inductive istrue : bool -> Prop :=
     istrue0 : istrue true.
  
+Functional Scheme plus_ind := Induction for plus Sort Prop.
+
 Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
 intros n m.
  functional induction plus n m; intros.
@@ -264,7 +245,7 @@ intros n.
  functional induction plus 0 n; intros; auto with arith.
 Qed.
 
-Fixpoint mod2 (n : nat) : nat :=
+Function mod2 (n : nat) : nat :=
   match n with
   | O => 0
   | S (S m) => S (mod2 m)
@@ -276,13 +257,13 @@ intros n.
  functional induction mod2 n; simpl in |- *; auto with arith.
 Qed.
  
-Definition isfour (n : nat) : bool :=
+Function isfour (n : nat) : bool :=
   match n with
   | S (S (S (S O))) => true
   | _ => false
   end.
  
-Definition isononeorfour (n : nat) : bool :=
+Function isononeorfour (n : nat) : bool :=
   match n with
   | S O => true
   | S (S (S (S O))) => true
@@ -294,15 +275,22 @@ intros n.
  functional induction isononeorfour n; intros istr; simpl in |- *;
  inversion istr.
 apply istrue0.
+destruct n. inversion istr.
+destruct n. tauto.
+destruct n. inversion istr.
+destruct n. inversion istr.
+destruct n. tauto.
+simpl in *. inversion H1.
 Qed.
  
 Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
 intros n.
  functional induction isononeorfour n; intros m istr; inversion istr.
 apply istrue0.
+rewrite H in H0; simpl in H0;tauto.
 Qed.
  
-Definition ftest4 (n m : nat) : nat :=
+Function ftest4 (n m : nat) : nat :=
   match n with
   | O => match m with
          | O => 0
@@ -321,13 +309,20 @@ Qed.
  
 Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
 intros n m.
- functional induction ftest4 (S n) m.
+assert ({n0 | n0 = S n}).
+exists (S n);reflexivity.
+destruct H as [n0 H1].
+rewrite <- H1;revert H1.
+ functional induction ftest4 n0 m.
+inversion 1.
+inversion 1.
+
 auto with arith.
 auto with arith.
 Qed.
  
-Definition ftest44 (x : nat * nat) (n m : nat) : nat :=
-  let (p, q) := x in
+Function ftest44 (x : nat * nat) (n m : nat) : nat :=
+  let (p, q) := (x: nat*nat) in
   match n with
   | O => match m with
          | O => 0
@@ -349,7 +344,7 @@ auto with arith.
 auto with arith.
 Qed.
  
-Fixpoint ftest2 (n m : nat) {struct n} : nat :=
+Function ftest2 (n m : nat) {struct n} : nat :=
   match n with
   | O => match m with
          | O => 0
@@ -363,7 +358,7 @@ intros n m.
  functional induction ftest2 n m; simpl in |- *; intros; auto.
 Qed.
  
-Fixpoint ftest3 (n m : nat) {struct n} : nat :=
+Function ftest3 (n m : nat) {struct n} : nat :=
   match n with
   | O => 0
   | S p => match m with
@@ -384,7 +379,7 @@ simpl in |- *.
 auto.
 Qed.
  
-Fixpoint ftest5 (n m : nat) {struct n} : nat :=
+Function ftest5 (n m : nat) {struct n} : nat :=
   match n with
   | O => 0
   | S p => match m with
@@ -405,7 +400,7 @@ simpl in |- *.
 auto.
 Qed.
  
-Definition ftest7 (n : nat) : nat :=
+Function ftest7 (n : nat) : nat :=
   match ftest5 n 0 with
   | O => 0
   | S r => 0
@@ -416,11 +411,10 @@ Lemma essai7 :
    (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) 
    (n : nat), ftest7 n <= 2.
 intros hyp1 hyp2 n.
-unfold ftest7 in |- *.
  functional induction ftest7 n; auto.
 Qed.
  
-Fixpoint ftest6 (n m : nat) {struct n} : nat :=
+Function ftest6 (n m : nat) {struct n} : nat :=
   match n with
   | O => 0
   | S p => match ftest5 p 0 with
@@ -445,7 +439,6 @@ Qed.
  
 Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
 intros n m.
-unfold ftest6 in |- *.
  functional induction ftest6 n m; simpl in |- *; auto.
 Qed.
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index af5cee4fa..a94f40637 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -512,7 +512,7 @@ Proof.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt H2); intuition_in.
+ rewrite (IHt H1); intuition_in.
  (* EQ *)  
  inv avl.
  firstorder_in.
@@ -520,7 +520,7 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt H3); intuition_in.
+ rewrite (IHt H2); intuition_in.
 Qed.
 
 Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m).
@@ -528,15 +528,15 @@ Proof.
  intros elt m x e; functional induction (add x e m); 
    intros; inv bst; inv avl; auto; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H5.
+ red; red in H4.
  intros.
- rewrite (add_in x y0 e H1) in H2.
+ rewrite (add_in x y0 e H) in H1.
  intuition.
  eauto.
  (* gt_tree -> gt_tree (add ...) *)
  red; red in H5.
  intros.
- rewrite (add_in x y0 e H7) in H2.
+ rewrite (add_in x y0 e H6) in H1.
  intuition.
  apply lt_eq with x; auto.
 Qed.
@@ -588,7 +588,7 @@ Proof.
  inv avl; simpl in *; split; auto.
  avl_nns; omega_max.
  (* l = Node *)
- inversion_clear H1.
+ inversion_clear H.
  destruct (IHp lh); auto.
  split; simpl in *. 
  rewrite_all H0. simpl in *.
@@ -609,14 +609,14 @@ Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in.
  (* l = Node *)
- inversion_clear H1.
- generalize (remove_min_avl H2).
+ inversion_clear H.
+ generalize (remove_min_avl H1).
  
  rewrite_all H0; simpl; intros.
  rewrite bal_in; auto.
- generalize (IHp lh y H2).
+ generalize (IHp lh y H1).
  intuition.
- inversion_clear H9; intuition.
+ inversion_clear H8; intuition.
 Qed.
 
 Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> 
@@ -627,15 +627,15 @@ Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in; subst; auto.
  (* l = Node *)
- inversion_clear H1.
- generalize (remove_min_avl H2).
+ inversion_clear H.
+ generalize (remove_min_avl H1).
  rewrite_all H0; simpl; intros.
  rewrite bal_mapsto; auto; unfold create.
  simpl in *;destruct (IHp lh y e').
  auto.
  intuition.
- inversion_clear H4; intuition.
- inversion_clear H11; intuition.
+ inversion_clear H3; intuition.
+ inversion_clear H10; intuition.
 Qed.
 
 Lemma remove_min_bst : forall elt (l:t elt) x e r h, 
@@ -643,14 +643,14 @@ Lemma remove_min_bst : forall elt (l:t elt) x e r h,
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H1; inversion_clear H2.
+ inversion_clear H; inversion_clear H1.
  apply bal_bst; auto.
  rewrite_all H0;simpl in *;firstorder.
  intro; intros.
- generalize (remove_min_in y H1).
+ generalize (remove_min_in y H).
  rewrite_all H0; simpl in *.
  destruct 1.
- apply H5; intuition.
+ apply H4; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, 
@@ -659,15 +659,15 @@ Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h,
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H1; inversion_clear H2.
+ inversion_clear H; inversion_clear H1.
  intro; intro.
  rewrite_all H0;simpl in *.
- generalize (IHp lh H3 H1); clear H9 H8 IHp.
- generalize (remove_min_avl H1).
- generalize (remove_min_in (fst m) H1).
+ generalize (IHp lh H2 H); clear H7 H8 IHp.
+ generalize (remove_min_avl H).
+ generalize (remove_min_in (fst m) H).
  rewrite H0; simpl; intros.
- rewrite (bal_in x e y H9 H7) in H2.
- destruct H8.
+ rewrite (bal_in x e y H8 H6) in H1.
+ destruct H7.
  firstorder.
  apply lt_eq with x; auto.
  apply X.lt_trans with x; auto.
@@ -694,13 +694,13 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 ->
  avl (merge s1 s2) /\ 
  0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
 Proof.
- intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros;subst.
+ intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros.
  split; auto; avl_nns; omega_max.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  split; auto; avl_nns; simpl in *; omega_max.
- destruct _x;try contradiction;clear H1.
- generalize (remove_min_avl_1 H4).
-rewrite H2; simpl;destruct 1.
+ destruct s1;try contradiction;clear H1.
+ generalize (remove_min_avl_1 H0).
+ rewrite H2; simpl;destruct 1.
  split.
  apply bal_avl; auto.
  simpl; omega_max.
@@ -716,10 +716,10 @@ Qed.
 Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (In y (merge s1 s2) <-> In y s1 \/ In y s2).
 Proof. 
- intros elt s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
+ intros elt s1 s2; functional induction (merge s1 s2);intros.
  intuition_in.
  intuition_in.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
 (*  rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *)
  replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
  rewrite bal_in; auto.
@@ -731,10 +731,10 @@ Qed.
 Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
   (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2).
 Proof.
- intros elt s1 s2; functional induction (@merge elt s1 s2); subst; simpl in *; intros.
+ intros elt s1 s2; functional induction (@merge elt s1 s2); intros.
  intuition_in.
  intuition_in.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
  rewrite bal_mapsto; auto; unfold create.
  generalize (remove_min_avl H4); rewrite H2; simpl; auto.
@@ -747,16 +747,16 @@ Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2
  (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (merge s1 s2). 
 Proof.
- intros elt s1 s2; functional induction (@merge elt s1 s2); subst;simpl in *; intros; auto.
+ intros elt s1 s2; functional induction (@merge elt s1 s2); intros; auto.
 
  apply bal_bst; auto.
- destruct _x;try contradiction.
+ destruct s1;try contradiction.
  generalize (remove_min_bst H3); rewrite H2; simpl in *; auto.
- destruct _x;try contradiction.
+ destruct s1;try contradiction.
  intro; intro.
  apply H5; auto.
  generalize (remove_min_in x H4); rewrite H2; simpl; intuition.
- destruct _x;try contradiction.
+ destruct s1;try contradiction.
  generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto.
 Qed. 
 
@@ -775,7 +775,7 @@ Function remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with
 Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> 
  avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
 Proof.
- intros elt s x; functional induction (@remove elt x s); subst;simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); intros.
  split; auto; omega_max.
  (* LT *)
  inv avl.
@@ -811,20 +811,20 @@ Proof.
  (* LT *)
  inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (IHt y0 H2); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
  (* EQ *)
  inv avl; inv bst; clear H0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
- elim H10; eauto.
+ elim H9; eauto.
  (* GT *)
  inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (IHt y0 H7); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H6); intuition; [ order | order | intuition_in ].
 Qed.
 
 Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s).
 Proof. 
- intros elt s x; functional induction (@remove elt x s); subst;simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); simpl; intros.
  auto.
  (* LT *)
  inv avl; inv bst.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 128ed45d2..5564b174b 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -112,7 +112,7 @@ Proof.
  intros m Hm x; generalize Hm; clear Hm.      
  functional induction (mem x m);intros sorted belong1;trivial.
  
- inversion belong1. inversion H0.
+ inversion belong1. inversion H.
  
  absurd (In x ((k', _x) :: l));try assumption.
  apply Sort_Inf_NotIn with _x;auto.
@@ -200,7 +200,7 @@ Proof.
  functional induction (add x e' m) ;simpl;auto;  clear H0.
  subst;auto.
 
- intros y' e'' eqky';  inversion_clear 1; destruct H1; simpl in *.
+ intros y' e'' eqky';  inversion_clear 1;  destruct H0; simpl in *.
  order.
  auto.
  auto.
@@ -213,10 +213,10 @@ Lemma add_3 : forall m x y e e',
 Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl; intros.
+ apply (In_inv_3 H0); compute; auto.
  apply (In_inv_3 H1); compute; auto.
- subst s;apply (In_inv_3 H2); compute; auto.
- constructor 2; apply (In_inv_3 H2); compute; auto. 
- inversion_clear H2; auto.
+ constructor 2; apply (In_inv_3 H1); compute; auto. 
+ inversion_clear H1; auto.
 Qed.
 
 
@@ -441,8 +441,8 @@ Proof.
   apply Inf_lt with (x,e); auto.
  elim (Sort_Inf_NotIn H5 H7 H4).
 
- destruct _x;
- destruct _x0;try contradiction.
+ destruct m;
+ destruct m';try contradiction.
  
  clear H1;destruct p as (k,e).
  destruct (H0 k).
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 415e0c113..53485a67c 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -101,12 +101,12 @@ Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true.
 Proof.
  intros m Hm x; generalize Hm; clear Hm.      
  functional induction (mem x m);intros NoDup belong1;trivial.
- inversion belong1. inversion H0.
+ inversion belong1. inversion H.
  inversion_clear NoDup.
  inversion_clear belong1.
- inversion_clear H3.
- compute in H4; destruct H4.
- elim H; auto.
+ inversion_clear H2.
+ compute in H3; destruct H3.
+ contradiction.
  apply IHb; auto.
  exists x0; auto.
 Qed. 
@@ -184,7 +184,7 @@ Proof.
  intros m x  y e e'; generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl;auto.
  intros y' e'' eqky';  inversion_clear 1.
- destruct H2; simpl in *.
+ destruct H1; simpl in *.
  elim eqky'; apply X.eq_trans with k'; auto.
  auto.
  intros y' e'' eqky'; inversion_clear 1; intuition.
@@ -195,8 +195,8 @@ Lemma add_3 : forall m x y e e',
 Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl;auto.
- intros; apply (In_inv_3 H1); auto.
- constructor 2; apply (In_inv_3 H2); auto.
+ intros; apply (In_inv_3 H0); auto.
+ constructor 2; apply (In_inv_3 H1); auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -206,10 +206,10 @@ Proof.
  intros m x y e e'. generalize y e; clear y e.
  functional induction (add x e' m);simpl;auto.
  inversion_clear 2.
- compute in H2; elim H0; auto.
- inversion H2. 
- constructor 2; inversion_clear H2; auto.
- compute in H3; elim H1; auto.
+ compute in H1; elim H; auto.
+ inversion H1. 
+ constructor 2; inversion_clear H1; auto.
+ compute in H2; elim H; auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -268,21 +268,21 @@ Proof.
  intros m Hm x y; generalize Hm; clear Hm.
  functional induction (remove x m);simpl;intros;auto.
 
- red; inversion 1; inversion H2.
+ red; inversion 1; inversion H1.
 
  inversion_clear Hm.
  subst.
- swap H2.
- destruct H as (e,H); unfold PX.MapsTo in H.
+ swap H1.
+ destruct H3 as (e,H3); unfold PX.MapsTo in H3.
  apply InA_eqk with (y,e); auto.
  compute; apply X.eq_trans with x; auto.
   
  intro H2.
  destruct H2 as (e,H2); inversion_clear H2.
- compute in H3; destruct H3.
+ compute in H1; destruct H1.
  elim _x; apply X.eq_trans with y; auto.
  inversion_clear Hm.
- elim (IHt0 H4 H1).
+ elim (IHt0 H3 H).
  exists e; auto.
 Qed.
   
@@ -292,8 +292,8 @@ Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
  functional induction (remove x m);auto.
  inversion_clear 3; auto.
- compute in H3; destruct H3.
- elim H1; apply X.eq_trans with k'; auto.
+ compute in H2; destruct H2.
+ elim H; apply X.eq_trans with k'; auto.
   
  inversion_clear 1; inversion_clear 2; auto.
 Qed.
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 5b912f8b2..425cfdfac 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -515,7 +515,7 @@ Proof.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt y0 H2); intuition_in.
+ rewrite (IHt y0 H1); intuition_in.
  (* EQ *)  
  inv avl.
  intuition.
@@ -523,7 +523,7 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt y0 H3); intuition_in.
+ rewrite (IHt y0 H2); intuition_in.
 Qed.
 
 Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s).
@@ -533,14 +533,14 @@ Proof.
  (* lt_tree -> lt_tree (add ...) *)
  red; red in H5.
  intros.
- rewrite (add_in l x y0 H1) in H2.
+ rewrite (add_in l x y0 H) in H1.
  intuition.
  eauto.
  inv bst; inv avl; apply bal_bst; auto.
  (* gt_tree -> gt_tree (add ...) *)
  red; red in H5.
  intros.
- rewrite (add_in r x y0 H7) in H2.
+ rewrite (add_in r x y0 H6) in H1.
  intuition.
  apply MX.lt_eq with x; auto.
 Qed.
@@ -722,13 +722,13 @@ Proof.
  intros l x r; functional induction (remove_min l x r); simpl in *; intros.
  intuition_in.
  (* l = Node *)
- inversion_clear H1.
- generalize (remove_min_avl ll lx lr lh H2).
+ inversion_clear H.
+ generalize (remove_min_avl ll lx lr lh H1).
  rewrite H0; simpl; intros.
  rewrite bal_in; auto.
- rewrite H0 in IHp;generalize (IHp lh y H2).
+ rewrite H0 in IHp;generalize (IHp lh y H1).
  intuition.
- inversion_clear H9; intuition.
+ inversion_clear H8; intuition.
 Qed.
 
 Lemma remove_min_bst : forall l x r h, 
@@ -788,7 +788,7 @@ Proof.
  intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
  split; auto; avl_nns; omega_max.
  split; auto; avl_nns; simpl in *; omega_max.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  generalize (remove_min_avl_1 l2 x2 r2 h2 H0).
  rewrite H2; simpl; destruct 1.
  split.
@@ -809,7 +809,7 @@ Proof.
  intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros.
  intuition_in.
  intuition_in.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto].
  rewrite bal_in; auto.
  generalize (remove_min_avl l2 x2 r2 h2); rewrite H2; simpl; auto.
@@ -822,7 +822,7 @@ Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 ->
  bst (merge s1 s2). 
 Proof.
  intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  apply bal_bst; auto.
  generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto.
  intro; intro.
@@ -901,8 +901,8 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in l x y0) in H1; auto.
- destruct H1; eauto.
+ rewrite (remove_in l x y0) in H; auto.
+ destruct H; eauto.
  (* EQ *)
  inv avl; inv bst.
  apply merge_bst; eauto.
@@ -910,8 +910,8 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in r x y0) in H1; auto.
- destruct H1; eauto.
+ rewrite (remove_in r x y0) in H; auto.
+ destruct H; eauto.
 Qed.
 
  (** * Minimum element *)
@@ -1038,7 +1038,7 @@ Function concat (s1 s2 : t) : t  :=
 Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
 Proof.
  intros s1 s2; functional induction (concat s1 s2); subst;auto.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  intros; apply join_avl; auto.
  generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto.
 Qed.
@@ -1048,7 +1048,7 @@ Lemma concat_bst :   forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 ->
  bst (concat s1 s2).
 Proof. 
  intros s1 s2; functional induction (concat s1 s2); subst ;auto.
- destruct _x;try contradiction;clear H1. 
+ destruct s1;try contradiction;clear H1. 
  intros;  apply join_bst; auto.
  generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto.
  generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
@@ -1064,10 +1064,10 @@ Proof.
  intros s1 s2; functional induction (concat s1 s2);subst;simpl.
  intuition.
  inversion_clear H5.
- destruct _x;try contradiction;clear H1;intuition.
+ destruct s1;try contradiction;clear H1;intuition.
  inversion_clear H5.
- destruct _x;try contradiction;clear H1; intros. 
- rewrite (join_in  (Node _x1 t _x2 i) m s2' y H0).
+ destruct s1;try contradiction;clear H1; intros. 
+ rewrite (join_in  (Node s1_1 t s1_2 i) m s2' y H0).
  generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
  generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl.
  intro EQ; rewrite EQ; intuition.