Comments (notes) removed.

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index bd6eca4a51a377ac95096ae4a27c10516d0efa3b..4ee37168450dc9fc84c409a82a40d9ef25828140 100644 (file)
--- 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) ->