diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/Utils.v | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 4ef4f3eced..102fa94ad4 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -12,8 +12,8 @@ Notation "( x & ? )" := (@exist _ _ x _) : core_scope. Notation " ! " := (False_rect _ _). -(* Logical if : keep a trace of the control flow in obligations. *) -Notation " 'lif' b 'then' e 'else' f " := (match b with true => e | false => f end) (at level 30). +Require Import Coq.Bool.Sumbool. +Notation "'dec'" := (sumbool_of_bool) (at level 0). Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. intros. diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 6086bd547b..17110c058c 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -2094,11 +2094,10 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let _, j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - let ty = tycon_constr in let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = ty; } + uj_type = out_some (valcon_of_tycon tycon0); } in j (* inh_conv_coerce_to_tycon loc env isevars j tycon0 *) else |