diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 12 | ||||
| -rw-r--r-- | interp/topconstr.ml | 2 |
3 files changed, 10 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c7078cf2a0..4dcf287efc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -579,7 +579,7 @@ let rec subordinate_letins letins = function let terms_of_binders bl = let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) - | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term." + | PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | PatCstr (c,l,_) -> let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in @@ -589,7 +589,7 @@ let terms_of_binders bl = | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l | {loc; v = GLocalDef (Anonymous,_,_,_)}::l - | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> error "Cannot turn \"_\" into a term." + | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> user_err Pp.(str "Cannot turn \"_\" into a term.") | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l | [] -> [] in extract_variables bl @@ -1862,7 +1862,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let eargs, rargs = extract_explicit_arg l args in if !parsing_explicit then if Id.Map.is_empty eargs then intern_args env subscopes rargs - else error "Arguments given by name or position not supported in explicit mode." + else user_err Pp.(str "Arguments given by name or position not supported in explicit mode.") else let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 74644b206a..6f91009111 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -42,7 +42,7 @@ let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ | _,(GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> error "Unsupported construction in recursive notations." + -> user_err Pp.(str "Unsupported construction in recursive notations.") | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ | GHole _ | GSort _ | GLetIn _), _ -> false @@ -112,7 +112,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with (* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function - | Anonymous -> CErrors.error "This expression should be a simple identifier." + | Anonymous -> CErrors.user_err Pp.(str "This expression should be a simple identifier.") | Name id -> id let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na @@ -377,7 +377,7 @@ let notation_constr_and_vars_of_glob_constr a = Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk != Explicit then - error "Binders marked as implicit not allowed in notations."; + user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) @@ -387,7 +387,7 @@ let notation_constr_and_vars_of_glob_constr a = NHole (w, naming, arg) | GRef (r,_) -> NRef r | GEvar _ | GPatVar _ -> - error "Existential variables not allowed in notations." + user_err Pp.(str "Existential variables not allowed in notations.") ) x in let t = aux a in @@ -415,9 +415,9 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = Id.List.mem_assoc_sym x foundrec || Id.List.mem_assoc_sym x foundrecbinding then - error + user_err Pp.(str (Id.to_string x ^ - " should not be bound in a recursive pattern of the right-hand side.") + " should not be bound in a recursive pattern of the right-hand side.")) else injective := false in let check_pair s x y where = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1fe63c19c4..a79f10df6b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -163,7 +163,7 @@ let split_at_annot bl na = match na with | None -> begin match names with - | [] -> error "A fixpoint needs at least one parameter." + | [] -> user_err (Pp.str "A fixpoint needs at least one parameter.") | _ -> ([], bl) end | Some (loc, id) -> |