aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/coq_omega.ml21
-rw-r--r--plugins/omega/coq_omega.mli4
-rw-r--r--plugins/omega/g_omega.mlg4
-rw-r--r--plugins/omega/omega.ml4
4 files changed, 16 insertions, 17 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 118db01ecb..2eef459217 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -25,7 +25,6 @@ open EConstr
open Tacticals.New
open Tacmach.New
open Tactics
-open Logic
open Libnames
open Nametab
open Contradiction
@@ -971,7 +970,7 @@ let rec transform sigma p t =
tac @ tac', t''
| Kapp(Z_of_nat,[t']) -> default true t'
| _ -> default false t
- with e when catchable_exception e -> default false t
+ with e when noncritical e -> default false t
let shrink_pair p f1 f2 =
match f1,f2 with
@@ -1420,7 +1419,7 @@ let destructure_omega env sigma tac_def (id,c) =
normalize_equation sigma
id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
| _ -> tac_def
- with e when catchable_exception e -> tac_def
+ with e when noncritical e -> tac_def
let reintroduce id =
(* [id] cannot be cleared if dependent: protect it by a try *)
@@ -1527,7 +1526,7 @@ let nat_inject =
Kapp(S,[t]) -> is_number t
| Kapp(O,[]) -> true
| _ -> false
- with e when catchable_exception e -> false
+ with e when noncritical e -> false
in
let rec loop p t : unit Proofview.tactic =
try match destructurate_term sigma t with
@@ -1538,7 +1537,7 @@ let nat_inject =
((Lazy.force coq_inj_S),[t]))
(loop (P_APP 1 :: p) t))
| _ -> explore p t
- with e when catchable_exception e -> explore p t
+ with e when noncritical e -> explore p t
in
if is_number t' then focused_simpl p else loop p t
| Kapp(Pred,[t]) ->
@@ -1551,7 +1550,7 @@ let nat_inject =
(explore p t_minus_one)
| Kapp(O,[]) -> focused_simpl p
| _ -> Proofview.tclUNIT ()
- with e when catchable_exception e -> Proofview.tclUNIT ()
+ with e when noncritical e -> Proofview.tclUNIT ()
and loop = function
| [] -> Proofview.tclUNIT ()
@@ -1615,7 +1614,7 @@ let nat_inject =
]
else loop lit
| _ -> loop lit
- with e when catchable_exception e -> loop lit end
+ with e when noncritical e -> loop lit end
in
let hyps_types = Tacmach.New.pf_hyps_types gl in
loop (List.rev hyps_types)
@@ -1725,7 +1724,7 @@ let destructure_hyps =
(assert_by (Name hid) hty reflexivity)
(loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit))
| _ -> loop lit
- with e when catchable_exception e -> loop lit
+ with e when noncritical e -> loop lit
end
| decl :: lit -> (* variable without body (or !letin_flag isn't set) *)
let i = NamedDecl.get_id decl in
@@ -1857,7 +1856,7 @@ let destructure_hyps =
| _ -> loop lit
with
| Undecidable -> loop lit
- | e when catchable_exception e -> loop lit
+ | e when noncritical e -> loop lit
end
in
let hyps = Proofview.Goal.hyps gl in
diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli
index c292bdbb87..e723082803 100644
--- a/plugins/omega/coq_omega.mli
+++ b/plugins/omega/coq_omega.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index 7c653b223e..888a62b2bc 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 355e61deb9..24cd342e42 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 01:45:05 +0000