diff options
Diffstat (limited to 'parsing/g_primnew.ml4')
-rw-r--r-- | parsing/g_primnew.ml4 | 84 |
1 files changed, 0 insertions, 84 deletions
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4 deleted file mode 100644 index c1875634..00000000 --- a/parsing/g_primnew.ml4 +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: g_primnew.ml4,v 1.4.2.2 2004/07/16 19:30:39 herbelin Exp $ i*) - -open Coqast -open Pcoq -open Names -open Libnames -open Topconstr - -let _ = - if not !Options.v7 then - Pcoq.reset_all_grammars() -let _ = - if not !Options.v7 then - let f = Gram.Unsafe.clear_entry in - f Prim.bigint; - f Prim.qualid; - f Prim.ast; - f Prim.reference - -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"] -let _ = - if not !Options.v7 then - List.iter (fun s -> Lexer.add_token("",s)) prim_kw - -open Prim - -open Nametab -let local_id_of_string = id_of_string -let local_make_dirpath = make_dirpath -let local_make_qualid l id' = make_qualid (local_make_dirpath l) id' -let local_make_short_qualid id = make_short_qualid id -let local_make_posint = int_of_string -let local_make_negint n = - int_of_string n -let local_make_path l a = encode_kn (local_make_dirpath l) a -let local_make_binding loc a b = - match a with - | Nvar (_,id) -> Slam(loc,Some id,b) - | Nmeta (_,s) -> Smetalam(loc,s,b) - | _ -> failwith "Slam expects a var or a metavar" -let local_append l id = l@[id] - -if not !Options.v7 then -GEXTEND Gram - GLOBAL: bigint qualid reference ne_string; - field: - [ [ s = FIELD -> local_id_of_string s ] ] - ; - fields: - [ [ id = field; (l,id') = fields -> (local_append l id,id') - | id = field -> ([],id) - ] ] - ; - basequalid: - [ [ id = base_ident; (l,id')=fields -> - local_make_qualid (local_append l id) id' - | id = base_ident -> local_make_short_qualid id - ] ] - ; - reference: - [ [ id = base_ident; (l,id') = fields -> - Qualid (loc, local_make_qualid (local_append l id) id') - | id = base_ident -> Ident (loc,id) - ] ] - ; - qualid: - [ [ qid = basequalid -> loc, qid ] ] - ; - ne_string: - [ [ s = STRING -> - if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s - ] ] - ; - bigint: (* Negative numbers are dealt with specially *) - [ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ] - ; -END |