Cic.MutCase (uri,0,outtype, Cic.Rel 1,
[mk_lambdas fields (Cic.Rel i)]))))
-let projections_of uri =
+let projections_of uri field_names =
let buri = UriManager.buri_of_uri uri in
let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
match obj with
let fields =
let rec aux =
function
- Cic.MutInd _
- | Cic.Appl _ -> []
- | Cic.Prod (Cic.Name name,s,t) -> (name,s)::aux t
- | _ -> assert false
+ Cic.MutInd _, []
+ | Cic.Appl _, [] -> []
+ | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl)
+ | _,_ -> assert false
in
- aux (CicSubstitution.lift 1 ty)
+ aux ((CicSubstitution.lift 1 ty),field_names)
in
let rec aux i =
function
- Cic.MutInd _
- | Cic.Appl _ -> []
- | Cic.Prod (Cic.Name name,s,t) ->
+ Cic.MutInd _, []
+ | Cic.Appl _, [] -> []
+ | Cic.Prod (_,s,t), name::tl ->
(match generate_one_proj uri leftparams paramsno fields s i with
- Some p ->
- let puri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
- in
- (puri,name,p) ::
- aux (i - 1)
- (CicSubstitution.subst
- (Cic.Appl
- (Cic.Const (puri,[]) ::
- CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
- ) t)
- | None -> assert false)
- | _ -> assert false
+ Some p ->
+ let puri =
+ UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+ in
+ (puri,name,p) ::
+ aux (i - 1)
+ (CicSubstitution.subst
+ (Cic.Appl
+ (Cic.Const (puri,[]) ::
+ CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
+ ) t, tl)
+ | None -> assert false)
+ | _,_ -> assert false
in
- aux (List.length fields) (CicSubstitution.lift 2 ty)
+ aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
| _ -> assert false