diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 70a41ddc..2e55b656 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id: pcoq.ml4 10987 2008-05-26 12:28:36Z herbelin $ i*) +(*i $Id: pcoq.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) open Pp open Util @@ -247,7 +247,7 @@ let get_entry (u, utab) s = Hashtbl.find utab s with Not_found -> errorlabstrm "Pcoq.get_entry" - (str "unknown grammar entry " ++ str u ++ str ":" ++ str s) + (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".") let new_entry etyp (u, utab) s = let ename = u ^ ":" ^ s in @@ -307,12 +307,12 @@ let get_generic_entry s = try object_of_typed_entry (Hashtbl.find utab s) with Not_found -> - error ("unknown grammar entry "^u^":"^s) + error ("Unknown grammar entry "^u^":"^s^".") let get_generic_entry_type (u,utab) s = try type_of_typed_entry (Hashtbl.find utab s) with Not_found -> - error ("unknown grammar entry "^u^":"^s) + error ("Unknown grammar entry "^u^":"^s^".") let force_entry_type (u, utab) s etyp = try @@ -578,7 +578,7 @@ let error_level_assoc p current expected = errorlabstrm "" (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative") + pr_assoc expected ++ str " associative.") let find_position_gen forpat ensure assoc lev = let ccurrent,pcurrent as current = List.hd !level_stack in @@ -628,13 +628,13 @@ let rec list_mem_assoc_triple x = function | [] -> false | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l -let register_empty_levels forpat symbs = - map_succeed (function - | Gramext.Snterml (_,n) when - let levels = (if forpat then snd else fst) (List.hd !level_stack) in - not (list_mem_assoc_triple (int_of_string n) levels) -> - find_position_gen forpat true None (Some (int_of_string n)) - | _ -> failwith "") symbs +let register_empty_levels forpat levels = + map_succeed (fun n -> + let levels = (if forpat then snd else fst) (List.hd !level_stack) in + if not (list_mem_assoc_triple n levels) then + find_position_gen forpat true None (Some n) + else + failwith "") levels let find_position forpat assoc level = find_position_gen forpat false assoc level @@ -695,7 +695,7 @@ let compute_entry allow_create adjust forpat = function | ETPattern -> weaken_entry Constr.pattern, None, false | ETOther ("constr","annot") -> weaken_entry Constr.annot, None, false - | ETConstrList _ -> error "List of entries cannot be registered" + | ETConstrList _ -> error "List of entries cannot be registered." | ETOther (u,n) -> let u = get_univ u in let e = @@ -762,6 +762,6 @@ let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> user_err_loc (loc, "coerce_reference_to_id", - str "This expression should be a simple identifier") + str "This expression should be a simple identifier.") let coerce_global_to_id = coerce_reference_to_id |