From 999ac2c4c2bb6c7397c88ee1b6f39bdb43eaecb1 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 27 Mar 2009 16:13:00 +0000
Subject: Remove unused mli files

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

(limited to 'parsing')

diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
deleted file mode 100644
index 5b4db848ef..0000000000
--- a/parsing/g_minicoq.mli
+++ /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        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Pp
-open Names
-open Term
-open Environ
-(*i*)
-
-val term : constr Grammar.Entry.e
-
-type command =
-  | Definition of identifier * constr option * constr
-  | Parameter of identifier * constr
-  | Variable of identifier * constr
-  | Inductive of 
-      (identifier * constr) list *
-      (identifier * constr * (identifier * constr) list) list
-  | Check of constr
-
-val command : command Grammar.Entry.e
-
-val pr_term : path_kind -> env -> constr -> std_ppcmds
-- 
cgit v1.2.3