- let metasenv, term = CicMkImplicit.expand_implicits metasenv [] context term in
- debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
- try
- let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
- Ok (term', metasenv')
- with
- | CicRefine.Uncertain _ ->
- debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
- Uncertain
- | CicRefine.RefineFailure _ ->
- debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
- Ko
+ let metasenv, term =
+ CicMkImplicit.expand_implicits metasenv [] context term in
+ debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
+ try
+ let term', _, metasenv',ugraph1 =
+ CicRefine.type_of_aux' metasenv context term ugraph in
+ (Ok (term', metasenv')),ugraph1
+ with
+ | CicRefine.Uncertain _ ->
+ debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ Uncertain,ugraph
+ | CicRefine.RefineFailure msg ->
+ debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) msg);
+ Ko,ugraph