- let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
- ) in
- let (_,_,_,constructors) = List.nth inductive_types typeno in
+ let inductive_types,noparams =
+ (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,n,_) -> l,n
+ ) in
+ let (_,_,_,constructors) = List.nth inductive_types typeno in
+ let name_and_arities =
+ let rec count_prods =
+ function
+ C.Prod (_,_,t) -> 1 + count_prods t
+ | _ -> 0 in
+ List.map
+ (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in
+ let pp =
+ let build_proof p (name,arity) =
+ let rec make_context_and_body c p n =
+ if n = 0 then c,(aux p)
+ else
+ (match p with
+ Cic.ALambda(idl,vname,s1,t1) ->
+ let ce =
+ build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
+ make_context_and_body (ce::c) t1 (n-1)
+ | _ -> assert false) in
+ let context,body = make_context_and_body [] p arity in
+ K.ArgProof
+ {body with K.proof_name = name; K.proof_context=context} in
+ List.map2 build_proof patterns name_and_arities in