Cic.Prod (nn_2_on n,convert_term k s, convert_term (k+1) t)
| NCic.Lambda (n,s,t) ->
Cic.Lambda(nn_2_on n,convert_term k s, convert_term (k+1) t)
- | NCic.LetIn (n,_,s,t) ->
- Cic.LetIn (nn_2_on n,convert_term k s, convert_term (k+1) t)
+ | NCic.LetIn (n,ty_s,s,t) ->
+ Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t)
| NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop
| NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp
- | NCic.Sort NCic.Set -> Cic.Sort Cic.Set
| NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
| NCic.Implicit _ -> assert false
| NCic.Const (NReference.Ref (_,u,NReference.Ind i)) ->
if NUri.eq u uri then
Cic.Rel (n_fl - i + k)
else
- Cic.Const (NUri.ouri_of_nuri u,[])
+ let ouri = NUri.ouri_of_nuri u in
+ let ouri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri ouri ^ "/" ^
+ UriManager.name_of_uri ouri ^ string_of_int i ^ ".con") in
+ Cic.Const (ouri,[])
| _ -> assert false
in
convert_term 0 t
| u,_,_,_,NCic.Fixpoint (is_fix, fl, _) ->
List.map
(fun nth ->
- let name = UriManager.name_of_uri (NUri.ouri_of_nuri u) in
+ let name =
+ UriManager.name_of_uri (NUri.ouri_of_nuri u) ^ string_of_int nth in
let buri = UriManager.buri_of_uri (NUri.ouri_of_nuri u) in
let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in
uri,