diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 4d333c30d..c8e0d1637 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -57,7 +57,7 @@ let rec complete_conclusion a cs = function | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then - user_err ~loc "" + user_err ~loc (strbrk"Cannot infer the non constant arguments of the conclusion of " ++ pr_id cs ++ str "."); let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in @@ -330,7 +330,7 @@ let do_assumptions kind nl l = match l with | (Discharge, _, _) when Lib.sections_are_opened () -> let loc = fst id in let msg = Pp.str "Section variables cannot be polymorphic." in - user_err ~loc "" msg + user_err ~loc msg | _ -> () in do_assumptions_bound_univs coe kind nl id (Some pl) c @@ -342,7 +342,7 @@ let do_assumptions kind nl l = match l with let loc = fst id in let msg = Pp.str "Assumptions with bound universes can only be defined one at a time." in - user_err ~loc "" msg + user_err ~loc msg in (coe, (List.map map idl, c)) in @@ -438,7 +438,7 @@ let interp_ind_arity env evdref ind = let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in let pseudo_poly = check_anonymous_type c in let () = if not (Reduction.is_arity env t) then - user_err ~loc:(constr_loc ind.ind_arity) "" (str "Not an arity") + user_err ~loc:(constr_loc ind.ind_arity) (str "Not an arity") in t, pseudo_poly, impls @@ -553,7 +553,7 @@ let check_named (loc, na) = match na with | Name _ -> () | Anonymous -> let msg = str "Parameters must be named." in - user_err ~loc "" msg + user_err ~loc msg let check_param = function @@ -955,7 +955,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let relargty = let error () = user_err ~loc:(constr_loc r) - "Command.build_wellfounded" + ~hdr:"Command.build_wellfounded" (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try @@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l = match n with | Some n -> mkIdentC (snd n) | None -> - user_err "do_program_fixpoint" + user_err ~hdr:"do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn @@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l = do_program_recursive local poly fixkind fixl ntns | _, _ -> - user_err "do_program_fixpoint" + user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let check_safe () = |