diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-25 17:13:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-25 17:13:13 +0200 |
| commit | 6d4d16eb5518a9fb461e0f0433c9ce54d2197158 (patch) | |
| tree | ee9249b420e41ff864da77b65ba0ee467d983306 /engine | |
| parent | c97a4b7bb4af07c22137e0933d041d1f7eea95f1 (diff) | |
| parent | 38fbc6e523bb45aa18761dbb027bc1ae479632cd (diff) | |
Merge PR #6866: Slight improvement of messages related to direct and indirect uses of tactic `clear`.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 10 | ||||
| -rw-r--r-- | engine/evarutil.mli | 2 |
2 files changed, 6 insertions, 6 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6a8f8fb1d..710491f84 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -534,7 +534,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option exception Depends of Id.t @@ -545,13 +545,13 @@ let rec check_and_clear_in_constr env evdref err ids global c = is a section variable *) match kind c with | Var id' -> - if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c + if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c | ( Const _ | Ind _ | Construct _ ) -> let () = if global then let check id' = if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err)) + raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) in Id.Set.iter check (Environ.vars_of_global env c) in @@ -599,8 +599,8 @@ let rec check_and_clear_in_constr env evdref err ids global c = let global = Id.Set.exists is_section_variable nids in let concl = EConstr.Unsafe.to_constr (evar_concl evi) in check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl - with ClearDependencyError (rid,err) -> - raise (ClearDependencyError (Id.Map.find rid rids,err)) in + with ClearDependencyError (rid,err,where) -> + raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in if Id.Map.is_empty rids then c else diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c3de488c6..d3937f28e 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -232,7 +232,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types |