From c17dc580374628504e9c7fac7f59bd7ddf7d420e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Feb 2004 14:34:20 +0000 Subject: [PATCH] Comments (notes) removed. --- helm/ocaml/cic_unification/cicMetaSubst.ml | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index bd6eca4a5..4ee371684 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -485,16 +485,6 @@ let delift n subst 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) -> - (*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 (MetaSubstFailure "RelToHiddenHypothesis")) | C.Var (uri,exp_named_subst) -> -- 2.39.2