basic_rg: reduction was not tail recursive by mistake

[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index a05d4b5d682b7333c26b182fd76c4ba139ccda99..b7eb88f6395ee4f3fd0a5dbb24f4d6d9450b8907 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -120,6 +120,7 @@ let rec ho_whd f c m x =
       | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w  
       | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
       | LRef_ (_, None)        -> assert false
+      | GRef_ (_, _, Y.Void)   -> assert false
    in
    whd aux c m x