From e1feff1215562d8f99fedf73c87011e6d7edca19 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 19 May 2010 15:29:32 +0000
Subject: Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a
 naive way

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/refutpat.ml4 | 31 -------------------------------
 1 file changed, 31 deletions(-)
 delete mode 100644 lib/refutpat.ml4

(limited to 'lib')

diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
deleted file mode 100644
index ef28019416..0000000000
--- a/lib/refutpat.ml4
+++ /dev/null
@@ -1,31 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pcaml
-
-(** * Non-irrefutable patterns
-
-    This small camlp4 extension creates a "let*" variant of the "let"
-    syntax that allow the use of a non-exhaustive pattern. The typical
-    usage is:
-
-      let* x::l = foo in ...
-
-    when foo is already known to be non-empty. This way, no warnings by ocamlc.
-    A Failure is raised if the pattern doesn't match the expression.
-*)
-
-
-EXTEND
- expr:
-   [[ "let"; "*"; p = patt; "="; e1 = expr; "in"; e2 = expr ->
-       <:expr< match $e1$ with
-	        [ $p$ -> $e2$
-                | _ -> failwith "Refutable pattern failed"
-                ] >> ]];
-END
-- 
cgit v1.2.3