diff options
Diffstat (limited to 'src/verit/smtlib2_util.ml')
| -rw-r--r-- | src/verit/smtlib2_util.ml | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/verit/smtlib2_util.ml b/src/verit/smtlib2_util.ml new file mode 100644 index 0000000..1ce5e46 --- /dev/null +++ b/src/verit/smtlib2_util.ml @@ -0,0 +1,29 @@ +(**************************************************************************) +(* *) +(* 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;; |