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 7f1ec58359b728857fb4536258e7f33de7b934f1..532d0dc1ec374f20a0b135cbedc8495e4767f827 100644 (file)
--- 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)