- removed ancient refine exception

- s/Try every selection/Try selected/ on a button

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 786971fc11cddcecab7d6e11a6785923753135f2..3d2325c05b7cbb21d10e67dc20023615a2de12ce 100644 (file)
--- 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:")