X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=a19bb2b25e405a83b6de8026c0c7b9b2f9795c9d;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=bd6eca4a51a377ac95096ae4a27c10516d0efa3b;hpb=34dfcf625e3ee6fac4ad4f7199055dee4edc5abb;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index bd6eca4a5..a19bb2b25 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -27,7 +27,7 @@ let apply_subst_gen ~appl_fun subst term =
           in
            C.Meta (i,l'))
     | C.Sort _ as t -> t
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
@@ -280,7 +280,7 @@ let rec force_does_not_occur subst to_be_restricted t =
       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
     | C.Rel _
     | C.Sort _ as t -> t
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Meta (n, l) ->
        (* we do not retrieve the term associated to ?n in subst since *)
        (* in this way we can restrict if something goes wrong         *)
@@ -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) ->
@@ -526,7 +516,7 @@ let delift n subst context metasenv l t =
            let l' = deliftl 1 l1 in
             C.Meta(i,l')
      | C.Sort _ as t -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)