X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FoldDisambiguate.ml;h=122409df907941fd9906b6438cec03bc1109c00c;hb=a8c9f88c2c310e303dba976bf37b2eb755798268;hp=8d6ef6295dfb461a2a9da6ab438088d534d8a835;hpb=e82d6ed939d9ab6b0cff9b6a469a006732d0da51;p=helm.git

diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml
index 8d6ef6295..122409df9 100644
--- 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
           | _ ->