diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/instances.ml | 4 | ||||
| -rw-r--r-- | plugins/firstorder/rules.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 1394f4764..eebd974ea 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -8,7 +8,7 @@ open Unify open Rules -open Errors +open CErrors open Util open Term open Vars @@ -156,7 +156,7 @@ let left_instance_tac (inst,id) continue seq= (mkApp(idc,[|ot|])) rc in let evmap, _ = try Typing.type_of (pf_env gl) evmap gt - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) else diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 92b6e828e..ffb63af07 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 3e8033da0..1248b60a7 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,7 +7,7 @@ (************************************************************************) open Term -open Errors +open CErrors open Util open Formula open Unify |