diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-17 17:24:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-29 12:16:29 +0200 |
| commit | 410b3cc1cc0f677e052cfedcee03e14521264b64 (patch) | |
| tree | b092df75c1313b6a149366ff9015134547774283 /pretyping/cases.mli | |
| parent | 5e979cf6020eea9fa0feaa77c7436a29443e35db (diff) | |
Program: cleanup in cases, add options
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d7fff8af4..ba566f374 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -121,4 +121,3 @@ val prepare_predicate : Loc.t -> Context.Rel.t list -> Constr.constr option -> 'a option -> (Evd.evar_map * Names.name list * Term.constr) list - |