X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=56e98775f31caf7276303a091dbeb22612128046;hb=0c8963a0f3aef05cf4866e8bcd3fdbebddac8b87;hp=dd1e57f91f3372c94c66151fd6464fcd334c2124;hpb=a031240cd6e2e0dcd6936eca6e535f3c55d0b91a;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index dd1e57f91..56e98775f 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -602,22 +602,6 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
           (function t -> RS.compute_to_stack ~reduce ~unwind (k,e,ens,t,[])) tl
         in
          reduce (k, e, ens, he, (List.append tl') s)
-  (* CSC: Old Dead Code 
-     | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) 
-     | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)  
-     | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) 
-     | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
-  (* strict evaluation, but constants are NOT unfolded *)
-        let red =
-         function
-            C.Const _ as t -> unwind k e ens t
-          | t -> reduce (k,e,ens,t,[])
-        in
-         let tl' = List.map red tl in
-          reduce (k, e, ens, he , List.append tl' s)
-     | (k, e, ens, C.Appl l, s) ->
-         C.Appl (List.append (List.map (unwind k e ens) l) s)
-  *)
      | (_, _, _, C.Const _, _) as config when delta=false-> config
      | (k, e, ens, C.Const (uri,exp_named_subst), s) as config ->
         (let o,_ = 
@@ -703,18 +687,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
           (match recparam with
               Some recparam ->
                (match reduce recparam with
-                   (* match recparam with *) 
                    (_,_,_,C.MutConstruct _,_) as config ->
-                    (* OLD 
-                    let body' =
-                     let counter = ref (List.length fl) in
-                      List.fold_right
-                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
-                       fl
-                       body
-                    in 
-                     reduce (k, e, ens, body', s) *)
-                    (* NEW *)
                     let leng = List.length fl in
                     let new_env =
                      let counter = ref 0 in
@@ -748,21 +721,11 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
    in
     reduce
   ;;
-  (*
-  let rec whd context t = 
-    try 
-      reduce context (0, [], [], t, [])
-    with Not_found -> 
-      debug_print (lazy (CicPp.ppterm t)) ; 
-      raise Not_found
-  ;;
-  *)
 
   let whd ?(delta=true) ?(subst=[]) context t = 
    unwind (reduce ~delta ~subst context (0, [], [], t, []))
   ;;
 
-  
  end
 ;;
 
@@ -783,8 +746,8 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
-(*module R = Reduction(CallByValueByNameForUnwind);; *)
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
 module U = UriManager;;
 
 let whd = R.whd
@@ -1005,13 +968,11 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
         | (_,_) -> false,ugraph
     end
   in
-    begin
-     debug t1 [t2] "PREWHD";
-     let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
-     let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
-      debug t1' [t2'] "POSTWHD";
-      aux2 test_equality_only t1' t2' ugraph
-    end
+   debug t1 [t2] "PREWHD";
+   let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+   let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
+    debug t1' [t2'] "POSTWHD";
+    aux2 test_equality_only t1' t2' ugraph
  in
   aux false (*c t1 t2 ugraph *)
 ;;