From 4f523e7d25ed22b6e41cabf1c2bd091afc0fde7f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 28 Nov 2011 16:10:46 +0000
Subject: Extraction: Richer patterns in matchs as proposed by P.N. Tollitte

 The MLcase has notably changed:
  - No more case_info in it, but only a type annotation
  - No more "one branch for one constructor", but rather a sequence
    of patterns. Earlier "full" pattern correspond to pattern Pusual.
    Patterns Pwild and Prel allow to encode optimized matchs without
    hacks as earlier. Other pattern situations aren't used (yet)
    by extraction, but only by P.N Tollitte's code.

 A MLtuple constructor has been introduced. It isn't used by
 the extraction for the moment, but only but P.N. Tollitte's code.

 Many pretty-print functions in ocaml.ml and other have been reorganized

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/extraction.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 8123726a16..3f8a3bc498 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -342,7 +342,7 @@ case H1.
 exact H0.
 intros.
 exact n.
-Qed.
+Defined.
 Extraction oups.
 (*
 let oups h0 =
-- 
cgit v1.2.3