From 410b3cc1cc0f677e052cfedcee03e14521264b64 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 17 May 2016 17:24:57 +0200 Subject: 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. --- pretyping/coercion.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/coercion.ml') 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 -> -- cgit v1.2.3