From daee2d3b0fa0d76dc06382221b53ea76d6ad2b32 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 4 Apr 2001 13:53:40 +0000
Subject: implification de extract_constr et extract_term

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1545 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extraction.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'contrib/extraction/extraction.mli')

diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 100028f14..0f08f3128 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -30,7 +30,6 @@ type extraction_context = bool list
 type extraction_result =
   | Emltype of ml_type * signature * identifier list
   | Emlterm of ml_ast
-  | Eprop
 
 (*s Extraction functions. *)
 
-- 
cgit v1.2.3