Refinement of Fix and CoFix now implemented.

diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml
index 8d6ef6295dfb461a2a9da6ab438088d534d8a835..122409df907941fd9906b6438cec03bc1109c00c 100644 (file)
--- a/helm/gTopLevel/oldDisambiguate.ml
+++ b/helm/gTopLevel/oldDisambiguate.ml
@@ -166,13 +166,7 @@ module Make(C:Callbacks) =
           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
           | _ ->