From b9e27721e88872a93ec7ca91575304ce1496a0ef Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 16 Feb 2007 19:17:27 +0000
Subject: 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
---
 contrib/subtac/Utils.v         | 4 ++--
 contrib/subtac/subtac_cases.ml | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'contrib')

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
-- 
cgit v1.2.3