diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.mli | 1 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 1 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 12 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 7 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 |
7 files changed, 5 insertions, 20 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9b671bcf0..eb1081706 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -10,7 +10,6 @@ open Names open Term open Environ open Evd -open Mod_subst open Unification open Misctypes diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index da40427c4..ea2043613 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ open Term open Clenv -open Proof_type open Tacexpr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index e3570242e..107ce7f8e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,8 +9,6 @@ open Util open Pp open Term -open Vars -open Context (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated diff --git a/proofs/logic.ml b/proofs/logic.ml index 53f8093e5..b8206ca1b 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Environ open Reductionops @@ -83,12 +82,6 @@ let apply_to_hyp sign id f = if !check then error_no_such_hypothesis id else sign -let apply_to_hyp_and_dependent_on sign id f g = - try apply_to_hyp_and_dependent_on sign id f g - with Hyp_not_found -> - if !check then error_no_such_hypothesis id - else sign - let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -277,11 +270,6 @@ let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let rename_hyp id1 id2 sign = - apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) _ -> (id2,b,t)) - (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) - (**********************************************************************) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f55ab7007..971729245 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -339,10 +339,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context let return_proof () = - let { proof; strength = (_,poly,_) } = cur_pstate () in + let { pid; proof; strength = (_,poly,_) } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let evd = - let error s = raise (Errors.UserError("last tactic before Qed",s)) in + let error s = + let prf = str " (in proof " ++ Id.print pid ++ str ")" in + raise (Errors.UserError("last tactic before Qed",s ++ prf)) + in try Proof.return proof with | Proof.UnfinishedProof -> error(str"Attempt to save an incomplete proof") diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 26bb78dfe..47b2b255e 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -10,7 +10,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e709be5bc..f5e2bad2a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -9,7 +9,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab |