aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend102
-rw-r--r--dev/TODO6
-rw-r--r--dev/base_db1
-rw-r--r--dev/changements.txt15
-rw-r--r--dev/db1
-rw-r--r--proofs/clenv.ml35
-rw-r--r--proofs/evar_refiner.ml3
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/refiner.ml5
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/pattern.ml5
-rw-r--r--tactics/tacticals.ml5
-rw-r--r--tactics/tactics.ml2
15 files changed, 110 insertions, 84 deletions
diff --git a/.depend b/.depend
index 846fc89b7..6f010d7aa 100644
--- a/.depend
+++ b/.depend
@@ -155,8 +155,8 @@ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \
toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi
toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi
-toplevel/himsg.cmi: kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
- kernel/sign.cmi kernel/type_errors.cmi
+toplevel/himsg.cmi: kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi \
+ lib/pp.cmi kernel/sign.cmi kernel/type_errors.cmi
toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi
toplevel/mltop.cmi: library/libobject.cmi
toplevel/protectedtoplevel.cmi: lib/pp.cmi
@@ -173,36 +173,14 @@ config/coq_config.cmo: config/coq_config.cmi
config/coq_config.cmx: config/coq_config.cmi
dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi
dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx
-dev/top_printers.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
- kernel/closure.cmi toplevel/command.cmi kernel/constant.cmi \
- parsing/coqast.cmi toplevel/discharge.cmi parsing/egrammar.cmi \
- tactics/elim.cmi kernel/environ.cmi parsing/esyntax.cmi kernel/evd.cmi \
- kernel/generic.cmi kernel/inductive.cmi parsing/lexer.cmi \
- library/libobject.cmi library/library.cmi toplevel/metasyntax.cmi \
- toplevel/mltop.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
- parsing/pretty.cmi parsing/printer.cmi proofs/proof_trees.cmi \
- kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi kernel/sosub.cmi \
- library/states.cmi library/summary.cmi lib/system.cmi \
- tactics/tacentries.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
- tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
- parsing/termast.cmi toplevel/toplevel.cmi pretyping/typing.cmi \
- kernel/univ.cmi toplevel/vernac.cmi toplevel/vernacentries.cmi \
- toplevel/vernacinterp.cmi
-dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
- kernel/closure.cmx toplevel/command.cmx kernel/constant.cmx \
- parsing/coqast.cmx toplevel/discharge.cmx parsing/egrammar.cmx \
- tactics/elim.cmx kernel/environ.cmx parsing/esyntax.cmx kernel/evd.cmx \
- kernel/generic.cmx kernel/inductive.cmx parsing/lexer.cmx \
- library/libobject.cmx library/library.cmx toplevel/metasyntax.cmx \
- toplevel/mltop.cmi kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
- parsing/pretty.cmx parsing/printer.cmx proofs/proof_trees.cmx \
- kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx kernel/sosub.cmx \
- library/states.cmx library/summary.cmx lib/system.cmx \
- tactics/tacentries.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
- tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
- parsing/termast.cmx toplevel/toplevel.cmx pretyping/typing.cmx \
- kernel/univ.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
- toplevel/vernacinterp.cmx
+dev/top_printers.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/environ.cmi \
+ kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \
+ proofs/tacmach.cmi kernel/univ.cmi
+dev/top_printers.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/environ.cmx \
+ kernel/evd.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \
+ proofs/tacmach.cmx kernel/univ.cmx
kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
kernel/term.cmi lib/util.cmi kernel/abstraction.cmi
kernel/abstraction.cmx: kernel/generic.cmx kernel/names.cmx kernel/sosub.cmx \
@@ -284,9 +262,9 @@ kernel/term.cmo: kernel/generic.cmi lib/hashcons.cmi kernel/names.cmi \
kernel/term.cmx: kernel/generic.cmx lib/hashcons.cmx kernel/names.cmx \
lib/pp.cmx kernel/univ.cmx lib/util.cmx kernel/term.cmi
kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
- kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi
+ kernel/sign.cmi kernel/term.cmi lib/util.cmi kernel/type_errors.cmi
kernel/type_errors.cmx: kernel/environ.cmx kernel/names.cmx lib/pp.cmx \
- kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmi
+ kernel/sign.cmx kernel/term.cmx lib/util.cmx kernel/type_errors.cmi
kernel/typeops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \
kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
@@ -610,13 +588,13 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
- kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
- proofs/clenv.cmi
+ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi kernel/type_errors.cmi \
+ pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi
proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
- kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
- proofs/clenv.cmi
+ kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx kernel/type_errors.cmx \
+ pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi
proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \
@@ -646,13 +624,15 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \
library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \
kernel/generic.cmi library/global.cmi library/lib.cmi kernel/names.cmi \
- lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \
- kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi
+ lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \
+ proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+ proofs/pfedit.cmi
proofs/pfedit.cmx: parsing/astterm.cmx kernel/constant.cmx \
library/declare.cmx lib/edit.cmx kernel/environ.cmx kernel/evd.cmx \
kernel/generic.cmx library/global.cmx library/lib.cmx kernel/names.cmx \
- lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx proofs/tacmach.cmx \
- kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi
+ lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \
+ proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+ proofs/pfedit.cmi
proofs/proof_trees.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \
parsing/printer.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
@@ -666,13 +646,13 @@ proofs/proof_trees.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/environ.cmx \
proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi kernel/evd.cmi \
kernel/generic.cmi kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi \
parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
- kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi \
- proofs/refiner.cmi
+ kernel/sign.cmi lib/stamps.cmi kernel/term.cmi kernel/type_errors.cmi \
+ lib/util.cmi proofs/refiner.cmi
proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx kernel/evd.cmx \
kernel/generic.cmx kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx \
parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
- kernel/sign.cmx lib/stamps.cmx kernel/term.cmx lib/util.cmx \
- proofs/refiner.cmi
+ kernel/sign.cmx lib/stamps.cmx kernel/term.cmx kernel/type_errors.cmx \
+ lib/util.cmx proofs/refiner.cmi
proofs/tacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi proofs/macros.cmi \
kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
kernel/term.cmi lib/util.cmi proofs/tacinterp.cmi
@@ -699,7 +679,7 @@ tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
parsing/coqast.cmi library/declare.cmi tactics/dhyp.cmi kernel/evd.cmi \
kernel/generic.cmi library/global.cmi tactics/hiddentac.cmi \
kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
- library/library.cmi kernel/names.cmi tactics/pattern.cmi \
+ library/library.cmi kernel/names.cmi lib/options.cmi tactics/pattern.cmi \
proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \
proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
@@ -709,7 +689,7 @@ tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \
parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx kernel/evd.cmx \
kernel/generic.cmx library/global.cmx tactics/hiddentac.cmx \
kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
- library/library.cmx kernel/names.cmx tactics/pattern.cmx \
+ library/library.cmx kernel/names.cmx lib/options.cmx tactics/pattern.cmx \
proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \
proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
@@ -821,8 +801,6 @@ tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
tools/coqdep_lexer.cmo: config/coq_config.cmi
tools/coqdep_lexer.cmx: config/coq_config.cmx
-tools/gallina.cmo: tools/gallina_lexer.cmo
-tools/gallina.cmx: tools/gallina_lexer.cmx
toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
@@ -880,11 +858,11 @@ toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
kernel/typeops.cmx lib/util.cmx toplevel/discharge.cmi
toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/inductive.cmi \
- parsing/lexer.cmi lib/options.cmi lib/pp.cmi kernel/type_errors.cmi \
- lib/util.cmi toplevel/errors.cmi
+ parsing/lexer.cmi proofs/logic.cmi lib/options.cmi lib/pp.cmi \
+ kernel/type_errors.cmi lib/util.cmi toplevel/errors.cmi
toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/inductive.cmx \
- parsing/lexer.cmx lib/options.cmx lib/pp.cmx kernel/type_errors.cmx \
- lib/util.cmx toplevel/errors.cmi
+ parsing/lexer.cmx proofs/logic.cmx lib/options.cmx lib/pp.cmx \
+ kernel/type_errors.cmx lib/util.cmx toplevel/errors.cmi
toplevel/fhimsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi
@@ -892,15 +870,15 @@ toplevel/fhimsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi
toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi kernel/generic.cmi \
- kernel/inductive.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
- parsing/pretty.cmi parsing/printer.cmi kernel/reduction.cmi \
- kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi lib/util.cmi \
- toplevel/himsg.cmi
+ kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \
+ lib/pp.cmi parsing/pretty.cmi parsing/printer.cmi kernel/reduction.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi kernel/type_errors.cmi \
+ lib/util.cmi toplevel/himsg.cmi
toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx kernel/generic.cmx \
- kernel/inductive.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
- parsing/pretty.cmx parsing/printer.cmx kernel/reduction.cmx \
- kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx lib/util.cmx \
- toplevel/himsg.cmi
+ kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \
+ lib/pp.cmx parsing/pretty.cmx parsing/printer.cmx kernel/reduction.cmx \
+ kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx kernel/type_errors.cmx \
+ lib/util.cmx toplevel/himsg.cmi
toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \
library/lib.cmi library/libobject.cmi library/library.cmi \
diff --git a/dev/TODO b/dev/TODO
index c377eac2b..68f047426 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,4 +1,10 @@
+ o warning camlp4
+ <W> Changing associativity of level "<top>"
+ à comprendre et supprimmer
+ (on peut faire Grammar.warning_verbose := False, mais il vaut mieux
+ comprendre)
+
o options de la ligne de commande
- reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
diff --git a/dev/base_db b/dev/base_db
index c068b875c..d34ae6b68 100644
--- a/dev/base_db
+++ b/dev/base_db
@@ -1,3 +1,4 @@
+load_printer "gramlib.cma"
load_printer "top_printers.cmo"
install_printer Top_printers.prid
install_printer Top_printers.prsp
diff --git a/dev/changements.txt b/dev/changements.txt
index ab188cafb..da1b10255 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -21,6 +21,21 @@ Changements dans les types de données :
context -> typed_type signature
+ATTENTION:
+----------
+
+ Il y a maintenant d'autres exceptions que UserError (TypeError,
+ RefinerError, etc.)
+
+ Il ne faut donc plus se contenter (pour rattraper) de faire
+
+ try . .. with UserError _ -> ...
+
+ mais écrire à la place
+
+ try ... with e when Logic.catchable_exception e -> ...
+
+
Changements dans les fonctions :
--------------------------------
diff --git a/dev/db b/dev/db
index 2cb7bb5f3..77a995aa3 100644
--- a/dev/db
+++ b/dev/db
@@ -1,3 +1,4 @@
+load_printer "gramlib.cma"
load_printer "top_printers.cmo"
install_printer Top_printers.prid
install_printer Top_printers.prsp
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 3555a386a..0a44eff87 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -153,7 +153,7 @@ let unify_0 mc wc m n =
| _ -> error_cannot_unify CCI (m,n)
- with UserError _ as ex ->
+ with ex when catchable_exception ex ->
if (not(occur_meta cM)) & w_conv_x wc cM cN then
substn
else
@@ -250,7 +250,7 @@ and w_resrec metas evars wc =
else
(try
w_resrec metas t (w_Define evn rhs wc)
- with UserError _ ->
+ with ex when catchable_exception ex ->
(match rhs with
| DOPN(AppL,cl) ->
(match cl.(0) with
@@ -565,7 +565,7 @@ and clenv_resrec metas evars clenv =
else
(try
clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
- with UserError _ ->
+ with ex when catchable_exception ex ->
(match rhs with
| DOPN(AppL,cl) ->
(match cl.(0) with
@@ -675,18 +675,27 @@ let constrain_clenv_to_subterm clause = function
if closed0 cl
then clenv_unify op cl clause,cl
else error "Bound 1"
- with UserError _ ->
+ with ex when catchable_exception ex ->
(match telescope_appl cl with
| DOPN(AppL,tl) ->
if Array.length tl = 2 then
let c1 = tl.(0) and c2 = tl.(1) in
- (try matchrec c1 with UserError(_) -> matchrec c2)
+ (try
+ matchrec c1
+ with ex when catchable_exception ex ->
+ matchrec c2)
else
error "Match_subterm"
| DOP2(Prod,t,DLAM(_,c)) ->
- (try matchrec t with UserError(_) -> matchrec c)
+ (try
+ matchrec t
+ with ex when catchable_exception ex ->
+ matchrec c)
| DOP2(Lambda,t,DLAM(_,c)) ->
- (try matchrec t with UserError(_) -> matchrec c)
+ (try
+ matchrec t
+ with ex when catchable_exception ex ->
+ matchrec c)
| _ -> error "Match_subterm"))
in
matchrec cl
@@ -700,7 +709,7 @@ let constrain_clenv_using_subterm_list allow_K clause oplist t =
let (clause',cl) =
(try
constrain_clenv_to_subterm clause (strip_outer_cast op,t)
- with (UserError _ as e) ->
+ with e when catchable_exception e ->
if allow_K then (clause,op) else raise e)
in
(clause',cl::l)
@@ -919,7 +928,7 @@ and clenv_resrec metas evars clenv =
else
(try
clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
- with UserError _ ->
+ with ex when catchable_exception ex ->
(match rhs with
| DOPN(AppL,cl) ->
(match cl.(0) with
@@ -1023,19 +1032,19 @@ let clenv_unique_resolver allow_K clenv gls =
| ((DOP0(Meta _) as pathd,_),(DOP2(Lambda,_,_) as glhd,_)) ->
(try
clenv_typed_fo_resolver clenv gls
- with UserError (t1,t2) ->
+ with ex when catchable_exception ex ->
try
clenv_so_resolver allow_K clenv gls
- with UserError (s1,s2) ->
+ with ex when catchable_exception ex ->
error "Cannot solve a second-order unification problem")
| ((DOP0(Meta _),_),_) ->
(try
clenv_so_resolver allow_K clenv gls
- with UserError (t1,t2) ->
+ with ex when catchable_exception ex ->
try
clenv_typed_fo_resolver clenv gls
- with UserError (s1,s2) ->
+ with ex when catchable_exception ex ->
error "Cannot solve a second-order unification problem")
| _ -> clenv_fo_resolver clenv gls
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e43d51966..ec23d3258 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -115,7 +115,8 @@ let w_Underlying wc = (ts_it (ids_it wc)).decls
let w_type_of wc c = ctxt_type_of (ids_it wc) c
let w_env wc = get_env (ids_it wc)
let w_hyps wc = var_context (get_env (ids_it wc))
-let w_ORELSE wt1 wt2 wc = try wt1 wc with UserError _ -> wt2 wc
+let w_ORELSE wt1 wt2 wc =
+ try wt1 wc with e when catchable_exception e -> wt2 wc
let w_Declare sp c (wc:walking_constraints) =
begin match c with
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8a0432282..027ceab4a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,6 +13,7 @@ open Reduction
open Typing
open Proof_trees
open Typeops
+open Type_errors
open Coqast
open Declare
@@ -27,6 +28,13 @@ type refiner_error =
exception RefinerError of refiner_error
+let catchable_exception = function
+ | Util.UserError _ | TypeError _ | RefinerError _
+ | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _)) ->
+ true
+ | _ ->
+ false
+
let error_cannot_unify k (m,n) =
raise (RefinerError (CannotUnify (m,n)))
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 4d1c2de97..7df383a73 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -36,6 +36,8 @@ exception RefinerError of refiner_error
val error_cannot_unify : path_kind -> constr * constr -> 'a
+val catchable_exception : exn -> bool
+
(*s Pretty-printer. *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 4b3b797bf..137486bb4 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -60,7 +60,7 @@ let get_evmap_sign og =
try
let pftree = get_pftreestate () in
Some (nth_goal_of_pftreestate 1 pftree)
- with UserError _ ->
+ with e when Logic.catchable_exception e ->
None
in
match og with
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c1f3331d6..c4cab5b6b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -460,8 +460,7 @@ let tclNOTSAMEGOAL (tac:tactic) goal =
let tclORELSE0 t1 t2 g =
try
t1 g
- with UserError _ | TypeError _ | RefinerError _
- | Stdpp.Exc_located(_,(UserError _ | TypeError _ | RefinerError _)) ->
+ with e when catchable_exception e ->
t2 g
(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
@@ -907,7 +906,7 @@ let tclINFO (tac:tactic) gls =
mSGNL(hOV 0 [< 'sTR" == ";
print_subscript
((compose ts_it sig_sig) gls) sign pf >])
- with UserError _ ->
+ with e when catchable_exception e ->
mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >])
end;
res
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7e8d7678a..e0dec159b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -237,7 +237,7 @@ let make_resolve_hyp hname htyp =
[make_apply_entry (true, Options.is_verbose()) hname (mkVar hname, htyp)]
with
| Failure _ -> []
- | UserError _ -> anomaly "make_resolve_hyp"
+ | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
let add_resolves clist dbnames =
List.iter
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 5ff9a6294..dcc3a5f7b 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -178,7 +178,10 @@ let somatch metavars =
let somatches n pat =
let m = get_pat pat in
- try let _ = somatch None m n in true with UserError _ -> false
+ try
+ let _ = somatch None m n in true
+ with e when Logic.catchable_exception e ->
+ false
let dest_somatch n pat =
let m = get_pat pat in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bae9c8798..4755cc50e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -121,7 +121,10 @@ let clause_type cls gl =
let matches gls n pat =
let m = get_pat pat in
let (wc,_) = startWalk gls in
- try let _ = Clenv.unify_0 [] wc m n in true with UserError _ -> false
+ try
+ let _ = Clenv.unify_0 [] wc m n in true
+ with e when Logic.catchable_exception e ->
+ false
let dest_match gls n pat =
let m = get_pat pat in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5f4c73fea..8759e54a9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1675,7 +1675,7 @@ let abstract_subproof name tac gls =
by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro)
tac));
save_named true
- with UserError _ as e ->
+ with e when catchable_exception e ->
(abort_cur_goal(); raise e)
end;
exact (applist ((Declare.construct_reference env' CCI na),
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:27:24 +0000