=
let module C = Cic in
let params =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
- match o with
- C.Constant (_,_,_,params)
- | C.CurrentProof (_,_,_,_,params)
- | C.Variable (_,_,_,params)
- | C.InductiveDefinition (_,params,_) -> params
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ CicUtil.params_of_obj o
in
let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
let next_fresh_meta = ref newmeta in
[],[] -> []
| uri::tl,[] ->
let ty =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.Variable (_,_,ty,_) ->
+ C.Variable (_,_,ty,_,_) ->
CicSubstitution.subst_vars !exp_named_subst_diff ty
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
in
in
mk_tactic (intros_tac ~mk_fresh_name_callback ())
-let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
let cut_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
term (proof, goal)
let eliminator_uri =
let buri = U.buri_of_uri uri in
let name =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tys,_,_) ->
+ C.InductiveDefinition (tys,_,_,_) ->
let (name,_,_,_) = List.nth tys typeno in
name
| _ -> assert false