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/evarutil.mli | |
| 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/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 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 |