raise (NotWellTyped "Reference to an unchecked constant")
in
match cobj with
- C.Constant (_,_,ty,_) -> ty
- | C.CurrentProof (_,_,_,ty,_) -> ty
+ C.Constant (_,_,ty,_,_) -> ty
+ | C.CurrentProof (_,_,_,ty,_,_) -> ty
| _ -> raise (WrongUriToConstant (U.string_of_uri uri))
;;
let module R = CicReduction in
let module U = UriManager in
match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
- CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty
+ CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
| CicEnvironment.UncheckedObj (C.Variable _) ->
raise (NotWellTyped "Reference to an unchecked variable")
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
raise (NotWellTyped "Reference to an unchecked inductive type")
in
match cobj with
- C.InductiveDefinition (dl,_,_) ->
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,arity,_) = List.nth dl i in
arity
| _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
raise (NotWellTyped "Reference to an unchecked constructor")
in
match cobj with
- C.InductiveDefinition (dl,_,_) ->
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
ty
with Not_found -> assert false
in
match obj with
- C.InductiveDefinition (tl,_,parsno) ->
+ C.InductiveDefinition (tl,_,parsno,_) ->
let (_,_,_,cl) = List.nth tl i in (cl,parsno)
| _ ->
raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
with Not_found -> assert false
in
- match obj with
- Cic.Constant (_,_,_,params)
- | Cic.CurrentProof (_,_,_,_,params)
- | Cic.Variable (_,_,_,params)
- | Cic.InductiveDefinition (_,params,_) ->
- List.map
- (function uri ->
- let obj,_ =
- try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- with Not_found -> assert false
- in
- match obj with
- Cic.Variable (_,None,ty,_) -> uri,ty
- | _ -> assert false (* the theorem is well-typed *)
- ) params
+ let params = CicUtil.params_of_obj obj in
+ List.map
+ (function uri ->
+ let obj,_ =
+ try
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ Cic.Variable (_,None,ty,_,_) -> uri,ty
+ | _ -> assert false (* the theorem is well-typed *)
+ ) params
in
let rec check uris_and_types subst =
match uris_and_types,subst with