milestone in basic_2, λδ-2A reconstructed

[helm.git] / helm / software / components / cic_proof_checking / cicPp.ml

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 58f319f4a8fae7f5a91d0e4c2f9e68370d930b8e..97213404e7244a0b8c082b68b44f1d12bf14d53c 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -412,7 +412,7 @@ let rec check_rec ctx string_name =
     | Cic.Cast (te,ty) -> check_rec ctx string_name te
     | Cic.Prod (name,so,dest) -> 
        let l_string_name = check_rec ctx string_name so in
-       check_rec (name::ctx) string_name dest
+       check_rec (name::ctx) l_string_name dest
     | Cic.Lambda (name,so,dest) -> 
         let string_name =
           match name with