From ccff0b020b3a0950a6358846b6a40b8cd7a96562 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 18 Jul 2008 10:06:36 +0000 Subject: Modification rapide du message d'erreur lorsqu'un _ ne peut être effacé dans un intro-pattern (suggéré par ssreflect). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarutil.ml | 8 ++++---- pretyping/evarutil.mli | 8 ++++++-- 2 files changed, 10 insertions(+), 6 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3