Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

4 files changed, 53 insertions, 49 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1d1e4a2a..33d77568 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1371,7 +1371,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 (* 		 let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
 (* 		 rewrite *)
 (* 	      ) *)
-	      Eauto.gen_eauto false (false,5) [] (Some [])
+	      Eauto.gen_eauto (false,5) [] (Some [])
 	    ]
 	    gls
 
@@ -1449,7 +1449,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			   (
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
-				      false
 				      (true,5)
 				      [Evd.empty,Lazy.force refl_equal]
 				      [Auto.Hint_db.empty empty_transparent_state false]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 123399d5..06abb8ce 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna
 let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
   (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
   (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) =
-  Genarg.create_arg "function_rec_definition_loc"
+  Genarg.create_arg None "function_rec_definition_loc"
 VERNAC COMMAND EXTEND Function
    ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
 	[
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0b04a572..95ca86c2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -588,15 +588,15 @@ let rec reflexivity_with_destruct_cases g =
     )
   in
   (tclFIRST
-    [ reflexivity;
-      tclTHEN (tclPROGRESS discr_inject) (destruct_case ());
+    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity;
+      observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
       (*  We reach this point ONLY if
 	  the same value is matched (at least) two times
 	  along binding path.
 	  In this case, either we have a discriminable hypothesis and we are done,
 	  either at least an injectable one and we do the injection before continuing
       *)
-      tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases
+      observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases)
     ])
     g
 
@@ -752,6 +752,7 @@ let do_save () = Lemmas.save_named false
 *)
 
 let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
+  let previous_state = States.freeze () in
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let funs_constr = Array.map mkConst funs  in
   try
@@ -793,22 +794,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Lemmas.start_proof
-	   (*i The next call to mk_correct_id is valid since we are constructing the lemma
+	 (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
-	     i*)
-	   (mk_correct_id f_id)
+	 i*)
+	 let lem_id = mk_correct_id f_id in
+	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
-	 Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
+	 Pfedit.by
+	   (observe_tac ("prove correctness ("^(string_of_id f_id)^")")
+	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
-	 update_Function
-	   {finfo with
-	      correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id)))
-	   }
-
+	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
+	 update_Function {finfo with correctness_lemma = Some lem_cst}
       )
       funs;
     let lemmas_types_infos =
@@ -845,34 +845,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Lemmas.start_proof
-	   (*i The next call to mk_complete_id is valid since we are constructing the lemma
+	 (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
-	     i*)
-	   (mk_complete_id f_id)
+	   i*)
+	 let lem_id = mk_complete_id f_id in
+	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
-	 Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
+	 Pfedit.by
+	   (observe_tac ("prove completeness ("^(string_of_id f_id)^")")
+	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
-	 update_Function
-	   {finfo with
-	      completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id)))
-	   }
+	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
+	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs;
   with e ->
     (* In case of problem, we reset all the lemmas *)
-    (*i The next call to mk_correct_id is valid since we are erasing the lemmas
-      Ensures by: obvious
-      i*)
-    let first_lemma_id =
-      let f_id = id_of_label (con_label funs.(0)) in
-
-      mk_correct_id f_id
-    in
-     ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ());
+    Pfedit.delete_all_proofs ();
+    States.unfreeze previous_state;
     raise e
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 55ebd31b..3355300e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -48,7 +48,8 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+    (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
@@ -232,18 +233,19 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
   | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[])
   | Var(_) when eq_constr expr f -> errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function")
   | Var(id) -> (fun l -> expr), []
-  | Meta(_) -> error "find_call_occs : Meta"
-  | Evar(_) -> error "find_call_occs : Evar"
+  | Meta(_) -> error "Found a metavariable. Can not treat such a term" 
+  | Evar(_) -> error "Found an evar. Can not treat such a term"
   | Sort(_)  -> (fun l -> expr), []
   | Cast(b,_,_) -> find_call_occs nb_arg nb_lam f b
-  | Prod(_,_,_) -> error "find_call_occs : Prod"
+  | Prod(na,t,b) -> 
+    error "Found a product. Can not treat such a term"
   | Lambda(na,t,b) ->
       begin
 	match find_call_occs nb_arg (succ nb_lam) f b with
 	  | _, [] ->  (* Lambda are authorized as long as they do not contain
 			 recursives calls *)
 	      (fun l -> expr),[]
-	  | _ ->  error "find_call_occs : Lambda"
+	  | _ ->  error "Found a lambda which body contains a recursive call. Such terms are not allowed"
       end
   | LetIn(na,v,t,b) ->
       begin
@@ -254,7 +256,7 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
 	      ((fun  l -> mkLetIn(na,v,t,cf l)),l)
 	  | (cf,(_::_ as l)),(_,[]) ->
 	      ((fun l -> mkLetIn(na,cf l,t,b)), l)
-	  | _ -> error "find_call_occs : LetIn"
+	  | _ -> error "Found a letin with recursive calls in both variable value and body. Such terms are not allowed."
       end
   | Const(_) -> (fun l -> expr), []
   | Ind(_) -> (fun l -> expr), []
@@ -263,8 +265,8 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
       (match find_call_occs nb_arg nb_lam f a with
 	cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
       | _ -> (fun l -> expr),[])
-  | Fix(_) -> error "find_call_occs : Fix"
-  | CoFix(_) -> error "find_call_occs : CoFix";;
+  | Fix(_) -> error "Found a local fixpoint. Can not treat such a term"
+  | CoFix(_) -> error "Found a local cofixpoint : CoFix";;
 
 let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
@@ -896,6 +898,20 @@ let build_and_l l =
   let conj_constr = coq_conj () in
   let mk_and p1 p2 =
     Term.mkApp(and_constr,[|p1;p2|]) in
+  let rec is_well_founded t = 
+    match kind_of_term t with 
+      | Prod(_,_,t') -> is_well_founded t'
+      | App(_,_) -> 
+	let (f,_) = decompose_app t in 
+	eq_constr f (well_founded ())
+      | _ -> assert false
+  in
+  let compare t1 t2 = 
+    let b1,b2= is_well_founded t1,is_well_founded t2 in 
+    if (b1&&b2) || not (b1 || b2) then 0
+    else if b1 && not b2 then 1 else -1
+  in
+  let l = List.sort compare l in 
   let rec f  = function
     | [] -> failwith "empty list of subgoals!"
     | [p] -> p,tclIDTAC,1
@@ -1006,7 +1022,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 			  (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
 			  e_assumption;
 		      Eauto.eauto_with_bases
-			false
 			(true,5)
 			[Evd.empty,delayed_force refl_equal]
 			[Auto.Hint_db.empty empty_transparent_state false]
@@ -1378,6 +1393,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
+  let previous_label = Lib.current_command_label () in
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
@@ -1429,7 +1445,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
-(* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
 	  stop := true;
 	end
     end;
@@ -1461,10 +1476,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       hook
   with e ->
     begin
-      ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
-(*       anomaly "Cannot create termination Lemma" *)
+      (try ignore (Backtrack.backto previous_label) with _ -> ());
+      (*       anomaly "Cannot create termination Lemma" *)
       raise e
     end
-
-
-