Merge branch 'v8.5'

7 files changed, 43 insertions, 15 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8884aef1cf..05f4c49030 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -302,9 +302,9 @@ let rec proof_tac p : unit Proofview.tactic =
   	     Tacticals.New.tclFIRST
 	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
-                Proofview.tclZERO (UserError ("Congruence" ,
+                Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")))]]
+		       "I don't know how to handle dependent equality")]]
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d0b7f3466..36273faae2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -125,10 +125,34 @@ let go_to_proof_mode () =
 
 (* closing gaps *)
 
+(* spiwack: should use [Proofview.give_up] but that would require
+   moving the whole declarative mode into the new proof engine.  It
+   will eventually have to be done.
+
+   As far as I can tell, [daimon_tac] is used after a [thus thesis],
+   it will leave uninstantiated variables instead of giving a relevant
+   message at [Qed]. *)
 let daimon_tac gls =
   set_daimon_flag ();
   {it=[];sigma=sig_sig gls;}
 
+let daimon_instr env p =
+  let (p,(status,_)) =
+    Proof.run_tactic env begin
+      Proofview.tclINDEPENDENT Proofview.give_up
+    end p
+  in
+  p,status
+
+let do_daimon () =
+  let env = Global.env () in
+  let status =
+    Proof_global.with_current_proof begin fun _ p ->
+      daimon_instr env p
+    end
+  in
+  if not status then Pp.feedback Feedback.AddedAxiom else ()
+
 (* post-instruction focus management *)
 
 let goto_current_focus () = 
@@ -144,7 +168,7 @@ let goto_current_focus_or_top () =
 (* return *)
 
 let close_tactic_mode () =
-  try goto_current_focus ()
+  try do_daimon ();goto_current_focus ()
   with Not_found ->
     error "\"return\" cannot be used outside of Declarative Proof Mode."
 
@@ -165,7 +189,7 @@ let close_block bt pts =
       in
       match bt,stack with
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
-	  (goto_current_focus ())
+	  do_daimon ();goto_current_focus ()
       | _, Claim::_ ->
 	  error "\"end claim\" expected."
       | _, Focus_claim::_ ->
@@ -196,7 +220,7 @@ let close_previous_case pts =
     match get_stack pts with
 	Per (et,_,_,_) :: _ -> ()
       | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  goto_current_focus ()
+	  do_daimon ();goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
 
 (* Proof instructions *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 45e5aaf545..a2bbf97ae3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -604,7 +604,8 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
+                errorlabstrm "FunInd.build_scheme"
+                  (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
 	    let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in 
@@ -636,10 +637,12 @@ let build_case_scheme fa =
 (*   let id_to_constr id =  *)
 (*     Constrintern.global_reference  id *)
 (*   in  *)
-  let funs =  (fun (_,f,_) ->
-		 try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
-		 with Not_found ->
-		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+  let funs =
+    let (_,f,_) = fa in
+    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    with Not_found ->
+      errorlabstrm "FunInd.build_case_scheme"
+        (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 738ade8ca3..1c409500ef 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,9 @@ let const_of_id id =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Constrintern.locate_reference princ_ref
-  with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
+  with Not_found ->
+    Errors.errorlabstrm "IndFun.const_of_id"
+      (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d9ae87ecc1..d10924f886 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -378,7 +378,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g));
 				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
@@ -427,7 +426,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       (params_bindings@lemmas_bindings)
     in
-    Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type);
     tclTHENSEQ
       [ 
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c6fab43d1c..77a7f006b7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -305,7 +305,8 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then error ("check_not_nested : failure "^Id.to_string x)
+        then errorlabstrm "Recdef.check_not_nested"
+               (str "check_not_nested: failure " ++ pr_id x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 37428c39da..4e2696dfdb 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1462,7 +1462,7 @@ let coq_omega =
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
       Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
+    with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
   end
   end