From 6a67a0e30bdd96df994dd7d309d1f0d8cc22751f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 31 May 2017 12:30:50 -0400
Subject: 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
```
---
 plugins/cc/ccalgo.ml  | 16 ++++++++--------
 plugins/cc/ccproof.ml |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins/cc')

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);
-- 
cgit v1.2.3