From f6382ef326099651cd051aa907b4e9ac6c905698 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Jun 2014 10:39:56 +0200 Subject: Add an Unset Standard... --- test-suite/bugs/closed/2378.v | 3 +++ 1 file changed, 3 insertions(+) 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) -- cgit v1.2.3