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

[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 518f7061b12fa8fec1ac63a6d79d479c04d125f0..fc1efcd775000d784810b0a6dc3394354322aeef 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -33,7 +33,6 @@ type whd_result =
 
 type ho_whd_result =
    | Sort of int
-   | GRef of U.uri * B.term list
    | Abst of B.term
 
 (* Internal functions *******************************************************)