aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-27 11:03:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 12:08:03 +0200
commitf14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch)
tree8a331593d0d1b518e8764c92ac54e3b11c222358 /proofs/proof.ml
parent500d38d0887febb614ddcadebaef81e0c7942584 (diff)
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml28
1 files changed, 14 insertions, 14 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 86af420dc..5fe29653d 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -64,17 +64,17 @@ exception NoSuchGoals of int * int
exception FullyUnfocused
-let _ = Errors.register_handler begin function
+let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- Errors.error "This proof is focused, but cannot be unfocused this way"
+ CErrors.error "This proof is focused, but cannot be unfocused this way"
| NoSuchGoals (i,j) when Int.equal i j ->
- Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+ CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
- Errors.errorlabstrm "Focus" Pp.(
+ CErrors.errorlabstrm "Focus" Pp.(
str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
)
- | FullyUnfocused -> Errors.error "The proof is not focused"
- | _ -> raise Errors.Unhandled
+ | FullyUnfocused -> CErrors.error "The proof is not focused"
+ | _ -> raise CErrors.Unhandled
end
let check_cond_kind c k =
@@ -300,12 +300,12 @@ exception UnfinishedProof
exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
-let _ = Errors.register_handler begin function
- | UnfinishedProof -> Errors.error "Some goals have not been solved."
- | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
- | HasGivenUpGoals -> Errors.error "Some goals have been given up."
- | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | UnfinishedProof -> CErrors.error "Some goals have not been solved."
+ | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
+ | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
+ | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+ | _ -> raise CErrors.Unhandled
end
let return p =
@@ -397,9 +397,9 @@ module V82 = struct
let evl = Evarutil.non_instantiated sigma in
let evl = Evar.Map.bindings evl in
if (n <= 0) then
- Errors.error "incorrect existential variable index"
+ CErrors.error "incorrect existential variable index"
else if CList.length evl < n then
- Errors.error "not so many uninstantiated existential variables"
+ CErrors.error "not so many uninstantiated existential variables"
else
CList.nth evl (n-1)
in