From e82d6ed939d9ab6b0cff9b6a469a006732d0da51 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 30 Jan 2004 08:11:56 +0000 Subject: [PATCH] - removed ancient refine exception - s/Try every selection/Try selected/ on a button --- helm/ocaml/cic_disambiguation/disambiguate.ml | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 786971fc1..3d2325c05 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -54,14 +54,6 @@ let refine metasenv context term = let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in Ok (term', metasenv') with - | CicRefine.MutCaseFixAndCofixRefineNotImplemented -> - (* TODO remove this case as soon as refine is fully implemented *) - (try - debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term)); - let term' = CicTypeChecker.type_of_aux' metasenv context term in - Ok (term',metasenv) -(* with _ -> Ko) *) - with _ -> Uncertain) | CicRefine.Uncertain _ -> debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain @@ -279,7 +271,7 @@ module Make (C: Callbacks) = | [uri] -> [uri] | _ -> C.interactive_user_uri_choice ~selection_mode:`MULTIPLE - ~ok:"Try every selection." ~enable_button_for_non_vars:true + ~ok:"Try selected." ~enable_button_for_non_vars:true ~title:"Ambiguous input." ~id ~msg: ("Ambiguous input \"" ^ id ^ "\". Please, choose one or more interpretations:") -- 2.39.2