From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Dec 2003 14:42:06 +0000 (+0000)
Subject: Bug commented out. The comment is also commented.
X-Git-Tag: V_0_5_1_3~50
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=23bc3ec624eaf3051da7465002d33526df604898;p=helm.git

Bug commented out. The comment is also commented.
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 8ba84c74c..dd33f3e44 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -92,10 +92,16 @@ let delift context metasenv l t =
              (*CSC: first order unification. Does it help or does it harm? *)
              deliftaux k (S.lift m t)
           | Some (_,C.Decl t) ->
-             (* It may augment to_be_restricted *)
-             (*CSC: Really? Even in the case of well-typed terms?      *)
-             (*CSC: I am no longer sure of the usefulness of the check *)
-             ignore (deliftaux k (S.lift m t)) ;
+             (*CSC: The following check seems to be wrong!             *)
+             (*CSC: B:Set |- ?2 : Set                                  *)
+             (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x                 *)
+             (*CSC: Why should I restrict ?2 over B? The instantiation *)
+             (*CSC: ?1 := A is perfectly reasonable and well-typed.    *)
+             (*CSC: Thus I comment out the following two lines that    *)
+             (*CSC: are the incriminated ones.                         *)
+             (*(* It may augment to_be_restricted *)
+               ignore (deliftaux k (S.lift m t)) ;*)
+             (*CSC: end of bug commented out                           *)
              C.Rel ((position (m-k) l) + k)
           | None -> raise RelToHiddenHypothesis)
      | C.Var (uri,exp_named_subst) ->