diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /pretyping/evarutil.ml | |
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 'pretyping/evarutil.ml')
-rw-r--r-- | pretyping/evarutil.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index c2ba6d957..f4f373754 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -853,7 +853,7 @@ let make_projectable_subst aliases sigma evi args = cstrs) | _ -> (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) - | _ -> anomaly "Instance does not match its signature") + | _ -> anomaly (Pp.str "Instance does not match its signature")) sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) @@ -862,7 +862,7 @@ let make_pure_subst evi args = (fun (id,b,c) (args,l) -> match args with | a::rest -> (rest, (id,a)::l) - | _ -> anomaly "Instance does not match its signature") + | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) (*------------------------------------* @@ -1036,7 +1036,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = | _ -> subst' end | [] -> subst' - | _ -> anomaly "More than one non var in aliases class of evar instance" + | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance") else subst' in Id.Map.fold is_projectable subst [] @@ -1883,7 +1883,7 @@ let undefined_evars_of_term evd t = (try match (Evd.find evd n).evar_body with | Evar_empty -> Int.Set.add n acc | Evar_defined c -> evrec acc c - with Not_found -> anomaly "undefined_evars_of_term: evar not found") + with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found")) | _ -> fold_constr evrec acc c in evrec Int.Set.empty t |