From 4c3301517cf8887b3684fda58e2e4626a072a5fb Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 15 May 2008 12:51:59 +0000
Subject: Various fixes: - Fix a typo in lowercase_utf8 - Fix generation of
 signatures in subtac_cases not working for dependent inductive types with
 dependent indices. - Fix coercion of inductive types generating ill-typed
 terms. - Fix test script using new syntax for Instances. - Move simpl_existTs
 to Program.Equality and use it in simpl_depind.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Subset.v | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'theories/Program/Subset.v')

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c9de1a9e17..d021326a10 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -13,16 +13,6 @@ Open Local Scope program_scope.
 
 (** Tactics related to subsets and proof irrelevance. *)
 
-(** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
-
-Ltac simpl_existT :=
-  match goal with
-    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
-    let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
-  end.
-
-Ltac simpl_existTs := repeat simpl_existT.
-
 (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to 
    factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
 
-- 
cgit v1.2.3