diff options
Diffstat (limited to 'plugins/xml/cic2acic.ml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 4a8436d76..2772779d4 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -12,6 +12,8 @@ (* http://helm.cs.unibo.it *) (************************************************************************) +open Pp + (* Utility Functions *) exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; @@ -162,7 +164,7 @@ let family_of_term ty = match Term.kind_of_term ty with Term.Sort s -> Coq_sort (Term.family_of_sort s) | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Errors.anomaly "family_of_term" + | _ -> Errors.anomaly (Pp.str "family_of_term") ;; module CPropRetyping = @@ -177,7 +179,7 @@ module CPropRetyping = | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Errors.anomaly "Non-functional construction" + | _ -> Errors.anomaly (Pp.str "Non-functional construction") let sort_of_atomic_type env sigma ft args = @@ -193,7 +195,7 @@ let typeur sigma metamap = match Term.kind_of_term cstr with | T.Meta n -> (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Errors.anomaly "type_of: this is not a well-typed term") + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in T.lift n ty @@ -202,7 +204,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound")) + Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -212,7 +214,7 @@ let typeur sigma metamap = | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Errors.anomaly "type_of: Bad recursive type" in + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) @@ -253,7 +255,7 @@ let typeur sigma metamap = | _, (CProp as s) -> s) | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) and sort_family_of env t = @@ -265,7 +267,7 @@ let typeur sigma metamap = | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) in type_of, sort_of, sort_family_of @@ -514,7 +516,7 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.AEvar (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML" + | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") | T.Sort s -> A.ASort (fresh_id'', s) | T.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; |