diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-16 12:34:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-24 13:11:59 +0200 |
| commit | 38fbc6e523bb45aa18761dbb027bc1ae479632cd (patch) | |
| tree | 7561cabb1146c0ff65a4706f4dfdba96d83ebb2a /engine/evarutil.mli | |
| parent | 5c34cfa54ec1959758baa3dd283e2e30853380db (diff) | |
Improving error message for clear tactic (and indirect uses of it).
- Be more precise when trying to clear an hypothesis which
occurs implicitly in a global constant.
- Warns if destruct/induction cannot clear an hypothesis occurring
implicitly in a global.
In the first case, the change in situation
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a.
is:
- before: "a is used in conclusion"
- after: "a is used implicitly in b in conclusion"
In the second case:
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a.
produces a warning: "Cannot remove a, it is used implicitly in b".
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 40c1ee082..831a7f26b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -224,7 +224,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 |