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/coercion.ml | |
| 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/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index cba28f817..65d79bcc8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -192,7 +192,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let term = co x in Typing.e_solve_evars env evdref term) in - if isEvar c || isEvar c' then + if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) raise NoSubtacCoercion; aux [] typ typ' 0 (fun x -> x) @@ -280,7 +280,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let c1 = coerce_unify env a a' in let c2 = coerce_unify env b b' in match c1, c2 with - None, None -> None + | None, None -> None | _, _ -> Some (fun x -> |