1 files changed, 0 insertions, 74 deletions
diff --git a/man/gallina.1 b/man/gallina.1
deleted file mode 100644
index f8879c45..00000000
--- a/man/gallina.1
+++ /dev/null
@@ -1,74 +0,0 @@
-.TH COQ 1 "29 March 1995" "Coq tools"
-
-.SH NAME
-gallina \- extracts specification from Coq vernacular files
-
-.SH SYNOPSIS
-.B gallina
-[
-.BI \-
-]
-[
-.BI \-stdout
-]
-[
-.BI \-nocomments
-]
-.I file ...
-
-.SH DESCRIPTION
-
-.B gallina 
-takes Coq files as arguments and builds the corresponding
-specification files.
-The Coq file
-.IR foo.v \&
-gives bearth to the specification file
-.IR foo.g. \&
-The suffix '.g' stands for Gallina.
-
-For that purpose, gallina removes all commands that follow a
-"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it
-reaches a command "Abort.", "Qed.", "Defined." or "Proof
-<...>.". It also removes every "Hint", "Syntax",
-"Immediate"  or "Transparent" command.
-
-Files without the .v suffix are ignored.
-
-
-.SH OPTIONS
-
-.TP
-.BI \-stdout
-Prints the result on standard output.
-.TP
-.BI \-
-Coq source is taken on standard input. The result is printed on
-standard output.
-.TP
-.BI \-nocomments
-Comments are removed in the *.g file.
-
-.SH NOTES
-
-Nested comments are correctly handled. In particular, every command
-"Qed." or "Abort." in a comment is not taken into account.
-
-
-.SH BUGS
-
-Please report any bug to
-.B coq@pauillac.inria.fr
-
-
-
-
-
-
-	
-
-	
-
-	
-
-