[] -> []
| Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
CicSubstitution.lift n a))] @ superlift next (n+1)
- | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
- CicSubstitution.lift n a))] @ superlift next (n+1)
+ | Some(name,Cic.Def(a,None))::next -> [Some(name,Cic.Def((
+ CicSubstitution.lift n a),None))] @ superlift next (n+1)
+ | Some(name,Cic.Def(a,Some ty))::next -> [Some(name,Cic.Def((
+ CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1)
| _::next -> superlift next (n+1) (*?? ??*)
;;