diff options
| -rw-r--r-- | engine/eConstr.mli | 3 | ||||
| -rw-r--r-- | engine/evd.ml | 7 | ||||
| -rw-r--r-- | engine/evd.mli | 1 | ||||
| -rw-r--r-- | proofs/proof.ml | 24 | ||||
| -rw-r--r-- | proofs/proof.mli | 5 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 7 |
6 files changed, 30 insertions, 17 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6532e08e9d..49cbc4d7e5 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t For getting the evar-normal form of a term with evars see {!Evarutil.nf_evar}. *) +val to_constr_opt : Evd.evar_map -> t -> Constr.t option +(** Same as [to_constr], but returns [None] if some unresolved evars remain *) + val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) diff --git a/engine/evd.ml b/engine/evd.ml index 31c326df6a..eee2cb700c 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1376,6 +1376,13 @@ module MiniEConstr = struct in UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c + let to_constr_opt sigma c = + let evar_value ev = Some (existential_value sigma ev) in + try + Some (UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c) + with NotInstantiatedEvar -> + None + let of_named_decl d = d let unsafe_to_named_decl d = d let of_rel_decl d = d diff --git a/engine/evd.mli b/engine/evd.mli index 7560d68805..de73144895 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -689,6 +689,7 @@ module MiniEConstr : sig val of_constr_array : Constr.t array -> t array val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t + val to_constr_opt : evar_map -> t -> Constr.t option val unsafe_to_constr : t -> Constr.t val unsafe_to_constr_array : t array -> Constr.t array diff --git a/proofs/proof.ml b/proofs/proof.ml index 1aeb24606b..4ce932b93d 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -351,19 +351,13 @@ let dependent_start ~name ~poly goals = type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar let print_open_error_reason er = let open Pp in match er with | UnfinishedProof -> str "Attempt to save an incomplete proof" - | HasShelvedGoals -> - str "Attempt to save a proof with shelved goals" | HasGivenUpGoals -> strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed." - | HasUnresolvedEvar -> - strbrk "Attempt to save a proof with existential variables still non-instantiated" exception OpenProof of Names.Id.t option * open_error_reason @@ -375,19 +369,25 @@ let _ = CErrors.register_handler begin function | _ -> raise CErrors.Unhandled end +let warn_remaining_shelved_goals = + CWarnings.create ~name:"remaining-shelved-goals" ~category:"tactics" + (fun () -> Pp.str"The proof has remaining shelved goals") + +let warn_remaining_unresolved_evars = + CWarnings.create ~name:"remaining-unresolved-evars" ~category:"tactics" + (fun () -> Pp.str"The proof has unresolved variables") + let return ?pid (p : t) = if not (is_done p) then raise (OpenProof(pid, UnfinishedProof)) - else if has_shelved_goals p then - raise (OpenProof(pid, HasShelvedGoals)) else if has_given_up_goals p then raise (OpenProof(pid, HasGivenUpGoals)) - else if has_unresolved_evar p then - (* spiwack: for compatibility with <= 8.3 proof engine *) - raise (OpenProof(pid, HasUnresolvedEvar)) - else + else begin + if has_shelved_goals p then warn_remaining_shelved_goals () + else if has_unresolved_evar p then warn_remaining_unresolved_evars (); let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview + end let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in diff --git a/proofs/proof.mli b/proofs/proof.mli index fd5e905a3b..40e8ff7eef 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -130,13 +130,10 @@ val compact : t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. Raises [HasShelvedGoals] if some goals are left on the shelf. - Raises [HasGivenUpGoals] if some goals have been given up. - Raises [HasUnresolvedEvar] if some evars have been left undefined. *) + Raises [HasGivenUpGoals] if some goals have been given up. *) type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar exception OpenProof of Names.Id.t option * open_error_reason diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f8adc58921..4cc73f419e 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -443,8 +443,13 @@ let return_proof ?(allow_partial=false) () = (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) + let proof_opt c = + match EConstr.to_constr_opt evd c with + | Some p -> p + | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") + in let proofs = - List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in + List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~opaque ~feedback_id proof = |