diff options
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 53 |
1 files changed, 28 insertions, 25 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index b90e06cd..b25ea766 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -1,15 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) -open Compat open Names open Libnames -open Tok (* necessary for camlp4 *) open Pcoq open Pcoq.Prim @@ -28,13 +28,13 @@ let my_int_of_string loc s = if n > 1024 * 2048 then raise Exit; n with Failure _ | Exit -> - CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") + CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring - ne_string string pattern_ident pattern_identref by_notation smart_global; + ne_string string lstring pattern_ident pattern_identref by_notation smart_global; preident: [ [ s = IDENT -> s ] ] ; @@ -45,13 +45,13 @@ GEXTEND Gram [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: - [ [ id = pattern_ident -> (!@loc, id) ] ] + [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ] ; var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> (!@loc, id) ] ] + [ [ id = ident -> CAst.make ~loc:!@loc id ] ] ; identref: - [ [ id = ident -> (!@loc, id) ] ] + [ [ id = ident -> CAst.make ~loc:!@loc id ] ] ; field: [ [ s = FIELD -> Id.of_string s ] ] @@ -62,8 +62,8 @@ GEXTEND Gram ] ] ; fullyqualid: - [ [ id = ident; (l,id')=fields -> !@loc,id::List.rev (id'::l) - | id = ident -> !@loc,[id] + [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l) + | id = ident -> CAst.make ~loc:!@loc [id] ] ] ; basequalid: @@ -72,32 +72,32 @@ GEXTEND Gram ] ] ; name: - [ [ IDENT "_" -> (!@loc, Anonymous) - | id = ident -> (!@loc, Name id) ] ] + [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous + | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ] ; reference: [ [ id = ident; (l,id') = fields -> - Qualid (!@loc, local_make_qualid (l@[id]) id') - | id = ident -> Ident (!@loc,id) + CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') + | id = ident -> CAst.make ~loc:!@loc @@ Ident id ] ] ; by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (!@loc, s, sc) ] ] + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ] ; smart_global: - [ [ c = reference -> Misctypes.AN c - | ntn = by_notation -> Misctypes.ByNotation ntn ] ] + [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c + | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ] ; qualid: - [ [ qid = basequalid -> !@loc, qid ] ] + [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] ; ne_string: [ [ s = STRING -> - if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s + if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s ] ] ; ne_lstring: - [ [ s = ne_string -> (!@loc, s) ] ] + [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ] ; dirpath: [ [ id = ident; l = LIST0 field -> @@ -106,6 +106,9 @@ GEXTEND Gram string: [ [ s = STRING -> s ] ] ; + lstring: + [ [ s = string -> (CAst.make ~loc:!@loc s) ] ] + ; integer: [ [ i = INT -> my_int_of_string (!@loc) i | "-"; i = INT -> - my_int_of_string (!@loc) i ] ] @@ -113,7 +116,7 @@ GEXTEND Gram natural: [ [ i = INT -> my_int_of_string (!@loc) i ] ] ; - bigint: (* Negative numbers are dealt with specially *) - [ [ i = INT -> (Bigint.of_string i) ] ] + bigint: (* Negative numbers are dealt with elsewhere *) + [ [ i = INT -> i ] ] ; END |