X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2FdoubleTypeInference.ml;h=905d1e6bc0be63568a8998ac6936f48cb59d2a78;hb=aa791b78493b604792383cf6326877d0d53e0458;hp=ca5848369c8f735bf410d5308daa67dfe7c9c72a;hpb=1dd2a5ffce1a935d18372d298e0d85df96ef53bd;p=helm.git

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index ca5848369..905d1e6bc 100644
--- a/components/cic_acic/doubleTypeInference.ml
+++ b/components/cic_acic/doubleTypeInference.ml
@@ -51,6 +51,8 @@ let rec does_not_occur n =
   function
      C.Rel m when m = n -> false
    | C.Rel _
+(* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *)
+(*         explicit subsitutions (copied from the kernel) ???            *)
    | C.Meta _
    | C.Sort _
    | C.Implicit _ -> true