Comments updated with new reflections.

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 3536623287f02712a2bb21655ad02137e69b1398..1dcbed6d297e4db01a5039e9eda32879c97d4ecd 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -625,15 +625,17 @@ let delift n subst context metasenv l t =
     function
        C.Rel m -> 
          if m <=k then
-          C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
-                    (*CSC: deliftato la regola per il LetIn                 *)
-                    (*CSC: FALSO! La regola per il LetIn non lo fa          *)
+          C.Rel m
          else
           (try
             match List.nth context (m-k-1) with
                Some (_,C.Def (t,_)) ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
                 (*CSC: first order unification. Does it help or does it harm? *)
+                (*CSC: ANSWER: it hurts performances since it is possible to  *)
+                (*CSC: have an exponential explosion of the size of the proof.*)
+                (*CSC: However, without this bit of reduction some "apply" in *)
+                (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
                 deliftaux k (S.lift m t)
              | Some (_,C.Decl t) ->
                 C.Rel ((position (m-k) l) + k)