From a8c9f88c2c310e303dba976bf37b2eb755798268 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 30 Jan 2004 08:13:29 +0000
Subject: [PATCH] Refinement of Fix and CoFix now implemented.

---
 helm/gTopLevel/oldDisambiguate.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

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
           | _ ->
-- 
2.39.2