| C.Sort s ->
C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
subst,metasenv
- | C.Implicit -> raise (Impossible 21)
+ | C.Implicit _ -> raise (Impossible 21)
| C.Cast (te,ty) ->
let _,subst',metasenv' =
type_of_aux subst metasenv context ty in
| Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
- with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst 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)))))
| Some t,Some (_,C.Decl ct) ->
let inferredty,subst',metasenv' =
type_of_aux subst metasenv context t
(try
CicUnification.fo_unif_subst
subst' context metasenv' inferredty ct
- with _ -> 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" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' 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)))))
| None, Some _ ->
raise (NotRefinable (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"
and sort_of_prod subst metasenv context (name,s) (t1, t2) =
let module C = Cic in
+ let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicMetaSubst.whd subst context t1 in
- let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
+ let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
* likely to know the exact value of the result e.g. if the rhs is a
* Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
- CicMkImplicit.mk_implicit metasenv [] in
+ CicMkImplicit.mk_implicit_sort metasenv in
let (subst, metasenv) =
- CicUnification.fo_unif_subst subst context metasenv
+ CicUnification.fo_unif_subst subst context_for_t2 metasenv
(C.Meta (idx,[])) t2''
in
t2'',subst,metasenv
in
let context'' = Some (name, Cic.Decl argty') :: context' in
let (metasenv, idx) =
- CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+ CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
let irl =
(Some (Cic.Rel 1))::args' @
(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2