From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 tools/gallina_lexer.mll | 126 ------------------------------------------------
 1 file changed, 126 deletions(-)
 delete mode 100644 tools/gallina_lexer.mll

(limited to 'tools/gallina_lexer.mll')

diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
deleted file mode 100644
index 1a594aeb..00000000
--- a/tools/gallina_lexer.mll
+++ /dev/null
@@ -1,126 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-{
-
- let chan_out = ref stdout
-
- let comment_depth = ref 0
- let cRcpt = ref 0
- let comments = ref true
- let print s = output_string !chan_out s
-
- exception Fin_fichier
-
-}
-
-let space = [' ' '\t' '\n' '\r']
-let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
-
-rule action = parse
-  | "Theorem" space { print "Theorem "; body lexbuf;
-  	              cRcpt := 1; action lexbuf }
-  | "Lemma" space   { print "Lemma ";   body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Fact" space    { print "Fact ";   body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Remark" space  { print "Remark ";  body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Goal" space    { print "Goal ";    body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Correctness" space { print "Correctness "; body_pgm lexbuf;
-      	       	          cRcpt := 1; action lexbuf }
-  | "Definition" space  { print "Definition "; body_def lexbuf;
-			  cRcpt := 1; action lexbuf }
-  | "Hint" space        { skip_until_point lexbuf ; action lexbuf }
-  | "Hints" space        { skip_until_point lexbuf ; action lexbuf }
-  | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
-  | "Immediate"	space   { skip_until_point lexbuf ; action lexbuf }
-  | "Syntax" space      { skip_until_point lexbuf ; action lexbuf }
-  | "(*"      { (if !comments then print "(*");
-		comment_depth := 1;
-      	        comment lexbuf;
-		cRcpt := 0; action lexbuf }
-  | [' ' '\t']* '\n'      { if !cRcpt < 2 then print "\n";
-      	       	       	    cRcpt := !cRcpt+1; action lexbuf}
-  | eof       { (raise Fin_fichier : unit)}
-  | _         { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
-
-and comment = parse
-  | "(*"  { (if !comments then print "(*");
-      	    comment_depth := succ !comment_depth; comment lexbuf }
-  | "*)"  { (if !comments then print "*)");
-      	    comment_depth := pred !comment_depth;
-            if !comment_depth > 0 then comment lexbuf }
-  | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf));
-      			  comment_depth := pred !comment_depth;
-			  if !comment_depth > 0 then comment lexbuf }
-  | eof   { raise Fin_fichier }
-  | _     { (if !comments then print (Lexing.lexeme lexbuf));
-	    comment lexbuf }
-
-and skip_comment = parse
-  | "(*"  { comment_depth := succ !comment_depth; skip_comment lexbuf }
-  | "*)"  { comment_depth := pred !comment_depth;
-            if !comment_depth > 0 then skip_comment lexbuf }
-  | eof   { raise Fin_fichier }
-  | _     { skip_comment lexbuf }
-
-and body_def = parse
-  | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () }
-  | _            { print (Lexing.lexeme lexbuf); body lexbuf }
-
-and body = parse
-  | enddot { print ".\n"; skip_proof lexbuf }
-  | ":="   { print ".\n"; skip_proof lexbuf }
-  | "(*"   { print "(*"; comment_depth := 1;
-      	     comment lexbuf; body lexbuf }
-  | eof    { raise Fin_fichier }
-  | _      { print (Lexing.lexeme lexbuf); body lexbuf }
-
-and body_pgm = parse
-  | enddot { print ".\n"; skip_proof lexbuf }
-  | "(*"   { print "(*"; comment_depth := 1;
-      	     comment lexbuf; body_pgm lexbuf }
-  | eof    { raise Fin_fichier }
-  | _      { print (Lexing.lexeme lexbuf); body_pgm lexbuf }
-
-and skip_until_point = parse
-  | '.' '\n' { () }
-  | enddot   { end_of_line lexbuf }
-  | "(*"     { comment_depth := 1;
-      	       skip_comment lexbuf; skip_until_point lexbuf }
-  | eof      { raise Fin_fichier }
-  | _        { skip_until_point lexbuf }
-
-and end_of_line = parse
-  | [' ' '\t' ]*	{ end_of_line lexbuf }
-  | '\n'		{ () }
-  | eof   	     	{ raise Fin_fichier }
-  | _	  		{ print (Lexing.lexeme lexbuf) }
-
-and skip_proof = parse
-  | "Save" space
-                { skip_until_point lexbuf }
-  | "Qed."  	{ end_of_line lexbuf }
-  | "Qed" space
-                { skip_until_point lexbuf }
-  | "Defined."  { end_of_line lexbuf }
-  | "Defined" space
-                { skip_until_point lexbuf }
-  | "Abort." 	{ end_of_line lexbuf }
-  | "Abort" space
-                { skip_until_point lexbuf }
-  | "Proof" space   { skip_until_point lexbuf }
-  | "Proof" [' ' '\t']* '.'  { skip_proof lexbuf }
-  | "(*"    { comment_depth := 1;
-      	      skip_comment lexbuf; skip_proof lexbuf }
-  | eof     { raise Fin_fichier }
-  | _       { skip_proof lexbuf }
-- 
cgit v1.2.3