From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 30 Jan 2004 08:13:29 +0000 (+0000)
Subject: Refinement of Fix and CoFix now implemented.
X-Git-Tag: V_0_2_3~121
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8c9f88c2c310e303dba976bf37b2eb755798268;p=helm.git

Refinement of Fix and CoFix now implemented.
---

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