new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes

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

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli
index a07e65cb010a53337cdc6715d83e926ffb2d96ef..ead9d511860e11abdacd22beb38f340a2cfa912d 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.mli
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli
@@ -14,7 +14,6 @@ exception LRefNotFound of Bag.message
 
 type ho_whd_result =
    | Sort of int
-   | GRef of NUri.uri * Bag.term list
    | Abst of Bag.term
 
 val ho_whd: