diff --git a/pieuvre.ml b/pieuvre.ml index 08fe688..2d62ce3 100644 --- a/pieuvre.ml +++ b/pieuvre.ml @@ -137,9 +137,9 @@ let rec computeType (env: gam) (l: lam) : ty option = | [] -> None end | LExf(l',t) -> - if (computeType env l')=Some t - then Some t - else None (* Le ex falso a le mauvais type *) + match (computeType env l') with + | Some TFalse -> Some t (* On applique le ExFalso *) + | _ -> None (* Le ex falso a le mauvais type *) ;; (* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)