diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-31 12:30:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-02 20:06:05 -0400 |
| commit | 6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch) | |
| tree | 7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 | |
| parent | 42d510ceea82d617ac4e630049d690acbe900688 (diff) | |
Drop '.' from CErrors.anomaly, insert it in args
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
127 files changed, 387 insertions, 386 deletions
diff --git a/checker/check.ml b/checker/check.ml index 6d93c11ea..b3b403425 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -165,7 +165,7 @@ let find_logical_path phys_dir = match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir | _,[] -> default_root_prefix - | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir)) + | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^".")) let remove_load_path dir = let physical, logical = !load_paths in @@ -197,7 +197,7 @@ let add_load_path (phys_path,coq_path) = end | _,[] -> load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) - | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path)) + | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^".")) let load_paths_of_dir_path dir = let physical, logical = !load_paths in diff --git a/checker/environ.ml b/checker/environ.ml index bce40861c..22d1eec17 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -106,7 +106,7 @@ let anomaly s = anomaly (Pp.str s) let add_constant kn cs env = if Cmap_env.mem kn env.env_globals.env_constants then - Printf.ksprintf anomaly ("Constant %s is already defined") + Printf.ksprintf anomaly ("Constant %s is already defined.") (Constant.to_string kn); let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in @@ -161,7 +161,7 @@ let is_projection cst env = let lookup_projection p env = match (lookup_constant (Projection.constant p) env).const_proj with | Some pb -> pb - | None -> anomaly ("lookup_projection: constant is not a projection") + | None -> anomaly ("lookup_projection: constant is not a projection.") (* Mutual Inductives *) let scrape_mind env kn= @@ -182,7 +182,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined") + Printf.ksprintf anomaly ("Inductive %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in @@ -201,7 +201,7 @@ let add_mind kn mib env = let add_modtype ln mtb env = if MPmap.mem ln env.env_globals.env_modtypes then - Printf.ksprintf anomaly ("Module type %s is already defined") + Printf.ksprintf anomaly ("Module type %s is already defined.") (ModPath.to_string ln); let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = @@ -211,7 +211,7 @@ let add_modtype ln mtb env = let shallow_add_module mp mb env = if MPmap.mem mp env.env_globals.env_modules then - Printf.ksprintf anomaly ("Module %s is already defined") + Printf.ksprintf anomaly ("Module %s is already defined.") (ModPath.to_string mp); let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = @@ -221,7 +221,7 @@ let shallow_add_module mp mb env = let shallow_remove_module mp env = if not (MPmap.mem mp env.env_globals.env_modules) then - Printf.ksprintf anomaly ("Module %s is unknown") + Printf.ksprintf anomaly ("Module %s is unknown.") (ModPath.to_string mp); let new_mods = MPmap.remove mp env.env_globals.env_modules in let new_globals = diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 0482912b0..c9ee326cb 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t = let env1 = push_rel (LocalDef (name,def,ty)) env in sorts_of_constr_args env1 c | _ when is_constructor_head t -> [] - | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") + | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.") (* Prop and Set are small *) @@ -302,11 +302,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") (* Conclusion of constructors: check the inductive type is called with the expected parameters *) diff --git a/checker/inductive.ml b/checker/inductive.ml index 9e417a8eb..f890adba9 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -75,7 +75,7 @@ let constructor_instantiate mind u mib c = let instantiate_params full t u args sign = let fail () = - anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = fold_rel_context (fun decl (largs,subs,ty) -> @@ -986,7 +986,7 @@ let check_one_fix renv recpos trees def = List.iter (check_rec_call renv []) l; check_rec_call renv [] c - | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") + | Var _ -> anomaly (Pp.str "Section variable in Coqchk!") | Sort _ -> assert (l = []) @@ -1004,7 +1004,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly (Pp.str "Not enough abstractions in fix body") + | _ -> anomaly (Pp.str "Not enough abstractions in fix body.") in check_rec_call renv [] def @@ -1018,7 +1018,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || Array.length names <> nbfix || bodynum < 0 || bodynum >= nbfix - then anomaly (Pp.str "Ill-formed fix term"); + then anomaly (Pp.str "Ill-formed fix term."); let fixenv = push_rec_types recdef env in let raise_err env i err = error_ill_formed_rec_body env err names i in @@ -1039,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -1073,7 +1073,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.") let rec codomain_is_coind env c = let b = whd_all env c in diff --git a/checker/reduction.ml b/checker/reduction.ml index 82f09cf4b..ba0b01784 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -333,13 +333,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Eta-expansion on the fly *) | (FLambda _, _) -> if v1 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr univ CONV infos (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) | (_, FLambda _) -> if v2 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr univ CONV infos (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) @@ -479,7 +479,7 @@ let vm_conv cv_pb = fconv cv_pb true let hnf_prod_app env t n = match whd_all env t with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl diff --git a/checker/term.ml b/checker/term.ml index 8cac78375..75c566aeb 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -333,7 +333,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") in prodec_rec [] diff --git a/checker/typeops.ml b/checker/typeops.ml index 1396d56df..0163db334 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -262,7 +262,7 @@ let rec execute env cstr = | Rel n -> judge_of_relative env n - | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") + | Var _ -> anomaly (Pp.str "Section variable in Coqchk!") | Const c -> judge_of_constant env c @@ -344,10 +344,10 @@ let rec execute env cstr = (* Partial proofs: unsupported by the kernel *) | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") + anomaly (Pp.str "the kernel does not support metavariables.") | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") + anomaly (Pp.str "the kernel does not support existential variables.") and execute_type env constr = let j = execute env constr in diff --git a/checker/univ.ml b/checker/univ.ml index fb1a0faa7..571743231 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -545,7 +545,7 @@ let repr g u = let a = try UMap.find u g with Not_found -> anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") + (str"Universe " ++ Level.pr u ++ str" undefined.") in match a with | Equiv v -> repr_rec v @@ -848,7 +848,7 @@ let merge g arcu arcv = else (max_rank, old_max_rank, best_arc, arc::rest) in match between g arcu arcv with - | [] -> anomaly (str "Univ.between") + | [] -> anomaly (str "Univ.between.") | arc::rest -> let (max_rank, old_max_rank, best_arc, rest) = List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in @@ -911,7 +911,7 @@ let enforce_univ_eq u v g = | FastLT -> error_inconsistency Eq u v | FastLE -> merge g arcv arcu | FastNLE -> merge_disc g arcu arcv - | FastEQ -> anomaly (Pp.str "Univ.compare")) + | FastEQ -> anomaly (Pp.str "Univ.compare.")) (* enforce_univ_leq : Level.t -> Level.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) @@ -924,7 +924,7 @@ let enforce_univ_leq u v g = | FastLT -> error_inconsistency Le u v | FastLE -> merge g arcv arcu | FastNLE -> fst (setleq g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") + | FastEQ -> anomaly (Pp.str "Univ.compare.") (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) let enforce_univ_lt u v g = @@ -937,7 +937,7 @@ let enforce_univ_lt u v g = | FastNLE -> match fast_compare_neq false g arcv arcu with FastNLE -> fst (setlt g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") + | FastEQ -> anomaly (Pp.str "Univ.compare.") | FastLE | FastLT -> error_inconsistency Lt u v (* Prop = Set is forbidden here. *) @@ -995,13 +995,13 @@ let constraint_add_leq v u c = else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then if Level.equal x y then (* u+(k+1) <= u *) raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u)) - else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints") + else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") else if j = 0 then Constraint.add (x,Le,y) c else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints") + else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -1012,7 +1012,7 @@ let enforce_leq u v c = match v with | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) -> Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c - | _ -> anomaly (Pp.str"A universe bound can only be a variable") + | _ -> anomaly (Pp.str"A universe bound can only be a variable.") let enforce_leq u v c = if check_univ_leq u v then c diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 3ef725cbb..59ad4ef47 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -220,7 +220,7 @@ let make_pure_subst evi args = (fun decl (args,l) -> match args with | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) - | _ -> anomaly (Pp.str "Instance does not match its signature")) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) (evar_filtered_context evi) (Array.rev_to_list args,[])) (*------------------------------------* diff --git a/engine/evd.ml b/engine/evd.ml index 36d469e04..08d26f40d 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -155,7 +155,7 @@ let make_evar hyps ccl = { } let instance_mismatch () = - anomaly (Pp.str "Signature and its instance do not match") + anomaly (Pp.str "Signature and its instance do not match.") let evar_concl evi = evi.evar_concl @@ -400,7 +400,7 @@ let rename evk id (evtoid, idtoev) = match id' with | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) | Some id' -> - if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); + if Idmap.mem id idtoev then anomaly (str "Evar name already in use."); (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = @@ -510,7 +510,7 @@ let raw_map f d = let () = match info.evar_body, ans.evar_body with | Evar_defined _, Evar_empty | Evar_empty, Evar_defined _ -> - anomaly (str "Unrespectful mapping function") + anomaly (str "Unrespectful mapping function.") | _ -> () in ans @@ -524,7 +524,7 @@ let raw_map_undefined f d = let ans = f evk info in let () = match ans.evar_body with | Evar_defined _ -> - anomaly (str "Unrespectful mapping function") + anomaly (str "Unrespectful mapping function.") | _ -> () in ans @@ -553,7 +553,7 @@ let existential_type d (n, args) = let info = try find d n with Not_found -> - anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in + anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in instantiate_evar_array info info.evar_concl args let add_constraints d c = @@ -635,9 +635,9 @@ let define_aux def undef evk body = try EvMap.find evk undef with Not_found -> if EvMap.mem evk def then - anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice") + anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.") else - anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") + anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in let newinfo = { oldinfo with evar_body = Evar_defined body } in @@ -1022,7 +1022,7 @@ let try_meta_fvalue evd mv = let meta_fvalue evd mv = try try_meta_fvalue evd mv - with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value") + with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value.") let meta_value evd mv = (fst (try_meta_fvalue evd mv)).rebus @@ -1041,7 +1041,7 @@ let meta_declare mv v ?(name=Anonymous) evd = let meta_assign mv (v, pb) evd = let modify _ = function | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty) - | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined") + | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.") in let metas = Metamap.modify mv modify evd.metas in set_metas evd metas @@ -1049,7 +1049,7 @@ let meta_assign mv (v, pb) evd = let meta_reassign mv (v, pb) evd = let modify _ = function | Clval(na, _, ty) -> Clval (na, (mk_freelisted v, pb), ty) - | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined") + | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined.") in let metas = Metamap.modify mv modify evd.metas in set_metas evd metas @@ -1090,7 +1090,7 @@ let dependent_evar_ident ev evd = let evi = find evd ev in match evi.evar_source with | (_,Evar_kinds.VarInstance id) -> id - | _ -> anomaly (str "Not an evar resulting of a dependent binding") + | _ -> anomaly (str "Not an evar resulting of a dependent binding.") (**********************************************************) (* Extra data *) diff --git a/engine/termops.ml b/engine/termops.ml index cbb0f0779..92016d4af 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -503,7 +503,7 @@ let push_named_rec_types (lna,typarray,_) env = (fun i na t -> match na with | Name id -> LocalAssum (id, lift i t) - | Anonymous -> anomaly (Pp.str "Fix declarations must be named")) + | Anonymous -> anomaly (Pp.str "Fix declarations must be named.")) lna typarray in Array.fold_left (fun e assum -> push_named assum e) env ctxt @@ -579,7 +579,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with (* Get the last arg of an application *) let last_arg sigma c = match EConstr.kind sigma c with | App (f,cl) -> Array.last cl - | _ -> anomaly (Pp.str "last_arg") + | _ -> anomaly (Pp.str "last_arg.") (* Get the last arg of an application *) let decompose_app_vect sigma c = @@ -1286,7 +1286,7 @@ let rec eta_reduce_head sigma c = (match EConstr.kind sigma (eta_reduce_head sigma c') with | App (f,cl) -> let lastn = (Array.length cl) - 1 in - if lastn < 0 then anomaly (Pp.str "application without arguments") + if lastn < 0 then anomaly (Pp.str "application without arguments.") else (match EConstr.kind sigma cl.(lastn) with | Rel 1 -> @@ -1439,7 +1439,7 @@ let prod_applist sigma c l = match EConstr.kind sigma c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> Vars.substl subst c - | _ -> anomaly (Pp.str "Not enough prod's") in + | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l (* Combinators on judgments *) @@ -1455,7 +1455,7 @@ let context_chop k ctx = | (0, l2) -> (List.rev acc, l2) | (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t) | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) - | (_, []) -> anomaly (Pp.str "context_chop") + | (_, []) -> anomaly (Pp.str "context_chop.") in chop_aux [] (k,ctx) (* Do not skip let-in's *) diff --git a/engine/universes.ml b/engine/universes.ml index 1900112dd..f20108186 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -101,7 +101,7 @@ let enforce_eq_instances_univs strict x y c = let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ - Pp.str " instances of different lengths"); + Pp.str " instances of different lengths."); CArray.fold_right2 (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) ax ay c diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index c736e1a74..3af63de4d 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -188,8 +188,8 @@ let declare_vernac_argument loc s pr cl = <:str_item< do { Pptactic.declare_extra_genarg_pprule $wit$ $pr_rules$ - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer")) - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer")) } + (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.")) + (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) } >> ] open Pcaml diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4e613f163..9c771cbef 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -357,7 +357,7 @@ let handle_exn (e, info) = let init = let initialized = ref false in fun file -> - if !initialized then anomaly (str "Already initialized") + if !initialized then anomaly (str "Already initialized.") else begin let init_sid = Stm.get_current_state () in initialized := true; diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 70133fb9f..d16efa603 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -411,7 +411,7 @@ class text_param_box param (tt:GData.tooltips) = let v = param.string_of_string (buffer#get_text ()) in if v <> param.string_value then ( - dbg "apply new value !"; + dbg "apply new value!"; let _ = param.string_f_apply v in param.string_value <- v ) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f6da10c96..5dc02e602 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -698,7 +698,7 @@ let rec extern inctx scopes vars r = | None :: q -> raise No_match | Some c :: q -> match locs with - | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]") + | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") | (_, false) :: locs' -> (* we don't want to print locals *) ip q locs' args acc @@ -1033,7 +1033,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> - anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable") + anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) @@ -1064,7 +1064,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | _, Some ind -> let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in simple_cases_matrix_of_branches ind bl' - | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive") + | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in let mat = if info.cip_extensible then mat @ [any_any_branch] else mat in @@ -1072,7 +1072,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> return_type_of_predicate ind nargs (glob_of_pat env sigma p) - | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") + | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 190369e8f..eac8bd1a3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -616,7 +616,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[]) with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation") in + anomaly (Pp.str "Inconsistent substitution of recursive notation.") in let termin = aux (terms,None,None) subinfos terminator in let fold a t = let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in @@ -659,7 +659,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = termin bl in make_letins letins res with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in @@ -1070,7 +1070,7 @@ let sort_fields ~complete loc fields completer = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) with Not_found -> - anomaly (str "Environment corruption for records") in + anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) @@ -1085,7 +1085,7 @@ let sort_fields ~complete loc fields completer = let field_glob_ref = ConstRef field_glob_id in let first_field = eq_gr field_glob_ref first_field_glob_ref in begin match proj_kinds with - | [] -> anomaly (Pp.str "Number of projections mismatch") + | [] -> anomaly (Pp.str "Number of projections mismatch.") | (_, regular) :: proj_kinds -> (* "regular" is false when the field is defined by a let-in in the record declaration @@ -1218,7 +1218,7 @@ let drop_notations_pattern looked_for = | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[]) - | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr "))) x + | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in let rec drop_syndef top scopes re pats = let (loc,qid) = qualid_of_reference re in @@ -1345,7 +1345,7 @@ let drop_notations_pattern looked_for = in_pat top (scopt,subscopes@snd scopes) a with Not_found -> if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else - anomaly (str "Unbound pattern notation variable: " ++ Id.print id) + anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> ensure_kind top loc g; @@ -1370,7 +1370,7 @@ let drop_notations_pattern looked_for = subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) termin with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NHole _ -> let () = assert (List.is_empty args) in CAst.make ?loc @@ RCPatAtom None @@ -1464,7 +1464,7 @@ let get_implicit_name n imps = let set_hole_implicit i b = function | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) - | _ -> anomaly (Pp.str "Only refs have implicits") + | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp)) diff --git a/interp/notation.ml b/interp/notation.ml index d19654b10..23332f7c4 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -381,7 +381,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function let declare_notation_level ntn level = if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level"); + anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); notation_level_map := String.Map.add ntn level !notation_level_map let level_of_notation ntn = @@ -1004,13 +1004,13 @@ let declare_notation_rule ntn ~extra unpl gram = let find_notation_printing_rule ntn = try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) + with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") let find_notation_extra_printing_rules ntn = try pi2 (String.Map.find ntn !notation_rules) with Not_found -> [] let find_notation_parsing_rules ntn = try pi3 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") let get_defined_notations () = String.Set.elements @@ String.Map.domain !notation_rules diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8e876ec16..08b9fbe8e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -690,7 +690,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig | { CAst.v = GVar id' } -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable") + | _ -> anomaly (str "A term which can be a binder has to be a variable.") with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) @@ -830,7 +830,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in add_bindinglist_env sigma var bl with Not_found -> - anomaly (str "There should be a binder list bindings this list of terms") + anomaly (str "There should be a binder list bindings this list of terms.") let match_fix_kind fk1 fk2 = match (fk1,fk2) with diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 8515d51b0..8bd4b5bfe 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -794,7 +794,7 @@ let drop_parameters depth n argstk = try try_drop_parameters depth n argstk with Not_found -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") + anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.") (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant diff --git a/kernel/cooking.ml b/kernel/cooking.ml index a9f212393..4deadff0a 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -26,7 +26,7 @@ module NamedDecl = Context.Named.Declaration (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with - | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath") + | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.") | _::l -> DirPath.make l let pop_mind kn = diff --git a/kernel/environ.ml b/kernel/environ.ml index 9986f439a..5727bf2ea 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -342,7 +342,7 @@ let template_polymorphic_pconstant (cst,u) env = let lookup_projection cst env = match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection") + | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") let is_projection cst env = match (lookup_constant cst env).const_proj with @@ -546,7 +546,7 @@ let register env field entry = | KInt31 (grp, Int31Type) -> let i31c = match kind_of_term entry with | Ind i31t -> mkConstructUi (i31t, 1) - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry @@ -592,7 +592,7 @@ fun rk value field -> let int31_op_from_const n op prim = match kind_of_term value with | Const kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in let int31_unop_from_const op prim = int31_op_from_const 1 op prim in @@ -604,20 +604,20 @@ fun rk value field -> match field with | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field") + (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = match kind_of_term int31bit with | Ind (i31bit_type,_) -> i31bit_type | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type") + (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = match kind_of_term value with | Ind (i31t,_) -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type") + (Pp.str "should be an inductive type.") in { empty_reactive_info with vm_decompile_const = Some int31_decompilation; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 2ff419338..1e13239bf 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -214,7 +214,7 @@ let param_ccls paramsctxt = *) let typecheck_inductive env mie = let () = match mie.mind_entry_inds with - | [] -> anomaly (Pp.str "empty inductive types declaration") + | [] -> anomaly (Pp.str "empty inductive types declaration.") | _ -> () in (* Check unicity of names *) @@ -313,7 +313,7 @@ let typecheck_inductive env mie = anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr infu) + ++ Universe.pr infu ++ Pp.str ".") in RegularArity (not is_natural,full_arity,defu) in @@ -333,7 +333,7 @@ let typecheck_inductive env mie = anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr clev) + ++ Universe.pr clev ++ Pp.str ".") else TemplateArity (param_ccls paramsctxt, infu) | _ (* Not an explicit occurrence of Type *) -> @@ -389,11 +389,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") (* Check the inductive type is called with the expected parameters *) (* [n] is the index of the last inductive type in [env] *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4f4b641b4..f3b03252d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -75,7 +75,7 @@ let constructor_instantiate mind u mib c = let instantiate_params full t u args sign = let fail () = - anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = Context.Rel.fold_outside (fun decl (largs,subs,ty) -> @@ -1023,7 +1023,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly (Pp.str "Not enough abstractions in fix body") + | _ -> anomaly (Pp.str "Not enough abstractions in fix body.") in check_rec_call renv [] def @@ -1039,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || not (Int.equal (Array.length names) nbfix) || bodynum < 0 || bodynum >= nbfix - then anomaly (Pp.str "Ill-formed fix term"); + then anomaly (Pp.str "Ill-formed fix term."); let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = @@ -1061,7 +1061,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -1100,7 +1100,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.") let rec codomain_is_coind env c = let b = whd_all env c in diff --git a/kernel/modops.ml b/kernel/modops.ml index 0f0056ed4..1f8b97ae6 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -265,7 +265,7 @@ let add_retroknowledge mp = Environ.register env f e |_ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" - (Pp.str "had to import an unsupported kind of term") + (Pp.str "had to import an unsupported kind of term.") in fun lclrk env -> (* The order of the declaration matters, for instance (and it's at the diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 5130aa9a4..d3cd6b62a 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -201,47 +201,47 @@ let empty_symbols = [||] let get_value tbl i = match tbl.(i) with | SymbValue v -> v - | _ -> anomaly (Pp.str "get_value failed") + | _ -> anomaly (Pp.str "get_value failed.") let get_sort tbl i = match tbl.(i) with | SymbSort s -> s - | _ -> anomaly (Pp.str "get_sort failed") + | _ -> anomaly (Pp.str "get_sort failed.") let get_name tbl i = match tbl.(i) with | SymbName id -> id - | _ -> anomaly (Pp.str "get_name failed") + | _ -> anomaly (Pp.str "get_name failed.") let get_const tbl i = match tbl.(i) with | SymbConst kn -> kn - | _ -> anomaly (Pp.str "get_const failed") + | _ -> anomaly (Pp.str "get_const failed.") let get_match tbl i = match tbl.(i) with | SymbMatch case_info -> case_info - | _ -> anomaly (Pp.str "get_match failed") + | _ -> anomaly (Pp.str "get_match failed.") let get_ind tbl i = match tbl.(i) with | SymbInd ind -> ind - | _ -> anomaly (Pp.str "get_ind failed") + | _ -> anomaly (Pp.str "get_ind failed.") let get_meta tbl i = match tbl.(i) with | SymbMeta m -> m - | _ -> anomaly (Pp.str "get_meta failed") + | _ -> anomaly (Pp.str "get_meta failed.") let get_evar tbl i = match tbl.(i) with | SymbEvar ev -> ev - | _ -> anomaly (Pp.str "get_evar failed") + | _ -> anomaly (Pp.str "get_evar failed.") let get_level tbl i = match tbl.(i) with | SymbLevel u -> u - | _ -> anomaly (Pp.str "get_level failed") + | _ -> anomaly (Pp.str "get_level failed.") let push_symbol x = try HashtblSymbol.find symb_tbl x diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 3593d94c2..fe9f393f6 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -144,7 +144,7 @@ let native_conv_gen pb sigma env univs t1 t2 = (* TODO change 0 when we can have de Bruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) end - | _ -> anomaly (Pp.str "Compilation failure") + | _ -> anomaly (Pp.str "Compilation failure.") let warn_no_native_compiler = let open Pp in diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 26d061768..f6c94158f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -15,7 +15,7 @@ open Envars used by the native compiler. *) let get_load_paths = - ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized") : unit -> string list) + ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized.") : unit -> string list) let open_header = ["Nativevalues"; "Nativecode"; diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8d5f6388c..7ffb48221 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -200,7 +200,7 @@ let mk_block tag args = (* Two instances of dummy_value should not be pointer equal, otherwise comparing them as terms would succeed *) let dummy_value : unit -> t = - fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed") + fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.") let cast_accu v = (Obj.magic v:accumulator) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 502a10113..59e90ca2e 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -54,8 +54,8 @@ let create cu = Direct ([],cu) let turn_indirect dp o tab = match o with | Indirect (_,_,i) -> if not (Int.Map.mem i tab.opaque_val) - then CErrors.anomaly (Pp.str "Indirect in a different table") - else CErrors.anomaly (Pp.str "Already an indirect opaque") + then CErrors.anomaly (Pp.str "Indirect in a different table.") + else CErrors.anomaly (Pp.str "Already an indirect opaque.") | Direct (d,cu) -> (** Uncomment to check dynamically that all terms turned into indirections are hashconsed. *) @@ -67,21 +67,21 @@ let turn_indirect dp o tab = match o with if DirPath.equal dp tab.opaque_dir then tab.opaque_dir else if DirPath.equal tab.opaque_dir DirPath.initial then dp else CErrors.anomaly - (Pp.str "Using the same opaque table for multiple dirpaths") in + (Pp.str "Using the same opaque table for multiple dirpaths.") in let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in Indirect ([],dp,id), ntab let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque") + | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") let iter_direct_opaque f = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ba714ada2..427ce04c5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -324,7 +324,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match kind_of_term a1, kind_of_term a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (Sort)"); + anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m @@ -421,7 +421,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inconsistency: we tolerate that v1, v2 contain shift and update but we throw them away *) if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FLambda)"); + anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in @@ -429,7 +429,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FProd)"); + anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv @@ -439,7 +439,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let () = match v1 with | [] -> () | _ -> - anomaly (Pp.str "conversion was given unreduced term (FLambda)") + anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr CONV l2r infos @@ -448,7 +448,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let () = match v2 with | [] -> () | _ -> - anomaly (Pp.str "conversion was given unreduced term (FLambda)") + anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr CONV l2r infos @@ -767,7 +767,7 @@ let betazeta_appvect = lambda_appvect_assum let hnf_prod_app env t n = match kind_of_term (whd_all env t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl diff --git a/kernel/term.ml b/kernel/term.ml index a4296a530..07a85329e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -456,7 +456,7 @@ let lambda_applist c l = match kind_of_term c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c - | _ -> anomaly (Pp.str "Not enough lambda's") in + | _ -> anomaly (Pp.str "Not enough lambda's.") in app [] c l let lambda_appvect c v = lambda_applist c (Array.to_list v) @@ -465,11 +465,11 @@ let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match kind_of_term t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) @@ -480,7 +480,7 @@ let prod_applist c l = match kind_of_term c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c - | _ -> anomaly (Pp.str "Not enough prod's") in + | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) @@ -490,11 +490,11 @@ let prod_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match kind_of_term t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough prod/let's") in + | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) @@ -660,7 +660,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") in prodec_rec [] diff --git a/kernel/typeops.ml b/kernel/typeops.ml index dbc0dcb73..1a07bb2fc 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -430,10 +430,10 @@ let rec execute env cstr = (* Partial proofs: unsupported by the kernel *) | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") + anomaly (Pp.str "the kernel does not support metavariables.") | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") + anomaly (Pp.str "the kernel does not support existential variables.") and execute_is_type env constr = let t = execute env constr in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 6971c0a2b..487257a77 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -132,7 +132,7 @@ let rec repr g u = let a = try UMap.find u g.entries with Not_found -> CErrors.anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") + (str"Universe " ++ Level.pr u ++ str" undefined.") in match a with | Equiv v -> repr g v diff --git a/kernel/univ.ml b/kernel/univ.ml index afe9cbe8d..d53dd8e73 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -781,7 +781,7 @@ let enforce_eq_level u v c = let enforce_eq u v c = match Universe.level u, Universe.level v with | Some u, Some v -> enforce_eq_level u v c - | _ -> anomaly (Pp.str "A universe comparison can only happen between variables") + | _ -> anomaly (Pp.str "A universe comparison can only happen between variables.") let check_univ_eq u v = Universe.equal u v @@ -801,13 +801,13 @@ let constraint_add_leq v u c = else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then if Level.equal x y then (* u+(k+1) <= u *) raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None)) - else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints") + else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") else if j = 0 then Constraint.add (x,Le,y) c else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints") + else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -982,7 +982,7 @@ let enforce_eq_instances x y = let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with") - (Pp.str " instances of different lengths")); + (Pp.str " instances of different lengths.")); CArray.fold_right2 enforce_eq_level ax ay type universe_instance = Instance.t diff --git a/kernel/vars.ml b/kernel/vars.ml index f1c0a4f08..629de80f7 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -175,7 +175,7 @@ let subst_of_rel_context_instance sign l = | LocalDef (_,c,_)::sign', args' -> aux (substl subst c :: subst) sign' args' | [], [] -> subst - | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match") + | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") in aux [] (List.rev sign) l let adjust_subst_to_rel_context sign l = diff --git a/kernel/vm.ml b/kernel/vm.ml index 53483a222..21c1225cc 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -236,7 +236,7 @@ let uni_lvl_val (v : values) : Univ.universe_level = in CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr) + ++ pr ++ str ".") let rec whd_accu a stk = let stk = @@ -285,7 +285,7 @@ let rec whd_accu a stk = end | tg -> CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -308,7 +308,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) else Vconstr_block(Obj.obj o) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b0e77a4c9..8ef11a2cd 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -77,7 +77,7 @@ let where = function if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () let raw_anomaly e = match e with - | Anomaly (s, pps) -> where s ++ pps ++ str "." + | Anomaly (s, pps) -> where s ++ pps | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." diff --git a/lib/future.ml b/lib/future.ml index 1360b7ac4..8bef1e58e 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -157,7 +157,7 @@ let chain ~pure ck f = | Val (v, None) -> match !ck with | Finished _ -> CErrors.anomaly(Pp.str - "Future.chain ~pure:false call on an already joined computation") + "Future.chain ~pure:false call on an already joined computation.") | Ongoing _ -> CErrors.anomaly(Pp.strbrk( "Future.chain ~pure:false call on a pure computation. "^ "This can happen if the computation was initial created with "^ @@ -171,7 +171,7 @@ let replace kx y = match !x with | Exn _ -> x := Closure (fun () -> force ~pure:false y) | _ -> CErrors.anomaly - (Pp.str "A computation can be replaced only if is_exn holds") + (Pp.str "A computation can be replaced only if is_exn holds.") let purify f x = let state = !freeze () in @@ -213,7 +213,7 @@ let map2 f x l = let xi = chain ~pure:true x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> - CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in + CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in f xi y) 0 l let print f kx = diff --git a/lib/genarg.ml b/lib/genarg.ml index 05c828d5f..377ff8182 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -159,7 +159,7 @@ let create_arg name = match ArgT.name name with | None -> ExtraArg (ArgT.create name) | Some _ -> - CErrors.anomaly (str "generic argument already declared: " ++ str name) + CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".") let make0 = create_arg @@ -180,7 +180,7 @@ struct let register0 arg f = match arg with | ExtraArg s -> if GenMap.mem s !arg0_map then - let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in + let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map @@ -192,7 +192,7 @@ struct with Not_found -> match M.default (ExtraArg name) with | None -> - CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) + CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".") | Some obj -> obj (** For now, the following function is quite dummy and should only be applied diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index e7646fb79..11f151a60 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build = (* - in the main process there is a race condition between slave managers (that are threads) and the main thread, hence the mutex *) if Flags.async_proofs_is_worker () then - CErrors.anomaly(Pp.str"Slave processes must install remote counters"); + CErrors.anomaly(Pp.str"Slave processes must install remote counters."); Mutex.lock m; let x = f () in Mutex.unlock m; build x in let mk_thsafe_remote_getter f () = @@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build = let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in let installer f = if not (Flags.async_proofs_is_worker ()) then - CErrors.anomaly(Pp.str"Only slave processes can install a remote counter"); + CErrors.anomaly(Pp.str"Only slave processes can install a remote counter."); getter := mk_thsafe_remote_getter f in (fun () -> !getter ()), installer diff --git a/lib/spawn.ml b/lib/spawn.ml index 479176973..4d7e78d86 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -200,7 +200,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) p, cout let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead"; + assert_ alive "This process is dead."; output_value oob_req ReqStats; flush oob_req; input_value oob_resp @@ -251,7 +251,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = with e -> prerr_endline ("kill: "^Printexc.to_string e) end let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead"; + assert_ alive "This process is dead."; output_value oob_req ReqStats; flush oob_req; let RespStats g = input_value oob_resp in g diff --git a/library/coqlib.ml b/library/coqlib.ml index 955ff4c08..0cb8c7afc 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s = | [] -> anomaly ~label:locstr (str "cannot find " ++ str s ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs) + prlist_with_sep pr_comma pr_dirpath dirs ++ str ".") | l -> anomaly ~label:locstr (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs) + prlist_with_sep pr_comma pr_dirpath dirs ++ str ".") (* For tactics/commands requiring vernacular libraries *) @@ -185,7 +185,7 @@ let build_bool_type () = andb_prop = init_reference ["Datatypes"] "andb_prop"; andb_true_intro = init_reference ["Datatypes"] "andb_true_intro" } -let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type") +let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.") let build_sigma_type () = { proj1 = init_reference ["Specif"] "projT1"; @@ -368,7 +368,7 @@ let coq_eq_ref = lazy (init_reference ["Logic"] "eq") let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq") let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true") -let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref")) +let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref.")) let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_exist_ref = lazy (init_reference ["Specif"] "exist") let coq_not_ref = lazy (init_reference ["Logic"] "not") diff --git a/library/declare.ml b/library/declare.ml index 29aa08e77..7d0edbc8b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) = obj.cst_was_seff <- false; if Global.exists_objlabel (Label.of_id (basename sp)) then constant_of_kn kn - else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") end else let () = check_exists sp in let kn', exported = Global.add_constant dir id obj.cst_decl in @@ -385,7 +385,7 @@ let declare_projections mind = let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename - | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in + | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in let isrecord,isprim = declare_projections mind in @@ -400,7 +400,7 @@ let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "no recursive definition") + | [] -> anomaly (Pp.str "no recursive definition.") | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" @@ -415,7 +415,7 @@ let fixpoint_message indexes l = let cofixpoint_message l = Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "No corecursive definition") + | [] -> anomaly (Pp.str "No corecursive definition.") | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ spc () ++ str "are corecursively defined")) diff --git a/library/declaremods.ml b/library/declaremods.ml index 08c33b5c1..c98d4a7f3 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -252,7 +252,7 @@ let in_modkeep : Lib.lib_objects -> obj = let do_modtype i sp mp sobjs = if Nametab.exists_modtype sp then - anomaly (pr_path sp ++ str " already exists"); + anomaly (pr_path sp ++ str " already exists."); Nametab.push_modtype (Nametab.Until i) sp mp; ModSubstObjs.set mp sobjs @@ -883,7 +883,7 @@ let register_library dir cenv (objs:library_objects) digest univ = (* If not, let's do it now ... *) let mp' = Global.import cenv univ digest in if not (ModPath.equal mp mp') then - anomaly (Pp.str "Unexpected disk module name"); + anomaly (Pp.str "Unexpected disk module name."); in let sobjs,keepobjs = objs in do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs diff --git a/library/global.ml b/library/global.ml index 5fa710b36..1ba86699d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -44,7 +44,7 @@ let () = let assert_not_parsing () = if !Flags.we_are_parsing then CErrors.anomaly ( - Pp.strbrk"The global environment cannot be accessed during parsing") + Pp.strbrk"The global environment cannot be accessed during parsing.") let safe_env () = assert_not_parsing(); !global_env diff --git a/library/globnames.ml b/library/globnames.ml index a78f5f13a..9aeb37973 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -242,4 +242,4 @@ let pop_global_reference = function | ConstRef con -> ConstRef (pop_con con) | IndRef (kn,i) -> IndRef (pop_kn kn,i) | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) - | VarRef id -> anomaly (Pp.str "VarRef not poppable") + | VarRef id -> anomaly (Pp.str "VarRef not poppable.") diff --git a/library/goptions.ml b/library/goptions.ml index a803771cb..a305214e8 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -273,23 +273,23 @@ type 'a write_function = 'a -> unit let declare_int_option = declare_option (fun v -> IntValue v) - (function IntValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun _ _ -> anomaly (Pp.str "async_option")) + (function IntValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) let declare_bool_option = declare_option (fun v -> BoolValue v) - (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun _ _ -> anomaly (Pp.str "async_option")) + (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) let declare_string_option = declare_option (fun v -> StringValue v) - (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) + (function StringValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun x y -> x^","^y) let declare_stringopt_option = declare_option (fun v -> StringOptValue v) - (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun _ _ -> anomaly (Pp.str "async_option")) + (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) (* 3- User accessible commands *) diff --git a/library/heads.ml b/library/heads.ml index 02465f22f..3adfe0fd2 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -72,7 +72,8 @@ let kind_of_head env t = with Not_found -> CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++ - str (Names.Constant.to_string cst))) + str (Names.Constant.to_string cst) ++ + str ".")) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType diff --git a/library/impargs.ml b/library/impargs.ml index 885185da1..8f3bfc17e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -291,16 +291,16 @@ let is_status_implicit = function | _ -> true let name_of_implicit = function - | None -> anomaly (Pp.str "Not an implicit argument") + | None -> anomaly (Pp.str "Not an implicit argument.") | Some (id,_,_) -> id let maximal_insertion_of = function | Some (_,_,(b,_)) -> b - | None -> anomaly (Pp.str "Not an implicit argument") + | None -> anomaly (Pp.str "Not an implicit argument.") let force_inference_of = function | Some (_, _, (_, b)) -> b - | None -> anomaly (Pp.str "Not an implicit argument") + | None -> anomaly (Pp.str "Not an implicit argument.") (* [in_ctx] means we know the expected type, [n] is the index of the argument *) let is_inferable_implicit in_ctx n = function @@ -324,7 +324,7 @@ let positions_of_implicits (_,impls) = let rec prepare_implicits f = function | [] -> [] - | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit") + | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") | (Name id, Some imp)::imps -> let imps' = prepare_implicits f imps in Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' diff --git a/library/kindops.ml b/library/kindops.ml index 21b1bec33..623d2537a 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -25,7 +25,7 @@ let string_of_theorem_kind = function let string_of_definition_kind def = let (locality, poly, kind) = def in - let error () = CErrors.anomaly (Pp.str "Internal definition kind") in + let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in match kind with | Definition -> begin match locality with @@ -64,4 +64,4 @@ let string_of_definition_kind def = | Global -> "Global Instance" end | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind") + CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/lib.ml b/library/lib.ml index 4ad4e261d..9d71a854f 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -350,7 +350,7 @@ let end_compilation_checks dir = try match find_entry_p is_opening_lib with | (oname, CompilingLibrary prefix) -> oname | _ -> assert false - with Not_found -> anomaly (Pp.str "No module declared") + with Not_found -> anomaly (Pp.str "No module declared.") in let _ = match !lib_state.comp_name with @@ -358,7 +358,7 @@ let end_compilation_checks dir = | Some m -> if not (Names.DirPath.equal m dir) then anomaly (str "The current open module has name" ++ spc () ++ pr_dirpath m ++ - spc () ++ str "and not" ++ spc () ++ pr_dirpath m); + spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str "."); in oname @@ -547,7 +547,7 @@ let discharge_item ((sp,_ as oname),e) = | FrozenState _ -> None | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> - anomaly (Pp.str "discharge_item") + anomaly (Pp.str "discharge_item.") let close_section () = let oname,fs = diff --git a/library/loadpath.ml b/library/loadpath.ml index 529b9502b..ad429ea84 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -29,7 +29,7 @@ let physical p = p.path_physical let get_load_paths () = !load_paths let anomaly_too_many_paths path = - anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) + anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") let find_load_path phys_dir = let phys_dir = CUnix.canonical_path_name phys_dir in diff --git a/library/nametab.ml b/library/nametab.ml index 2e4e98013..93e9c03ce 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -294,7 +294,7 @@ module DirPath' = struct include DirPath let repr dir = match DirPath.repr dir with - | [] -> anomaly (Pp.str "Empty dirpath") + | [] -> anomaly (Pp.str "Empty dirpath.") | id :: l -> (id, l) end diff --git a/library/summary.ml b/library/summary.ml index d9f644100..c7bf95fd4 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -46,7 +46,7 @@ let declare_summary sumname decl = let () = if Int.Map.mem hash !summaries then let (name, _) = Int.Map.find hash !summaries in anomaly ~label:"Summary.declare_summary" - (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name) + (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".") in all_declared_summaries := Int.Set.add hash !all_declared_summaries; summary_names := (hash, sumname) :: !summary_names; @@ -85,10 +85,10 @@ let unfreeze_summaries fs = * may modify the content of [summaries] ny loading new ML modules *) let (_, decl) = try Int.Map.find ml_modules_summary !summaries - with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules) + with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") in let () = match fs.ml_module with - | None -> anomaly (str "Undeclared summary " ++ str ml_modules) + | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") | Some state -> decl.unfreeze_function state in let fold id (_, decl) states = diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 6940fd6fb..890ce2dec 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -298,7 +298,7 @@ let interp_entry forpat e = match e with | ETName -> TTAny TTName | ETReference -> TTAny TTReference | ETBigint -> TTAny TTBigint -| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") +| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.") | ETBinder false -> TTAny TTBinder | ETConstr p -> TTAny (TTConstr (p, forpat)) | ETPattern -> assert false (** not used *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9a4766c0b..20601f900 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -338,7 +338,7 @@ module Gram = let rec remove_grammars n = if n>0 then (match !camlp4_state with - | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") + | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); camlp4_state := t; diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 5dea4631c..ba398c385 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -61,7 +61,7 @@ module ST=struct let enter t sign st= if IntPairTable.mem st.toterm sign then - anomaly ~label:"enter" (Pp.str "signature already entered") + anomaly ~label:"enter" (Pp.str "signature already entered.") else IntPairTable.replace st.toterm sign t; IntTable.replace st.tosign t sign @@ -321,7 +321,7 @@ let find uf i= find_aux uf [] i let get_representative uf i= match uf.map.(i).clas with Rep r -> r - | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative.") let get_constructors uf i= uf.map.(i).constructors @@ -339,7 +339,7 @@ let rec find_oldest_pac uf i pac= let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor.") let size uf i= (get_representative uf i).weight @@ -384,7 +384,7 @@ let term uf i=uf.map.(i).term let subterms uf i= match uf.map.(i).vertex with Node(j,k) -> (j,k) - | _ -> anomaly ~label:"subterms" (Pp.str "not a node") + | _ -> anomaly ~label:"subterms" (Pp.str "not a node.") let signature uf i= let j,k=subterms uf i in (find uf j,find uf k) @@ -485,7 +485,7 @@ let build_subst uf subst = (fun i -> try term uf i with e when CErrors.noncritical e -> - anomaly (Pp.str "incomplete matching")) + anomaly (Pp.str "incomplete matching.")) subst let rec inst_pattern subst = function @@ -750,7 +750,7 @@ let process_constructor_mark t i rep pac state = state.combine; f (n-1) q1 q2 | _-> anomaly ~label:"add_pacs" - (Pp.str "weird error in injection subterms merge") + (Pp.str "weird error in injection subterms merge.") in f cinfo.ci_nhyps opac.args pac.args | Partial_applied | Partial _ -> (* add_pac state.uf.map.(i) pac t; *) @@ -841,7 +841,7 @@ let complete_one_class state i= let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) - | _ -> anomaly (Pp.str "wrong incomplete class") + | _ -> anomaly (Pp.str "wrong incomplete class.") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes @@ -981,7 +981,7 @@ let find_instances state = Control.check_for_interrupt (); do_match state res pb_stack done; - anomaly (Pp.str "get out of here !") + anomaly (Pp.str "get out of here!") with Stack.Empty -> () in !res diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index f58847caf..642ceba3d 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -47,7 +47,7 @@ let rec ptrans p1 p3= {p_lhs=p1.p_lhs; p_rhs=p3.p_rhs; p_rule=Trans (p1,p3)} - else anomaly (Pp.str "invalid cc transitivity") + else anomaly (Pp.str "invalid cc transitivity.") let rec psym p = match p.p_rule with @@ -85,7 +85,7 @@ let rec nth_arg t n= if n>0 then nth_arg t1 (n-1) else t2 - | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args") + | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args.") let pinject p c n a = {p_lhs=nth_arg p.p_lhs (n-a); diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 60fe8e762..b67b9931e 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -19,7 +19,7 @@ open Mlutil let rec msid_of_mt = function | MTident mp -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name") + | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.") (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -231,7 +231,7 @@ let get_decl_in_structure r struc = | _ -> error_not_visible r in go ll sel with Not_found -> - anomaly (Pp.str "reference not found in extracted structure") + anomaly (Pp.str "reference not found in extracted structure.") (*s Optimization of a [ml_structure]. *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a369cbdf3..29dd8ff4f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -261,7 +261,7 @@ let safe_basename_of_global r = let last_chance r = try Nametab.basename_of_global r with Not_found -> - anomaly (Pp.str "Inductive object unknown to extraction and not globally visible") + anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in match r with | ConstRef kn -> Label.to_id (con_label kn) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 4c6355f61..04bca584f 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -77,7 +77,7 @@ let match_one_quantified_hyp sigma setref seq lf= Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> if do_sequent sigma setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref - | _ -> anomaly (Pp.str "can't happen") + | _ -> anomaly (Pp.str "can't happen.") let give_instances sigma lf seq= let setref=ref IS.empty in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8c6b5b91d..f745dbeb4 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -40,7 +40,7 @@ let wrap n b continue seq = let rec aux i nc ctx= if i<=0 then seq else match nc with - []->anomaly (Pp.str "Not the expected number of hyps") + []->anomaly (Pp.str "Not the expected number of hyps.") | nd::q-> let id = NamedDecl.get_id nd in if occur_var env sigma id (pf_concl gls) || diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0041797de..c2f705898 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -397,7 +397,7 @@ let rewrite_until_var arg_num eq_ids : tactic = then tclIDTAC g else match eq_ids with - | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property"); + | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property."); | eq_id::eq_ids -> tclTHEN (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) @@ -605,7 +605,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ pr_leconstr_env (pf_env g') (project g') new_term_value_eq ); - anomaly (Pp.str "cannot compute new term value") + anomaly (Pp.str "cannot compute new term value.") in let fun_body = mkLambda(Anonymous, @@ -838,7 +838,7 @@ let build_proof h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g - | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g @@ -1032,7 +1032,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c - | _ -> CErrors.anomaly (Pp.str "Not a constant") + | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) } | _ -> () @@ -1255,7 +1255,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam try let pte = try destVar (project gl) pte - with DestKO -> anomaly (Pp.str "Property is not a variable") + with DestKO -> anomaly (Pp.str "Property is not a variable.") in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 942527167..a0eb9e2b2 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -44,7 +44,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates - | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) + | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -399,7 +399,7 @@ let get_funs_constant mp dp = let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly (Pp.str "Anonymous fix") + anomaly (Pp.str "Anonymous fix.") ) na | _ -> [|const,0|] diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 68e097fe9..aa8f918ae 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1115,7 +1115,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude - | _ -> anomaly (Pp.str "Should not have an anonymous function here") + | _ -> anomaly (Pp.str "Should not have an anonymous function here.") (* We have renamed all the anonymous functions during alpha_renaming phase *) end diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 0361e8cb1..b99f5a923 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -532,7 +532,7 @@ let rec are_unifiable_aux = function else let eqs' = try (List.combine cpl1 cpl2) @ eqs - with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux") + with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux.") in are_unifiable_aux eqs' @@ -555,7 +555,7 @@ let rec eq_cases_pattern_aux = function else let eqs' = try (List.combine cpl1 cpl2) @ eqs - with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux") + with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux.") in eq_cases_pattern_aux eqs' | _ -> raise NotUnifiable diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 4946285e1..143ce8288 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -734,7 +734,7 @@ let rec add_args id new_args = CAst.map (function CAppExpl((None,r,None),new_args) | _ -> b end - | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") + | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) @@ -782,9 +782,9 @@ let rec add_args id new_args = CAst.map (function Miscops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) - | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") - | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") - | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") + | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") + | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") + | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") ) exception Stop of Constrexpr.constr_expr @@ -826,7 +826,7 @@ let rec chop_n_arrow n t = chop_n_arrow new_n t' with Stop t -> t end - | _ -> anomaly (Pp.str "Not enough products") + | _ -> anomaly (Pp.str "Not enough products.") let rec get_args b t : Constrexpr.local_binder_expr list * @@ -856,7 +856,7 @@ let make_graph (f_ref:global_reference) = | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with - | None -> error "Cannot build a graph over an axiom !" + | None -> error "Cannot build a graph over an axiom!" | Some body -> let env = Global.env () in let sigma = Evd.from_env env in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2476478ab..a73425543 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -369,7 +369,7 @@ let in_Function : function_info -> Libobject.obj = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant") + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) with Not_found -> None @@ -397,7 +397,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive") + with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") in let finfos = { function_constant = f; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 12232dd83..f373e486c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -140,7 +140,7 @@ let generate_type evd g_to_f f graph i = let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with - | [] | [_] -> anomaly (Pp.str "Not a valid context") + | [] | [_] -> anomaly (Pp.str "Not a valid context.") | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function @@ -292,7 +292,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun (_,pat) acc -> match pat with | IntroNaming (IntroIdentifier id) -> id::acc - | _ -> anomaly (Pp.str "Not an identifier") + | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) [] @@ -401,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes Array.map (fun ((_,(ctxt,concl))) -> match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") | hres::res::decl::ctxt -> let res = EConstr.it_mkLambda_or_LetIn (EConstr.it_mkProd_or_LetIn concl [hres;res]) @@ -708,7 +708,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = then let eq_lemma = try Option.get (infos).equation_lemma - with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma") + with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.") in tclTHENSEQ[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; @@ -938,7 +938,7 @@ let revert_graph kn post_tac hid g = let info = try find_Function_of_graph ind' with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) - anomaly (Pp.str "Cannot retrieve infos about a mutual block") + anomaly (Pp.str "Cannot retrieve infos about a mutual block.") in (* if we can find a completeness lemma for this function then we can come back to the functional form. If not, we do nothing diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62eba9513..e6f199dba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -76,7 +76,7 @@ let def_of_const t = | _ -> raise Not_found) with Not_found -> anomaly (str "Cannot find definition of constant " ++ - (Id.print (Label.to_id (con_label (fst sp))))) + (Id.print (Label.to_id (con_label (fst sp)))) ++ str ".") ) |_ -> assert false @@ -95,7 +95,7 @@ let constant sl s = constr_of_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn - | _ -> anomaly (Pp.str "ConstRef expected") + | _ -> anomaly (Pp.str "ConstRef expected.") let nf_zeta env = @@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = travel jinfo new_continuation_tac {expr_info with info = b; is_final=false} g end - | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") | Prod _ -> begin try @@ -486,7 +486,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info) + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> @@ -1165,7 +1165,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let f_id = match f_name with | Name f_id -> next_ident_away_in_goal f_id ids - | Anonymous -> anomaly (Pp.str "Anonymous function") + | Anonymous -> anomaly (Pp.str "Anonymous function.") in let n_names_types,_ = decompose_lam_n sigma nb_args body1 in let n_ids,ids = @@ -1175,7 +1175,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids - | _ -> anomaly (Pp.str "anonymous argument") + | _ -> anomaly (Pp.str "anonymous argument.") ) ([],(f_id::ids)) n_names_types @@ -1302,7 +1302,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | None -> try add_suffix current_proof_name "_subproof" with e when CErrors.noncritical e -> - anomaly (Pp.str "open_new_goal with an unamed theorem") + anomaly (Pp.str "open_new_goal with an unamed theorem.") in let na = next_global_ident_away name [] in if Termops.occur_existential sigma gls_type then @@ -1313,7 +1313,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c - | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") + | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in ref_ := Value (EConstr.Unsafe.to_constr lemma); @@ -1464,7 +1464,7 @@ let (com_eqn : int -> Id.t -> let opacity = match terminate_ref with | ConstRef c -> is_opaque_constant c - | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant") + | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in let (evmap, env) = Lemmas.get_current_context() in let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 580c21d40..d66298344 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -582,7 +582,7 @@ type 'a extra_genarg_printer = hv 0 (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) - | [] -> anomaly (Pp.str "LetIn must declare at least one binding") + | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = hv 0 (str "[ " ++ diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 3ff7b53c7..b237e917d 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -113,7 +113,7 @@ let rec to_ltacprof_tactic m xml = children = List.fold_left to_ltacprof_tactic M.empty xs; } in M.add name node m - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML.") let to_ltacprof_results xml = let open Xml_datatype in @@ -125,7 +125,7 @@ let to_ltacprof_results xml = max_total = 0.0; local = 0.0; children = List.fold_left to_ltacprof_tactic M.empty xs } - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML.") let feedback_results results = Feedback.(feedback diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index dadcfb9f2..f028abde9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -236,7 +236,7 @@ end) = struct let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") - | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") + | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.") | _, [] -> (match finalcstr with | None | Some (_, None) -> @@ -1424,7 +1424,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - user_err Pp.(str "fold: the term is not unfoldable !") + user_err Pp.(str "fold: the term is not unfoldable!") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 2d2dcd0c0..efb7e780d 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -24,7 +24,7 @@ let register_alias key tac = let interp_alias key = try KNmap.find key !alias_map - with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) + with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key ++ str ".") let check_alias key = KNmap.mem key !alias_map @@ -55,7 +55,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = if overwrite then tac_tab := MLTacMap.remove s !tac_tab else - CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s) + CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in tac_tab := MLTacMap.add s t !tac_tab diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 594c4fa15..2c09a8b69 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -379,7 +379,7 @@ let try_interp_ltac_var coerce ist env (loc,id) = let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") + with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.") let interp_ident ist env sigma id = try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d7408e88e..0cd18ae50 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -362,7 +362,7 @@ let coq_True = lazy (init_constant "True") let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn - | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant")) + | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) @@ -630,7 +630,7 @@ let compile name kind = let id = new_id () in tag_hypothesis name id; {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly (Pp.str "compile_equation") + | _ -> anomaly (Pp.str "compile_equation.") in loop [] diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index ba8356b52..59ed8439b 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -423,7 +423,7 @@ let quote_terms env sigma ivs lc = | None -> begin match ivs.constant_lhs with | Some c_lhs -> subst_meta [1, c] c_lhs - | None -> anomaly (Pp.str "invalid inversion scheme for quote") + | None -> anomaly (Pp.str "invalid inversion scheme for quote.") end | Some var_lhs -> begin match ivs.constant_lhs with diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 4eef1b0a7..153a6a49a 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -145,7 +145,7 @@ let add_step s sub = | SI_Or_r,[p] -> I_Or_r p | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity") + | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity.") type 'a with_deps = {dep_it:'a; @@ -167,7 +167,7 @@ type state = let project = function Complete prf -> prf - | Incomplete (_,_) -> anomaly (Pp.str "not a successful state") + | Incomplete (_,_) -> anomaly (Pp.str "not a successful state.") let pop n prf = let nprf= @@ -361,7 +361,7 @@ let search_norev seq= (Arrow(f2,f3))) f1; add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in + | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in Int.Map.iter add_one seq.norev_hyps; List.rev !goals @@ -386,7 +386,7 @@ let search_in_rev_hyps seq= | Arrow (Disjunct (f1,f2),f0) -> [make_step (SD_Or(i)), [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen") + | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.") with Not_found -> search_norev seq @@ -464,7 +464,7 @@ let branching = function | _::next -> s_info.nd_branching<-s_info.nd_branching+List.length next in List.map (append stack) successors - | Complete prf -> anomaly (Pp.str "already succeeded") + | Complete prf -> anomaly (Pp.str "already succeeded.") open Pp diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 38f05978d..cca5cde15 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -47,7 +47,7 @@ let tag_arg tag_rec map subs i c = let global_head_of_constr sigma c = let f, args = decompose_app sigma c in try fst (Termops.global_of_constr sigma f) - with Not_found -> CErrors.anomaly (str "global_head_of_constr") + with Not_found -> CErrors.anomaly (str "global_head_of_constr.") let global_of_constr_nofail c = try global_of_constr c diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 6b752fb4b..67e6c7e93 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -133,7 +133,7 @@ let dC t = CastConv t (** Constructors for constr_expr *) let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> - CErrors.anomaly (str"not a CRef") + CErrors.anomaly (str"not a CRef.") let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) @@ -150,8 +150,8 @@ let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) - | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr") - | _ -> CErrors.anomaly (str"have: mixed G-C constr") + | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr.") + | _ -> CErrors.anomaly (str"have: mixed G-C constr.") let loc_ofCG = function | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s @@ -620,12 +620,12 @@ let match_upats_FO upats env sigma0 ise orig_c = let pt' = pi1 pt', pi2 pt', EConstr.Unsafe.to_constr (pi3 pt') in raise (FoundUnif (ungen_upat lhs pt' u)) with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u - | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO") + | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO.") | e when CErrors.noncritical e -> () in List.iter one_match fpats done; iter_constr_LR loop f; Array.iter loop a in - try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO") + try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO.") let prof_FO = mk_profiler "match_upats_FO";; let match_upats_FO upats env sigma0 ise c = @@ -696,11 +696,11 @@ let fixed_upat = function let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) let assert_done r = - match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called") + match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called.") let assert_done_multires r = match !r with - | None -> CErrors.anomaly (str"do_once never called") + | None -> CErrors.anomaly (str"do_once never called.") | Some (n, xs) -> r := Some (n+1,xs); try List.nth xs n with Failure _ -> raise NoMatch @@ -757,7 +757,7 @@ let source () = match upats_origin, upats with | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat rule ++ spc() | _, [] | None, _::_::_ -> - CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in let on_instance, instances = let instances = ref [] in (fun x -> @@ -795,7 +795,7 @@ let rec uniquize = function errorstrm (source () ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> - CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in errorstrm (str"all matches of "++source()++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); @@ -833,7 +833,7 @@ let rec uniquize = function let sigma, uc, ({up_f = pf; up_a = pa} as u) = match !upat_that_matched with | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch - | None -> CErrors.anomaly (str"companion function never called") in + | None -> CErrors.anomaly (str"companion function never called.") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ @@ -920,7 +920,7 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) when isCVar t1 -> encode k "In" [r1; r2; bind_in t1 t2] | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> CErrors.anomaly (str"where are we?") + | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] @@ -1094,7 +1094,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = (Value.cast (topwit (Option.get wit_ssrpatternarg)) v) | it -> g t with e when CErrors.noncritical e -> g t in let decodeG t f g = decode ist (mkG t) f g in - let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id) in + let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id++str".") in let cleanup_XinE h x rp sigma = let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) @@ -1280,7 +1280,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let e = match p with - | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex") + | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex.") | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in let sigma = if not resolve_typeclasses then sigma diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 80680e408..efab5b977 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -70,7 +70,7 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> @@ -162,9 +162,9 @@ let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) | Continuation (n, _, _) -> - anomaly (str "Bad number of expected remaining patterns: " ++ int n) + anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".") | Result _ -> - anomaly (Pp.str "Exhausted pattern history") + anomaly (Pp.str "Exhausted pattern history.") (* This is for non exhaustive error message *) @@ -190,7 +190,7 @@ let pop_history_pattern = function | Continuation (0, l, MakeConstructor (pci, rh)) -> feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> - anomaly (Pp.str "Constructor not yet filled with its arguments") + anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = feed_history (CAst.make @@ PatVar Anonymous) h @@ -425,7 +425,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1 let current_pattern eqn = match eqn.patterns with | pat::_ -> pat - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let alias_of_pat = CAst.with_val (function | PatVar name -> name @@ -438,7 +438,7 @@ let remove_current_pattern eqn = { eqn with patterns = pats; alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let push_current_pattern (cur,ty) eqn = match eqn.patterns with @@ -447,7 +447,7 @@ let push_current_pattern (cur,ty) eqn = { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") (* spiwack: like [push_current_pattern] but does not introduce an alias in rhs_env. Aliasing binders are only useful for variables at @@ -457,7 +457,7 @@ let push_noalias_current_pattern eqn = match eqn.patterns with | _::pats -> { eqn with patterns = pats } - | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns") + | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.") @@ -641,7 +641,7 @@ let replace_tomatch sigma n c = | Pushed (initial,((b,tm),l,na)) :: rest -> let b = replace_term sigma n c depth b in let tm = map_tomatch_type (replace_term sigma n c depth) tm in - List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l; + List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l; Pushed (initial,((b,tm),l,na)) :: replrec depth rest | Alias (initial,(na,b,d)) :: rest -> (* [b] is out of replacement scope *) @@ -882,7 +882,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl = (*****************************************************************************) let generalize_predicate sigma (names,na) ny d tms ccl = let () = match na with - | Anonymous -> anomaly (Pp.str "Undetected dependency") + | Anonymous -> anomaly (Pp.str "Undetected dependency.") | _ -> () in let p = List.length names + 1 in let ccl = lift_predicate 1 ccl tms in @@ -1708,7 +1708,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type"); + if not b then anomaly (Pp.str "Build_tycon: should be a type."); { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1872,7 +1872,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then - anomaly (Pp.str "Ill-formed 'in' clause in cases"); + anomaly (Pp.str "Ill-formed 'in' clause in cases."); List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf')) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 83c26058a..1282e3cb8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -67,7 +67,7 @@ let apply_coercion_args env evd check isproj argl funj = if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly (Pp.str "apply_coercion_args") + | _ -> anomaly (Pp.str "apply_coercion_args.") in let res = apply_rec [] funj.uj_type argl in !evdref, res @@ -368,7 +368,7 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 13e2e5d71..c93b1e568 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -425,7 +425,7 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) +let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = @@ -508,7 +508,7 @@ let rec detype flags avoid env sigma t = CAst.make @@ let body' = EConstr.of_constr body' in substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> - anomaly (str"Cannot detype an unfolded primitive projection") + anomaly (str"Cannot detype an unfolded primitive projection.") in (detype flags avoid env sigma c').CAst.v else if print_primproj_params () then diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e2106dab5..1d6b611da 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -605,7 +605,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty postpone to see if other equations help, as in: [Check fun a b c : unit => (eqáµ£efl : _ a b = _ c a b)] *) UnifFailure (i,NotSameArgSize) - | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2") + | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") and f2 i = if Evar.equal sp1 sp2 then @@ -1088,7 +1088,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 98e71c7fd..de5a62726 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -634,7 +634,7 @@ let make_projectable_subst aliases sigma evi args = cstrs) | _ -> (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)) - | _ -> anomaly (Pp.str "Instance does not match its signature")) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) @@ -828,7 +828,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = | _ -> subst' end | [] -> subst' - | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance") + | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") else subst' in Id.Map.fold is_projectable subst [] diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c4a74d990..8a902f3a3 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -296,7 +296,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f - | _,[] | [],_ -> anomaly (Pp.str "process_constr") + | _,[] | [],_ -> anomaly (Pp.str "process_constr.") in process_constr env 0 f (List.rev cstr.cs_args, recargs) @@ -533,7 +533,7 @@ let weaken_sort_scheme env evd set sort npars term ty = mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') - | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type") + | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in let ty, term = drec npars ty in !evdref, ty, term @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function in let _ = check_arities env listdepkind in mis_make_indrec env sigma listdepkind mib u - | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types") + | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 7f3bafc68..d8252ea9b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -538,7 +538,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = | Name _ -> true end - | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate") + | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate.") in srec env (EConstr.of_constr pred) arsign diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 211ffbe01..e555742bc 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable") + | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") | Misctypes.ArgArg x -> x let occurrences_of_hyp id cls = diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 10d9173f1..61118cf77 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -139,7 +139,7 @@ let type_of_var env id = let open Context.Named.Declaration in try env |> lookup_named id |> get_type with Not_found -> - anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound") + anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.") let sort_of_product env domsort rangsort = match (domsort, rangsort) with @@ -183,7 +183,7 @@ let rec nf_val env sigma v typ = try decompose_prod env typ with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let env = push_rel (LocalAssum (name,dom)) env in let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in @@ -229,7 +229,7 @@ and nf_args env sigma accu t = try decompose_prod env t with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env sigma arg dom in (subst1 c codom, c::l) @@ -246,7 +246,7 @@ and nf_bargs env sigma b t = try decompose_prod env !t with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env sigma (block_field b i) dom in t := subst1 c codom; c) @@ -357,7 +357,7 @@ and nf_predicate env sigma ind mip params v pT = try decompose_prod env pT with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in @@ -405,7 +405,7 @@ let native_norm env sigma c ty = let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); EConstr.of_constr res - | _ -> anomaly (Pp.str "Compilation failure") + | _ -> anomaly (Pp.str "Compilation failure.") let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 0818a5525..845ac4fb7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -112,14 +112,14 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") + | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> ConstRef sp | Construct (sp,_) -> ConstructRef sp | Ind (sp,_) -> IndRef sp | Var id -> VarRef id - | _ -> anomaly (Pp.str "Not a rigid reference") + | _ -> anomaly (Pp.str "Not a rigid reference.") let pattern_of_constr env sigma t = let rec pattern_of_constr env t = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b0663af70..1d12b6d51 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -199,7 +199,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = let names, _ = Global.global_universe_names () in if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) + | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") | n :: dp -> let num = int_of_string n in let dp = DirPath.make (List.map Id.of_string dp) in @@ -1149,7 +1149,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | Sort s -> ESorts.kind sigma s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev - | _ -> anomaly (Pp.str "Found a type constraint which is not a type") + | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in { utj_val = v; utj_type = s } diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5a2328aaa..c976fe66d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1445,7 +1445,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl @@ -1456,7 +1456,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.") let hnf_lam_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl @@ -1693,5 +1693,5 @@ let betazetaevar_applist sigma n c l = | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar _, _ -> applist (substl env t, stack) - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in stacklam n [] c l diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 496c706ec..a1d0977f5 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -48,7 +48,7 @@ let retype_error re = raise (RetypeError re) let anomaly_on_error f x = try f x - with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) + with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".") let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3d41d2ddd..f2b0995b0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -107,7 +107,7 @@ let destEvalRefU sigma c = match EConstr.kind sigma c with | Var id -> (EvalVar id, EInstance.empty) | Rel n -> (EvalRel n, EInstance.empty) | Evar ev -> (EvalEvar ev, EInstance.empty) - | _ -> anomaly (Pp.str "Not an unfoldable reference") + | _ -> anomaly (Pp.str "Not an unfoldable reference.") let unsafe_reference_opt_value env sigma eval = match eval with @@ -307,7 +307,7 @@ let compute_consteval_mutual_fix env sigma ref = (* Forget all \'s and args and do as if we had started with c' *) let ref,_ = destEvalRefU sigma c' in (match unsafe_reference_opt_value env sigma ref with - | None -> anomaly (Pp.str "Should have been trapped by compute_direct") + | None -> anomaly (Pp.str "Should have been trapped by compute_direct.") | Some c -> srec env (minarg-nargs) [] ref c) | _ -> (* Should not occur *) NotAnElimination in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 757e12451..7ad988ad0 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -31,7 +31,7 @@ let push_rec_types pfix env = let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty @@ -121,11 +121,11 @@ let lambda_applist_assum sigma n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match EConstr.kind sigma t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l let e_type_case_branches env evdref (ind,largs) pj c = diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index ec52da07c..b08666483 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -314,7 +314,7 @@ and nf_fun env sigma f typ = with DestKO -> (* 27/2/13: Turned this into an anomaly *) CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let body = nf_val (push_rel (LocalAssum (name,dom)) env) sigma vb codom in mkLambda(name,dom,body) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e4eb93dd9..626464b96 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -208,7 +208,7 @@ let tag_var = tag Tag.variable match expl with | None -> pr (lapp,L) a | Some (_,ExplByPos (n,_id)) -> - anomaly (Pp.str "Explicitation by position not implemented") + anomaly (Pp.str "Explicitation by position not implemented.") | Some (_,ExplByName id) -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" @@ -345,7 +345,7 @@ let tag_var = tag Tag.variable hov 1 (str "`" ++ (surround_impl b' (pr_lident (loc,id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) - |_ -> anomaly (Pp.str "List of generalized binders have alwais one element") + |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") end | Default b -> match t with @@ -423,7 +423,7 @@ let tag_var = tag Tag.variable | CLambdaN ([[na],bk,t],c) -> (na,t,c) | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c)) | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body") + | _ -> anomaly (Pp.str "ill-formed fixpoint body.") ) let rename na na' t c = @@ -438,7 +438,7 @@ let tag_var = tag Tag.variable | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c)) | CProdN ((na::nal,bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body") + | _ -> anomaly (Pp.str "ill-formed fixpoint body.") ) let rec split_fix n typ def = @@ -485,7 +485,7 @@ let tag_var = tag Tag.variable pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function - | [] -> anomaly (Pp.str "(co)fixpoint with no definition") + | [] -> anomaly (Pp.str "(co)fixpoint with no definition.") | [d1] -> pr_decl false d1 | dl -> prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ()) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6aa136b60..781af4789 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -118,7 +118,7 @@ open Decl_kinds let pr_explanation (e,b,f) = let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported") + | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") | ExplByName id -> pr_id id in let a = if f then str"!" ++ a else a in if b then str "[" ++ a ++ str "]" else a @@ -318,7 +318,7 @@ open Decl_kinds keyword (if many then "Local Parameters" else "Local Parameter") | (Global,Conjectural) -> str"Conjecture" | ((Discharge | Local),Conjectural) -> - anomaly (Pp.str "Don't know how to beautify a local conjecture") + anomaly (Pp.str "Don't know how to beautify a local conjecture.") let pr_params pr_c (xl,(c,t)) = hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ @@ -1075,7 +1075,7 @@ open Decl_kinds ) | VernacSetOpacity _ -> return ( - CErrors.anomaly (keyword "VernacSetOpacity used to set something else") + CErrors.anomaly (keyword "VernacSetOpacity used to set something else.") ) | VernacSetStrategy l -> let pr_lev = function diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 87b31849e..d6ed201d8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -157,7 +157,7 @@ let error_incompatible_inst clenv mv = (str "An incompatible instantiation has already been found for " ++ pr_id id) | _ -> - anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned") + anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.") (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = diff --git a/proofs/logic.ml b/proofs/logic.ml index cd2cfbd32..c329bdf4a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -414,7 +414,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refiner called with a meta in non app/case subterm"); + anomaly (Pp.str "refiner called with a meta in non app/case subterm."); let (sigma, t'ty) = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) @@ -474,7 +474,7 @@ and mk_hdgoals sigma goal goalacc trm = | _ -> if !check && occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refine called with a dependent meta"); + anomaly (Pp.str "refine called with a dependent meta."); let (sigma, ty) = goal_type_of env sigma trm in goalacc, ty, sigma, trm @@ -502,7 +502,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct - with Not_found -> anomaly (Pp.str "mk_casegoals") in + with Not_found -> anomaly (Pp.str "mk_casegoals.") in let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 29939294f..3fb66d1b8 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -50,7 +50,7 @@ let cook_this_proof p = match p with | { Proof_global.id;entries=[constr];persistence;universes } -> (id,(constr,universes,persistence)) - | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term") + | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof () = cook_this_proof (fst @@ -113,7 +113,7 @@ let get_current_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") + | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") let solve ?with_end_tac gi info_lvl tac pr = try diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4d2f534a7..5ec34a638 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -719,7 +719,7 @@ type state = pstate list let freeze ~marshallable = match marshallable with | `Yes -> - CErrors.anomaly (Pp.str"full marshalling of proof state not supported") + CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") | `Shallow -> !pstates | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 7cd526843..383a6a523 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -195,7 +195,7 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") | ArgArg x -> x let out_with_occurrences (occs,c) = diff --git a/stm/spawned.ml b/stm/spawned.ml index c5bd5f6f9..de19dd535 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -46,7 +46,7 @@ let control_channel = ref None let channels = ref None let init_channels () = - if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice"); + if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice."); let () = match !main_channel with | None -> () | Some (Socket(mh,mpr,mpw)) -> @@ -65,7 +65,7 @@ let init_channels () = | Some (Socket (ch, cpr, cpw)) -> controller ch cpr cpw | Some AnonPipe -> - CErrors.anomaly (Pp.str "control channel cannot be a pipe") + CErrors.anomaly (Pp.str "control channel cannot be a pipe.") let get_channels () = match !channels with diff --git a/stm/stm.ml b/stm/stm.ml index 2057496f4..1ab22f642 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -219,7 +219,7 @@ end = struct (* {{{ *) let find_proof_at_depth vcs pl = try List.find (function | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl - | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth") + | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.") | _ -> false) (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) with Not_found -> failwith "find_proof_at_depth" @@ -227,9 +227,9 @@ end = struct (* {{{ *) exception Expired let visit vcs id = if Stateid.equal id Stateid.initial then - anomaly(Pp.str "Visiting the initial state id") + anomaly(Pp.str "Visiting the initial state id.") else if Stateid.equal id Stateid.dummy then - anomaly(Pp.str "Visiting the dummy state id") + anomaly(Pp.str "Visiting the dummy state id.") else try match Vcs_.Dag.from_node (Vcs_.dag vcs) id with @@ -245,7 +245,7 @@ end = struct (* {{{ *) | [n, Sideff (ReplayCommand x); p, Noop] | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n } | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n} - | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id)) + | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id^".")) with Not_found -> raise Expired end (* }}} *) @@ -533,7 +533,7 @@ end = struct (* {{{ *) | { next = n; step = `Sideff (ReplayCommand x,_) } -> (id,Sideff (ReplayCommand x)) :: aux n | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^ - " to "^Stateid.to_string block_stop)) + " to "^Stateid.to_string block_stop^".")) in aux block_stop let slice ~block_start ~block_stop = @@ -585,11 +585,11 @@ end = struct (* {{{ *) l let create_proof_task_box l ~qed ~block_start:lemma = - if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes"); + if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes."); vcs := create_property !vcs l (ProofTask { qed; lemma }) let create_proof_block ({ block_start; block_stop} as decl) name = let l = nodes_in_slice ~block_start ~block_stop in - if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes"); + if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes."); vcs := create_property !vcs l (ProofBlock (decl, name)) let box_of id = List.map Dag.Property.data (property_of !vcs id) let delete_boxes_of id = @@ -600,7 +600,7 @@ end = struct (* {{{ *) with | [] -> None | [x] -> Some x - | _ -> anomaly Pp.(str "node with more than 1 proof task box") + | _ -> anomaly Pp.(str "node with more than 1 proof task box.") let gc () = let old_vcs = !vcs in @@ -764,13 +764,13 @@ end = struct (* {{{ *) | _ -> (* coqc has a 1 slot cache and only for valid states *) if interactive () = `No && Stateid.equal id !cur_id then () - else anomaly Pp.(str "installing a non cached state") + else anomaly Pp.(str "installing a non cached state.") let get_cached id = try match VCS.get_info id with | { state = Valid s } -> s - | _ -> anomaly Pp.(str "not a cached state") - with VCS.Expired -> anomaly Pp.(str "not a cached state (expired)") + | _ -> anomaly Pp.(str "not a cached state.") + with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = if VCS.get_state id <> Empty then () else @@ -821,7 +821,7 @@ end = struct (* {{{ *) feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id); let str_id = Stateid.to_string id in if is_cached id && not redefine then - anomaly Pp.(str"defining state "++str str_id++str" twice"); + anomaly Pp.(str"defining state "++str str_id++str" twice."); try stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); @@ -1013,7 +1013,7 @@ end = struct (* {{{ *) match info.vcs_backup with | None, _ -> anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++ - str": a state with no vcs_backup") + str": a state with no vcs_backup.") | Some vcs, _ -> VCS.restore vcs let branches_of id = @@ -1021,7 +1021,7 @@ end = struct (* {{{ *) match info.vcs_backup with | _, None -> anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++ - str": a state with no vcs_backup") + str": a state with no vcs_backup.") | _, Some x -> x let rec fold_until f acc id = @@ -1075,7 +1075,7 @@ end = struct (* {{{ *) let id = VCS.get_branch_pos (VCS.current_branch ()) in let vcs = match (VCS.get_info id).vcs_backup with - | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup") + | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.") | Some vcs, _ -> vcs in let cb, _ = try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) @@ -1838,7 +1838,7 @@ end = struct (* {{{ *) let gid = Goal.goal g in let f = try List.assoc gid res - with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in + with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in if not (Future.is_over f) then (* One has failed and cancelled the others, but not this one *) if solve then Tacticals.New.tclZEROMSG @@ -2455,7 +2455,7 @@ let handle_failure (e, info) vcs = VCS.restore vcs; VCS.print (); anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info)) + CErrors.iprint_no_report (e, info) ++ str".") | Some (safe_id, id) -> stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; @@ -2487,7 +2487,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok | VtStm ((VtJoinDocument|VtWait),_), VtLater -> - anomaly(str"classifier: join actions cannot be classified as VtLater") + anomaly(str"classifier: join actions cannot be classified as VtLater.") (* Back *) | VtStm (VtBack oid, true), w -> @@ -2515,7 +2515,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok | VtStm (VtBack id, false), VtLater -> - anomaly(str"classifier: VtBack + VtLater must imply part_of_script") + anomaly(str"classifier: VtBack + VtLater must imply part_of_script.") (* Query *) | VtQuery (false,(report_id,route)), VtNow -> @@ -2536,7 +2536,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> - anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") + anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.") (* Proof *) | VtStartProof (mode, guarantee, names), w -> @@ -2553,7 +2553,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) Proof_global.activate_proof_mode mode; Backtrack.record (); if w == VtNow then finish (); `Ok | VtProofMode _, VtLater -> - anomaly(str"VtProofMode must be executed VtNow") + anomaly(str"VtProofMode must be executed VtNow.") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in VCS.commit id (mkTransCmd x [] false `MainQueue); @@ -2642,7 +2642,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) Backtrack.record (); `Ok | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow") + anomaly(str"classifier: VtUnknown must imply VtNow.") end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) @@ -2781,7 +2781,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = s let edit_at id = - if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else + if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = let rec aux cur = @@ -2820,7 +2820,7 @@ let edit_at id = (* Hum, this should be the real start_id in the cluster and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep - | _ -> anomaly (str "ProofTask not ending with Qed") in + | _ -> anomaly (str "ProofTask not ending with Qed.") in VCS.branch ~root:master_id ~pos:id VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); VCS.delete_boxes_of id; @@ -2872,7 +2872,7 @@ let edit_at id = end else if is_ancestor_of_cur_branch id then begin backto id (Some bn) end else begin - anomaly(str"Cannot leave an `Edit branch open") + anomaly(str"Cannot leave an `Edit branch open.") end | true, None, _ -> if on_cur_branch id then begin @@ -2883,7 +2883,7 @@ let edit_at id = end else if is_ancestor_of_cur_branch id then begin backto id None end else begin - anomaly(str"Cannot leave an `Edit branch open") + anomaly(str"Cannot leave an `Edit branch open.") end | false, None, Some(_,bn) -> backto id (Some bn) | false, None, None -> backto id None @@ -2896,7 +2896,7 @@ let edit_at id = | None -> VCS.print (); anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ - CErrors.print_no_report e) + CErrors.print_no_report e ++ str ".") | Some (_, id) -> stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; diff --git a/stm/tQueue.ml b/stm/tQueue.ml index a0b08778b..fee4f35b4 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -88,7 +88,7 @@ let broadcast { lock = m; cond = c } = let push { queue = q; lock = m; cond = c; release } x = if release then CErrors.anomaly(Pp.str - "TQueue.push while being destroyed! Only 1 producer/destroyer allowed"); + "TQueue.push while being destroyed! Only 1 producer/destroyer allowed."); Mutex.lock m; PriorityQueue.push q x; Condition.broadcast c; diff --git a/stm/vcs.ml b/stm/vcs.ml index 88f860eb6..df3b8aa62 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -113,7 +113,7 @@ let add_node vcs id edges = let get_branch vcs head = try BranchMap.find head vcs.heads - with Not_found -> anomaly (str"head " ++ str head ++ str" not found") + with Not_found -> anomaly (str"head " ++ str head ++ str" not found.") let reset_branch vcs head id = let map name h = diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c4f392f20..d597f64ad 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -206,7 +206,7 @@ let rec classify_vernac e = (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () - with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)) + with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let res = static_classifier e in if Flags.is_universe_polymorphism () then diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index bcd31cb7e..507ff10ee 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -632,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (EConstr.of_constr (applist (c, Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' - | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme") + | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme.") (**********************************************************************) (* Build the right-to-left rewriting lemma for conclusion associated *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 268daf6b6..d64cc38ef 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1211,7 +1211,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = else let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with | (_sigS,[a;p]) -> (a, p) - | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in + | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in let ev = Evarutil.e_new_evar env evdref a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in diff --git a/tactics/hints.ml b/tactics/hints.ml index 48a7b3f75..70e62eaba 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -912,7 +912,7 @@ let make_resolve_hyp env sigma decl = (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] - | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") + | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.") (* REM : in most cases hintname = id *) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2ba18ceb4..d95eaabb8 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -340,7 +340,7 @@ let match_arrow_pattern sigma t = match Id.Map.bindings result with | [(m1,arg);(m2,mind)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) - | _ -> anomaly (Pp.str "Incorrect pattern matching") + | _ -> anomaly (Pp.str "Incorrect pattern matching.") let match_with_imp_term sigma c = match EConstr.kind sigma c with @@ -471,7 +471,7 @@ let match_eq_nf gls eqn (ref, hetero) = | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); (t,pf_whd_all gls x,pf_whd_all gls y) - | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") + | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.") let dest_nf_eq gls eqn = try @@ -499,7 +499,7 @@ let coq_sig_pattern = let match_sigma sigma t = match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with | [(_,a); (_,p)] -> (a,p) - | _ -> anomaly (Pp.str "Unexpected pattern") + | _ -> anomaly (Pp.str "Unexpected pattern.") let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t @@ -545,7 +545,7 @@ let match_eqdec sigma t = match Id.Map.bindings subst with | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Lazy.force op, c1, c2, typ - | _ -> anomaly (Pp.str "Unexpected pattern") + | _ -> anomaly (Pp.str "Unexpected pattern.") (* Patterns "~ ?" and "? -> False" *) let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole])) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index c495b5ece..a7eadc3c3 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -238,7 +238,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = end | LetIn (_,_,_,c), rest -> false :: analrec c rest | _, [] -> [] - | _ -> anomaly (Pp.str "compute_constructor_signatures") + | _ -> anomaly (Pp.str "compute_constructor_signatures.") in let (mib,mip) = Global.lookup_inductive ity in let n = mib.mind_nparams in @@ -613,7 +613,7 @@ module New = struct let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> anomaly (str"elimination") + | _ -> anomaly (str"elimination.") in let pmv = let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in @@ -700,7 +700,7 @@ module New = struct let make_elim_branch_assumptions ba hyps = let assums = try List.rev (List.firstn ba.nassums hyps) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in + with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in { ba = ba; assums = assums } let elim_on_ba tac ba = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2a9928a3a..a93a86d3a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1246,7 +1246,7 @@ let cut c = let error_uninstantiated_metas t clenv = let t = EConstr.Unsafe.to_constr t in let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in - let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta") + let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.") in user_err (str "Cannot find an instance for " ++ pr_id id ++ str".") let check_unresolved_evars_of_metas sigma clenv = @@ -1305,13 +1305,13 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let last_arg sigma c = match EConstr.kind sigma c with | App (f,cl) -> Array.last cl - | _ -> anomaly (Pp.str "last_arg") + | _ -> anomaly (Pp.str "last_arg.") let nth_arg sigma i c = if Int.equal i (-1) then last_arg sigma c else match EConstr.kind sigma c with | App (f,cl) -> cl.(i) - | _ -> anomaly (Pp.str "nth_arg") + | _ -> anomaly (Pp.str "nth_arg.") let index_of_ind_arg sigma t = let rec aux i j t = match EConstr.kind sigma t with @@ -4705,7 +4705,7 @@ let elim_scheme_type elim t = clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false - | _ -> anomaly (Pp.str "elim_scheme_type") + | _ -> anomaly (Pp.str "elim_scheme_type.") end } let elim_type t = diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 4e2bf4511..82f726fa7 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -62,7 +62,7 @@ Check Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). -(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *) +(* This used to fail with anomaly (Pp.str "evar was not declared.") in V8.0pl3 *) Theorem contradiction : forall p, ~ p -> p -> False. Proof. trivial. Qed. diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index cd04665cc..9bca13512 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -265,7 +265,7 @@ let main () = (* Which ocaml compiler to invoke *) let prog = if !opt then "opt" else "ocamlc" in (* Which arguments ? *) - if !opt && !top then failwith "no custom toplevel in native code !"; + if !opt && !top then failwith "no custom toplevel in native code!"; let flags = if !opt then [] else Coq_config.vmbyteflags in let topstart = if !top then [ "topstart.cmo" ] else [] in let (modules, tolink) = files_to_link userfiles in diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 8806c7356..908786565 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -85,7 +85,7 @@ module TopErr = struct let get_bols_of_loc ibuf (bp,ep) = let add_line (b,e) lines = - if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location"); + if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location."); match lines with | ([],None) -> ([], Some (b,e)) | (fl,oe) -> ((b,e)::fl, oe) diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index bf274901b..726115653 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback = - The label has not been found in the structure. This is an error *) match fallback with | Some cb -> cb - | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst) + | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".") let lookup_constant cst = try @@ -146,7 +146,7 @@ let lookup_mind_in_impl mind = let fields = memoize_fields_of_mp mp in search_mind_label lab fields with Not_found -> - anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind) + anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".") let lookup_mind mind = try Global.lookup_mind mind diff --git a/vernac/command.ml b/vernac/command.ml index 87e7e50ec..0f9dee12c 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -674,7 +674,7 @@ let extract_coercions indl = let extract_params indl = let paramsl = List.map (fun (_,params,_,_) -> params) indl in match paramsl with - | [] -> anomaly (Pp.str "empty list of inductive types") + | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); diff --git a/vernac/discharge.ml b/vernac/discharge.ml index b898f3e83..65ade7887 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -23,7 +23,7 @@ let detype_param = function | LocalAssum (Name id, p) -> id, LocalAssumEntry p | LocalDef (Name id, p,_) -> id, LocalDefEntry p - | _ -> anomaly (Pp.str "Unnamed inductive local variable") + | _ -> anomaly (Pp.str "Unnamed inductive local variable.") (* Replace diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 040c86805..021fde961 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -109,7 +109,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = let () = if not allow_uncaught && not (CErrors.handled (fst e)) then let (e, info) = e in - let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in + let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in let err = CErrors.make_anomaly msg in Util.iraise (err, info) in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 045eed3e1..77e356eb2 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -169,7 +169,7 @@ let look_for_possibly_mutual_statements = function let recguard,ordered_inds = find_mutually_recursive_statements thms in let thms = List.map pi2 ordered_inds in Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) - | [] -> anomaly (Pp.str "Empty list of theorems") + | [] -> anomaly (Pp.str "Empty list of theorems.") (* Saving a goal *) @@ -242,7 +242,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) | App (t, args) -> mkApp (body_i t, args) - | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in + | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in let body_i = body_i body in match locality with | Discharge -> @@ -402,7 +402,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let () = match thms with [_] -> () | _ -> assert false in (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with - | [] -> anomaly (Pp.str "No proof to start") + | [] -> anomaly (Pp.str "No proof to start.") | ((id,pl),(t,(_,imps)))::other_thms -> let hook ctx strength ref = let ctx = match ctx with diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 42494dd28..34b9b97d8 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -250,7 +250,7 @@ let rec find_pattern nt xl = function | _, [] -> user_err Pp.(str msg_expected_form_of_recursive_notation) | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> - anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right") + anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.") let rec interp_list_parser hd = function | [] -> [], List.rev hd @@ -271,7 +271,7 @@ let rec interp_list_parser hd = function | NonTerminal _ as x :: tl -> let xyl,tl' = interp_list_parser [x] tl in xyl, List.rev_append hd tl' - | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser") + | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.") (* Find non-terminal tokens of notation *) @@ -645,7 +645,7 @@ let make_production etyps symbols = let tkl = List.flatten (List.map (function Terminal s -> [CLexer.terminal s] | Break _ -> [] - | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in + | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in match List.assoc x etyps with | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll | ETBinder o -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index b0b35aed5..6dee95bc5 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -64,7 +64,7 @@ let subst_evar_constr evs n idf t = ev_hyps = hyps ; ev_chop = chop } = try evar_info k with Not_found -> - anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found") + anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.") in seen := Int.Set.add id !seen; (* Evar arguments are created in inverse order, @@ -325,7 +325,7 @@ type program_info = program_info_aux CEphemeron.key let get_info x = try CEphemeron.get x with CEphemeron.InvalidKey -> - CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker") + CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.") let assumption_message = Declare.assumption_message @@ -1166,7 +1166,7 @@ let next_obligation n tac = let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in let i = match Array.findi is_open obls with | Some i -> i - | None -> anomaly (Pp.str "Could not find a solvable obligation") + | None -> anomaly (Pp.str "Could not find a solvable obligation.") in solve_obligation prg i tac diff --git a/vernac/record.ml b/vernac/record.ml index 5accc8e37..f8e12f4ee 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -174,7 +174,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = let degenerate_decl decl = let id = match RelDecl.get_name decl with | Name id -> id - | Anonymous -> anomaly (Pp.str "Unnamed record variable") in + | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in match decl with | LocalAssum (_,t) -> (id, LocalAssumEntry t) | LocalDef (_,b,_) -> (id, LocalDefEntry b) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 77be7f454..c6ec89c5e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -67,7 +67,7 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () -let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO") +let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.") let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) @@ -1918,10 +1918,10 @@ let interp ?proof ?loc locality poly c = | VernacToplevelControl e -> raise e (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") + | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") + | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") + | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") + | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") |