aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-31 12:30:50 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-02 20:06:05 -0400
commit6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch)
tree7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 /engine/evd.ml
parent42d510ceea82d617ac4e630049d690acbe900688 (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 ```
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml22
1 files changed, 11 insertions, 11 deletions
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 *)