diff options
author | 2013-01-28 21:05:35 +0000 | |
---|---|---|
committer | 2013-01-28 21:05:35 +0000 | |
commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /plugins/cc | |
parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc')
-rw-r--r-- | plugins/cc/ccalgo.ml | 18 | ||||
-rw-r--r-- | plugins/cc/ccproof.ml | 4 |
2 files changed, 11 insertions, 11 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 21077ecc8..a85c80a79 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -51,7 +51,7 @@ module ST=struct let enter t sign st= if Hashtbl.mem st.toterm sign then - anomaly "enter: signature already entered" + anomaly ~label:"enter" (Pp.str "signature already entered") else Hashtbl.replace st.toterm sign t; Hashtbl.replace st.tosign t sign @@ -272,7 +272,7 @@ let find uf i= find_aux uf [] i let get_representative uf i= match uf.map.(i).clas with Rep r -> r - | _ -> anomaly "get_representative: not a representative" + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") let find_pac uf i pac = PacMap.find pac (get_representative uf i).constructors @@ -280,7 +280,7 @@ let find_pac uf i pac = let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly "get_constructor: not a constructor" + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") let size uf i= (get_representative uf i).weight @@ -325,7 +325,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 "subterms: 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) @@ -402,7 +402,7 @@ let rec canonize_name c = let build_subst uf subst = Array.map (fun i -> try term uf i - with _ -> anomaly "incomplete matching") subst + with _ -> anomaly (Pp.str "incomplete matching")) subst let rec inst_pattern subst = function PVar i -> @@ -657,8 +657,8 @@ let process_constructor_mark t i rep pac state = {lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)} state.combine; f (n-1) q1 q2 - | _-> anomaly - "add_pacs : weird error in injection subterms merge" + | _-> anomaly ~label:"add_pacs" + (Pp.str "weird error in injection subterms merge") in f cinfo.ci_nhyps opac.args pac.args | Partial_applied | Partial _ -> add_pac rep pac t; @@ -750,7 +750,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 "wrong incomplete class" + | _ -> anomaly (Pp.str "wrong incomplete class") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes @@ -890,7 +890,7 @@ let find_instances state = check_for_interrupt (); do_match state res pb_stack done; - anomaly "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 25c01f2bd..5244dcf17 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 "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 "nth_arg: 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); |