in
Ok (term,metasenv'')
with
- CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
- (try
- let term = CicTypeChecker.type_of_aux' metasenv' context expr in
- Ok (term,metasenv')
- with _ -> Ko
- )
- | CicRefine.Uncertain _ ->
+ CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
Uncertain
| _ ->