DoubleTypeInference: added a comment on "does_not_occur"

[helm.git] / components / cic_acic / doubleTypeInference.ml

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index ca5848369c8f735bf410d5308daa67dfe7c9c72a..905d1e6bc0be63568a8998ac6936f48cb59d2a78 100644 (file)
--- 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