From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 plugins/decl_mode/decl_proof_instr.ml | 42 +++++++++++++++++++++++++++--------
 1 file changed, 33 insertions(+), 9 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d0b7f34..1a908064 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::_ ->
@@ -188,7 +212,7 @@ let close_previous_case pts =
     Proof.is_done pts
   then
     match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
+	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
       | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
@@ -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 *)
@@ -749,7 +773,7 @@ let rec take_tac wits gls =
   match wits with
       [] -> tclIDTAC gls
     | wit::rest ->
-	let typ = pf_type_of gls wit in
+	let typ = pf_unsafe_type_of gls wit in
 	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
@@ -830,7 +854,7 @@ let start_tree env ind rp =
 let build_per_info etype casee gls =
   let concl=pf_concl gls in
   let env=pf_env gls in
-  let ctyp=pf_type_of gls casee in
+  let ctyp=pf_unsafe_type_of gls casee in
   let is_dep = dependent casee concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
   let (ind,u) =
@@ -845,7 +869,7 @@ let build_per_info etype casee gls =
       | _ -> mind.mind_nparams,None in
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
-    let typ=pf_type_of gls c in
+    let typ=pf_unsafe_type_of gls c in
       lambda_create env (typ,subst_term c body) in
   let pred= List.fold_right abstract_obj
     real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1204,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let nparams = mind.mind_nparams in
 	let concl=pf_concl gls in
 	let env=pf_env gls in
-	let ctyp=pf_type_of gls casee in
+	let ctyp=pf_unsafe_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let ind', u = destInd hd in
 	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
-	  let typ=pf_type_of gls c in
+	  let typ=pf_unsafe_type_of gls c in
 	    lambda_create env (typ,subst_term c body) in
 	let elim_pred = List.fold_right abstract_obj
 	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
-- 
cgit v1.2.3