(try
(match CicTypeChecker.type_of_aux' [] context typ with
C.Sort C.Prop -> "H"
+ | C.Sort C.CProp -> "H"
| C.Sort C.Set -> "x"
| _ -> "H"
)
List.map
(function
Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
+ | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context
in
i,canonical_context',(subst_in ty)
(function
None -> None
| Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
- | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t))
+ | Some (i,Cic.Def (t,None)) ->
+ Some (i,Cic.Def ((subst_in t),None))
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context
in
(m,canonical_context',subst_in ty)::i