diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-07-15 18:52:18 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-07-15 18:52:18 +0200 |
| commit | 9b80b60bbf8bc7ec0ce8985b66399a179126882d (patch) | |
| tree | 5e5fcf64b916317425226edf2456dfed5ffd8c5e /3rdparty/alt-ergo/smtlib2_util.ml | |
| parent | c2f860da64b15ef094d2905330e74658934f9cc2 (diff) | |
| download | smtcoq-9b80b60bbf8bc7ec0ce8985b66399a179126882d.tar.gz smtcoq-9b80b60bbf8bc7ec0ce8985b66399a179126882d.zip | |
3rdparty
Diffstat (limited to '3rdparty/alt-ergo/smtlib2_util.ml')
| -rw-r--r-- | 3rdparty/alt-ergo/smtlib2_util.ml | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/3rdparty/alt-ergo/smtlib2_util.ml b/3rdparty/alt-ergo/smtlib2_util.ml new file mode 100644 index 0000000..d503145 --- /dev/null +++ b/3rdparty/alt-ergo/smtlib2_util.ml @@ -0,0 +1,30 @@ +(**************************************************************************) +(* *) +(* 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;; |