From 23bc3ec624eaf3051da7465002d33526df604898 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Dec 2003 14:42:06 +0000 Subject: [PATCH] Bug commented out. The comment is also commented. --- helm/ocaml/cic_unification/cicUnification.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) 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) -> -- 2.39.2