| GrafiteAst.Decompose (_, names) ->
let mk_fresh_name_callback = namer_of names in
Tactics.decompose ~mk_fresh_name_callback ()
- | GrafiteAst.Demodulate _ ->
+ | GrafiteAst.Demodulate (_, params) ->
Tactics.demodulate
- ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
+ ~dbd:(LibraryDb.instance ()) ~params
+ ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
let is_a_coercion uri =
try
let obj,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in
let attrs = CicUtil.attributes_of_obj obj in
try
match List.find
let t = CicUtil.term_of_uri u in
let ty',g =
CicTypeChecker.type_of_aux'
- metasenv' [] t CicUniv.empty_ugraph
+ metasenv' [] t CicUniv.oblivion_ugraph
in
fst(CicReduction.are_convertible [] ty' ty g))
similar