diff options
Diffstat (limited to 'src/smtlib2/smtlib2_util.ml')
| -rw-r--r-- | src/smtlib2/smtlib2_util.ml | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/src/smtlib2/smtlib2_util.ml b/src/smtlib2/smtlib2_util.ml deleted file mode 100644 index d503145..0000000 --- a/src/smtlib2/smtlib2_util.ml +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq, originally belong to The Alt-ergo theorem prover *) -(* Copyright (C) 2006-2010 *) -(* *) -(* Sylvain Conchon *) -(* Evelyne Contejean *) -(* Stephane Lescuyer *) -(* Mohamed Iguernelala *) -(* Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -(* auto-generated by gt *) - -(* no extra data from grammar file. *) -type extradata = unit;; -let initial_data() = ();; - -let file = ref "stdin";; -let line = ref 1;; -type pos = int;; -let string_of_pos p = "line "^(string_of_int p);; -let cur_pd() = (!line, initial_data());; (* "pd": pos + extradata *) -type pd = pos * extradata;; |