diff options
| -rw-r--r-- | test-suite/success/CasesDep.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 07c9dbf242..0256280cea 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -391,3 +391,15 @@ end. (* ------------------------------------------------------------------ *) End Sig. + +(* Exemple soumis par Bruno *) + +Definition bProp [b:bool] : Prop := + if b then True else False. + +Definition f0 [F:False;ty:bool]: (bProp ty) := + <[_:bool][ty:bool](bProp ty)>Cases ty ty of + true true => I + | _ false => F + | _ true => I + end. |