diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 10:39:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 10:40:19 +0200 |
| commit | f6382ef326099651cd051aa907b4e9ac6c905698 (patch) | |
| tree | c97ae7af493e2fcefce8b1c781f292d7d4906f40 | |
| parent | f2a4ad8b7ca2407d3dd2b6f38b70f635bd6ad0ed (diff) | |
Add an Unset Standard...
| -rw-r--r-- | test-suite/bugs/closed/2378.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index ab39633f8..35c69db2f 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -503,6 +503,9 @@ Qed. Require Export Coq.Logic.FunctionalExtensionality. Print PLanguage. + +Unset Standard Proposition Elimination Names. + Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): Transformation (PLanguage l1) (PLanguage l2) := mkTransformation (PLanguage l1) (PLanguage l2) |