diff options
| author | msozeau | 2007-02-16 19:17:27 +0000 |
|---|---|---|
| committer | msozeau | 2007-02-16 19:17:27 +0000 |
| commit | b9e27721e88872a93ec7ca91575304ce1496a0ef (patch) | |
| tree | 355b6e71179b8ace71691c22033874f6e7b6cae9 /contrib | |
| parent | 481494be9f20d9c497e4d7ac108ae19bbaa53201 (diff) | |
Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |