diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
commit | 4c3301517cf8887b3684fda58e2e4626a072a5fb (patch) | |
tree | bd1ed746e255a9f25b486711163001b2f45d8017 /theories/Program/Subset.v | |
parent | a8b034513e0c03ceb7e154949b15f62ac6862f3b (diff) |
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
Diffstat (limited to 'theories/Program/Subset.v')
-rw-r--r-- | theories/Program/Subset.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index c9de1a9e1..d021326a1 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. *) |