aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml2
-rw-r--r--interp/genarg.ml4
-rw-r--r--interp/genarg.mli2
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/q_coqast.ml410
-rw-r--r--pretyping/evarutil.ml8
-rw-r--r--pretyping/evarutil.mli8
-rw-r--r--proofs/tacmach.ml13
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tacinterp.ml10
-rw-r--r--tactics/tactics.ml29
11 files changed, 60 insertions, 30 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8b805cc26..2e4ff80bb 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -625,7 +625,7 @@ let rec xlate_intro_pattern =
(fun l ->
CT_intro_patt_list(List.map xlate_intro_pattern l))
ll)
- | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
+ | IntroWildcard _ -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
| IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
| IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
| IntroFresh _ -> xlate_error "TODO: IntroFresh"
diff --git a/interp/genarg.ml b/interp/genarg.ml
index ac45bfe8d..b371582a1 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -76,7 +76,7 @@ let exists_argtype s = List.mem s !dyntab
type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
- | IntroWildcard
+ | IntroWildcard of loc
| IntroIdentifier of identifier
| IntroAnonymous
| IntroRewrite of bool
@@ -85,7 +85,7 @@ and case_intro_pattern_expr = intro_pattern_expr list list
let rec pr_intro_pattern = function
| IntroOrAndPattern pll -> pr_case_intro_pattern pll
- | IntroWildcard -> str "_"
+ | IntroWildcard _ -> str "_"
| IntroIdentifier id -> pr_id id
| IntroAnonymous -> str "?"
| IntroRewrite true -> str "->"
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 977308218..da0371899 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -33,7 +33,7 @@ type 'a with_ebindings = 'a * open_constr bindings
type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
- | IntroWildcard
+ | IntroWildcard of loc
| IntroIdentifier of identifier
| IntroAnonymous
| IntroRewrite of bool
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a1fd1649e..092dc9f88 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -251,7 +251,7 @@ GEXTEND Gram
| ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
| t::q -> IntroOrAndPattern [[t;pairify q]]
in pairify (si::tc)
- | "_" -> IntroWildcard
+ | "_" -> IntroWildcard loc
| prefix = pattern_ident -> IntroFresh prefix
| "?" -> IntroAnonymous
| id = ident -> IntroIdentifier id
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6bd795ed5..66a74ad16 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -62,12 +62,16 @@ let mlexpr_of_reference = function
| Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
| Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
+let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
+
+let mlexpr_of_loc loc = <:expr< $dloc$ >>
+
let mlexpr_of_by_notation f = function
| Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
| Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
let mlexpr_of_intro_pattern = function
- | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
+ | Genarg.IntroWildcard loc -> <:expr< Genarg.IntroWildcard $mlexpr_of_loc loc$ >>
| Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
| Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
| Genarg.IntroIdentifier id ->
@@ -85,10 +89,6 @@ let mlexpr_of_quantified_hypothesis = function
| Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >>
| Rawterm.NamedHyp id -> <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >>
-let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
-
-let mlexpr_of_loc loc = <:expr< $dloc$ >>
-
let mlexpr_of_or_var f = function
| Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >>
| Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2f2665bbc..f0c020908 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -437,12 +437,14 @@ let rec check_and_clear_in_constr evdref c ids hist =
| _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids hist) c
+exception OccurHypInSimpleClause of identifier * identifier option
+
let clear_hyps_in_evi evdref hyps concl ids =
(* clear_evar_hyps erases hypotheses ids in hyps, checking if some
hypothesis does not depend on a element of ids, and erases ids in
the contexts of the evars occuring in evi *)
let nconcl = try check_and_clear_in_constr evdref concl ids EvkSet.empty
- with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
+ with Dependency_error id' -> raise (OccurHypInSimpleClause (id',None)) in
let (nhyps,_) =
let check_context (id,ob,c) =
try
@@ -451,9 +453,7 @@ let clear_hyps_in_evi evdref hyps concl ids =
None -> None
| Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)),
check_and_clear_in_constr evdref c ids EvkSet.empty)
- with Dependency_error id' ->
- errorlabstrm "" (pr_id id' ++ strbrk " is used in hypothesis "
- ++ pr_id id ++ str ".")
+ with Dependency_error id' -> raise (OccurHypInSimpleClause (id',Some id))
in
let check_value vk =
match !vk with
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 27e964b6a..c48c97910 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -172,7 +172,11 @@ val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
-(**********************************)
-(* Removing hyps in evars'context *)
+(*********************************************************************)
+(* Removing hyps in evars'context; *)
+(* raise OccurHypInSimpleClause if the removal breaks dependencies *)
+
+exception OccurHypInSimpleClause of identifier * identifier option
+
val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
identifier list -> named_context_val * types
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7fd7aabe4..8e3e48d4f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -8,6 +8,7 @@
(* $Id$ *)
+open Pp
open Util
open Names
open Nameops
@@ -226,11 +227,21 @@ let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
let refine c = with_check (refine_no_check c)
let convert_concl d sty = with_check (convert_concl_no_check d sty)
let convert_hyp d = with_check (convert_hyp_no_check d)
-let thin l = with_check (thin_no_check l)
let thin_body c = with_check (thin_body_no_check c)
let move_hyp b id id' = with_check (move_hyp_no_check b id id')
let rename_hyp l = with_check (rename_hyp_no_check l)
+let thin l gl =
+ try with_check (thin_no_check l) gl
+ with Evarutil.OccurHypInSimpleClause (id,ido) ->
+ match ido with
+ | None ->
+ errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
+ | Some id' ->
+ errorlabstrm ""
+ (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str ".")
+
+
(* Pretty-printers *)
open Pp
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6edc723cf..4e06fffb7 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -376,7 +376,7 @@ let rewrite_equations_gene othin neqns ba gl =
Some thin: the equations are rewritten, and cleared if thin is true *)
let rec get_names allow_conj = function
- | IntroWildcard ->
+ | IntroWildcard _ ->
error "Discarding pattern not allowed for inversion equations."
| IntroAnonymous ->
error "Anonymous pattern not allowed for inversion equations."
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f81f15d89..1af19868a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -98,7 +98,9 @@ let catch_error loc tac g =
try tac g
with e when loc <> dummy_loc ->
match e with
- | Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e))
+ | Stdpp.Exc_located (loc',e') ->
+ if loc' = dummy_loc then raise (Stdpp.Exc_located (loc,e'))
+ else raise e
| e -> raise (Stdpp.Exc_located (loc,e))
(* Signature for interpretation: val_interp and interpretation functions *)
@@ -488,7 +490,7 @@ let rec intern_intro_pattern lf ist = function
IntroOrAndPattern (intern_case_intro_pattern lf ist l)
| IntroIdentifier id ->
IntroIdentifier (intern_ident lf ist id)
- | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
+ | IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
and intern_case_intro_pattern lf ist =
List.map (List.map (intern_intro_pattern lf ist))
@@ -1364,7 +1366,7 @@ let rec intropattern_ids = function
| IntroIdentifier id -> [id]
| IntroOrAndPattern ll ->
List.flatten (List.map intropattern_ids (List.flatten ll))
- | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
+ | IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
let rec extract_ids ids = function
| (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
@@ -1638,7 +1640,7 @@ let rec interp_message_nl ist = function
let rec interp_intro_pattern ist gl = function
| IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l)
| IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id
- | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
+ | IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
and interp_case_intro_pattern ist gl =
List.map (List.map (interp_intro_pattern ist gl))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1fdd4c16f..8c84b40d1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -882,11 +882,24 @@ let (assumption : tactic) = fun gl ->
* subsequently used in other hypotheses or in the conclusion of the
* goal. *)
-let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *)
- if ids=[] then tclIDTAC gl else with_check (thin ids) gl
+let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
+ if ids=[] then tclIDTAC else thin ids
let clear_body = thin_body
+let clear_wildcards ids =
+ tclMAP (fun (loc,id) gl ->
+ try with_check (Tacmach.thin_no_check [id]) gl
+ with OccurHypInSimpleClause (id,ido) ->
+ (* Intercept standard [thin] error message *)
+ match ido with
+ | None ->
+ user_err_loc (loc,"",str "_ is used in conclusion.")
+ | Some id ->
+ user_err_loc
+ (loc,"",str "_ is used in hypothesis " ++ pr_id id ++ str "."))
+ ids
+
(* Takes a list of booleans, and introduces all the variables
* quantified in the goal which are associated with a value
* true in the boolean list. *)
@@ -1056,7 +1069,7 @@ let clear_if_atomic l2r id gl =
let rec explicit_intro_names = function
| IntroIdentifier id :: l ->
id :: explicit_intro_names l
-| (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) :: l ->
+| (IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _) :: l ->
explicit_intro_names l
| IntroOrAndPattern ll :: l' ->
List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
@@ -1068,13 +1081,13 @@ let rec explicit_intro_names = function
dependency order (see bug #1000); we use fresh names, not used in
the tactic, for the hyps to clear *)
let rec intros_patterns avoid thin destopt = function
- | IntroWildcard :: l ->
+ | IntroWildcard loc :: l ->
tclTHEN
(intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true)
(onLastHyp (fun id ->
tclORELSE
(tclTHEN (clear [id]) (intros_patterns avoid thin destopt l))
- (intros_patterns avoid (id::thin) destopt l)))
+ (intros_patterns avoid ((loc,id)::thin) destopt l)))
| IntroIdentifier id :: l ->
tclTHEN
(intro_gen (IntroMustBe id) destopt true)
@@ -1100,7 +1113,7 @@ let rec intros_patterns avoid thin destopt = function
allClauses;
clear_if_atomic l2r id;
intros_patterns avoid thin destopt l ]))
- | [] -> clear thin
+ | [] -> clear_wildcards thin
let intros_pattern = intros_patterns [] []
@@ -1122,7 +1135,7 @@ let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid)
let prepare_intros s ipat gl = match ipat with
| IntroAnonymous -> make_id s gl, tclIDTAC
| IntroFresh id -> fresh_id [] id gl, tclIDTAC
- | IntroWildcard -> let id = make_id s gl in id, thin [id]
+ | IntroWildcard loc -> let id = make_id s gl in id, clear_wildcards [loc,id]
| IntroIdentifier id -> id, tclIDTAC
| IntroRewrite l2r ->
let id = make_id s gl in
@@ -1456,7 +1469,7 @@ let rec first_name_buggy = function
| IntroOrAndPattern [] -> None
| IntroOrAndPattern ([]::l) -> first_name_buggy (IntroOrAndPattern l)
| IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
- | IntroWildcard -> None
+ | IntroWildcard _ -> None
| IntroRewrite _ -> None
| IntroIdentifier id -> Some id
| IntroAnonymous | IntroFresh _ -> assert false
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 16:58:37 +0000