- | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
+ | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
| C.Const (uri,exp_named_subst) ->
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
@@ -251,7+252,8 @@ and type_of_aux' metasenv context t =
List.nth l i , expl_params, parsno
| _ ->
raise
List.nth l i , expl_params, parsno
| _ ->
raise
- (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
let rec count_prod t =
match CicMetaSubst.whd subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
let rec count_prod t =
match CicMetaSubst.whd subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
@@ -412,7+414,7 @@ and type_of_aux' metasenv context t =
| Some t,Some (_,C.Def (ct,_)) ->
(try
fo_unif_subst subst context metasenv t ct
| Some t,Some (_,C.Def (ct,_)) ->
(try
fo_unif_subst subst context metasenv t ct
- with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
+ with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| Some t,Some (_,C.Decl ct) ->
let inferredty,subst',metasenv' =
type_of_aux subst metasenv context t
| Some t,Some (_,C.Decl ct) ->
let inferredty,subst',metasenv' =
type_of_aux subst metasenv context t
@@ -420,9+422,9 @@ and type_of_aux' metasenv context t =
(try
fo_unif_subst
subst' context metasenv' inferredty ct
(try
fo_unif_subst
subst' context metasenv' inferredty ct
- with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
+ with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| None, Some _ ->
| None, Some _ ->
- raise (NotRefinable (sprintf
+ raise (RefineFailure (sprintf
"Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
"Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"