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 /kernel/term.ml | |
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
```
Diffstat (limited to 'kernel/term.ml')
-rw-r--r-- | kernel/term.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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 [] |