(**************************************************************************) (* *) (* 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;;