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 /tactics | |
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 'tactics')
-rw-r--r-- | tactics/eqschemes.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 2 | ||||
-rw-r--r-- | tactics/hints.ml | 2 | ||||
-rw-r--r-- | tactics/hipattern.ml | 8 | ||||
-rw-r--r-- | tactics/tacticals.ml | 6 | ||||
-rw-r--r-- | tactics/tactics.ml | 8 |
6 files changed, 14 insertions, 14 deletions
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 = |