diff options
| author | msozeau | 2007-06-09 16:02:11 +0000 |
|---|---|---|
| committer | msozeau | 2007-06-09 16:02:11 +0000 |
| commit | 5caebcd8ff2bedae02a23d79251a2344c7aea4d6 (patch) | |
| tree | f10f3e2fb94e16fb5fc6df04e03d79ff428b4bb1 /contrib/subtac/Utils.v | |
| parent | 481b6a29a87d04cfe54607702c83c9d35f371d75 (diff) | |
Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion code for
simultaneous coercion of different arguments of an inductive type. Add tactics for dealing
with heterogeneous equality. Export more error reporting functions from Cases.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9886 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/Utils.v')
| -rw-r--r-- | contrib/subtac/Utils.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index db30c497a1..137ac8c983 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -43,5 +43,6 @@ Extract Inductive prod => "pair" [ "" ]. Extract Inductive sigT => "pair" [ "" ]. Require Export ProofIrrelevance. +Require Export Coq.subtac.Heq. Delimit Scope program_scope with program. |