diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 8 |
2 files changed, 10 insertions, 6 deletions
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 |