C.Var (uri,exp_named_subst')
| C.Meta _ -> assert false
| C.Sort _
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
| C.Rel _
| C.Meta _
| C.Sort _
- | C.Implicit -> true
+ | C.Implicit _ -> true
| C.Cast (te,ty) ->
does_not_occur context n nn te && does_not_occur context n nn ty
| C.Prod (name,so,dest) ->
| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _ (*CSC ??? *) ->
raise (AssertFailure "3") (* due to type-checking *)
| C.Prod (name,so,de) ->
eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
in
(te, k + 1, context')
- | (_, _) -> raise (AssertFailure "9")
+ | (n, te) ->
+ raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
and check_is_really_smaller_arg context n nn kl x safes te =
| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _
(* | C.Cast (te,ty) ->
check_is_really_smaller_arg n nn kl x safes te &&
)
| C.Meta _
| C.Sort _
- | C.Implicit -> true
+ | C.Implicit _ -> true
| C.Cast (te,ty) ->
guarded_by_destructors context n nn kl x safes te &&
guarded_by_destructors context n nn kl x safes ty
| C.Rel _ -> true
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _
| C.Prod _
| C.LetIn _ ->
| C.Var _
| C.Sort _ ->
does_not_occur context n nn te
- | C.Implicit
+ | C.Implicit _
| C.Cast _ ->
raise (AssertFailure "24")(* due to type-checking *)
| C.Prod (name,so,de) ->
| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
| C.Prod (name,so,de) ->
begin
check_metasenv_consistency metasenv context canonical_context l;
CicSubstitution.lift_meta l ty
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | C.Implicit -> raise (AssertFailure "21")
+ | C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) as t ->
let _ = type_of_aux context ty in
if R.are_convertible context (type_of_aux context te) ty then
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
C.Sort s2
| (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | (_,_) ->
- raise (TypeCheckerFailure (sprintf
+ | (C.Meta _, C.Sort _) -> t2'
+ | (C.Meta _, C.Meta (_,[]))
+ | (C.Sort _, C.Meta (_,[])) -> t2'
+ | (_,_) -> raise (TypeCheckerFailure (sprintf
"Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
(CicPp.ppterm t2')))