From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Mar 2008 13:25:42 +0000 (+0000)
Subject: whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
X-Git-Tag: make_still_working~5544
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c036cf8b560ad40dbc06e94530af938e6f994aca;p=helm.git

whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
some operations when definitions are in the context.
Moreover, the semantics seems more reasonable (????).
---

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 7f1ec5835..532d0dc1e 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -596,19 +596,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
     function
        (k, e, _, C.Rel n, s) as config ->
         let config' =
-         try
-          Some (RS.from_env (List.nth e (n-1)))
-         with
-          Failure _ ->
-           try
-            begin
-             match List.nth context (n - 1 - k) with
-                None -> assert false
-              | Some (_,C.Decl _) -> None
-              | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
-            end
-           with
-            Failure _ -> None
+         if not delta then None
+         else
+          try
+           Some (RS.from_env (List.nth e (n-1)))
+          with
+           Failure _ ->
+            try
+             begin
+              match List.nth context (n - 1 - k) with
+                 None -> assert false
+               | Some (_,C.Decl _) -> None
+               | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
+             end
+            with
+             Failure _ -> None
         in
          (match config' with 
              Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s)