]> matita.cs.unibo.it Git - helm.git/commitdiff
LetIn was missing.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 Nov 2001 18:28:16 +0000 (18:28 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 Nov 2001 18:28:16 +0000 (18:28 +0000)
helm/fix_params/cicFindParameters.ml

index 03c3e1c85be094463eff514d6e32f8f9752ef6d1..555f44e2e482ae2b0d4c67d20fdb55344b84900d 100644 (file)
@@ -64,6 +64,7 @@ let rec parameters_of te ty pparams=
      | C.Cast (te, ty) -> aux te @@ aux ty
      | C.Prod (_, s, t) -> aux s @@ aux t
      | C.Lambda (_, s, t) -> aux s @@ aux t
+     | C.LetIn (_, s, t) -> aux s @@ aux t
      | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
      | C.Const (uri,_) ->
         (* the parameters could be not exact but only possible *)