| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
List.fold_left
| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
List.fold_left
- | Ast.Theorem (_,_,ty,bo) ->
+ | Ast.Theorem (_,_,ty,bo,_) ->
~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
in refine_profiler.HExtlib.profile foo ()
with
| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
in refine_profiler.HExtlib.profile foo ()
with
| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))