(context',ty,C.Lambda(n',s,bo))
| C.LetIn (n,s,t) ->
let (context',ty,bo) =
- collect_context ((Some (n,(C.Def s)))::context) t
+ collect_context ((Some (n,(C.Def (s,None))))::context) t
in
(context',ty,C.LetIn(n,s,bo))
| _ as t ->
match entry with
Some (n,Cic.Decl s) ->
Some (n,Cic.Decl (subst_in canonical_context' s))
- | Some (n,Cic.Def s) ->
- Some (n,Cic.Def (subst_in canonical_context' s))
+ | Some (n,Cic.Def (s,None)) ->
+ Some (n,Cic.Def ((subst_in canonical_context' s),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
in
entry'::canonical_context'
) canonical_context []
let fresh_name =
mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in
let context_for_newmeta =
- (Some (fresh_name,C.Def term))::context in
+ (Some (fresh_name,C.Def (term,None)))::context in
let irl =
identity_relocation_list_for_metavariable context_for_newmeta in
let newmetaty = CicSubstitution.lift 1 ty in
match T.type_of_aux' metasenv context ty with
C.Sort C.Prop -> "_ind"
| C.Sort C.Set -> "_rec"
+ | C.Sort C.CProp -> "_rec"
| C.Sort C.Type -> "_rect"
| _ -> assert false
in
let context' =
List.map
(function
- Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
+ Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None))
| Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context
in
let metasenv' =