aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 18:54:06 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 18:54:06 +0200
commite278d031a1d9a7bf3de463d3d415065299c99395 (patch)
treeddd3a123e1887a9fa4634af7559bc7bb67b0cc25 /engine/evd.ml
parentd7664c0530edd196d52e9fd8a4b925dbfefd1b9b (diff)
parent3ce70f21a18cc19e720e8ac54b93652527881942 (diff)
Merge branch 'cerrors-cclosure' into trunk
Was PR#226: CErrors & CClosure
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 1276c5994..196f44760 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -999,7 +999,7 @@ let declare_principal_goal evk evd =
| None -> { evd with
future_goals = evk::evd.future_goals;
principal_future_goal=Some evk; }
- | Some _ -> Errors.error "Only one main subgoal per instantiation."
+ | Some _ -> CErrors.error "Only one main subgoal per instantiation."
let future_goals evd = evd.future_goals