X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=236f5778e86394317930eababfede4aaedc8fb3e;hb=0c302a9fda708e5019e48d14c5419a8a65190745;hp=2417f718b8e4576fca9ffc16a6024a456a615e1c;hpb=21478bf4534374bb3c2c131acb096c7d3ffc2058;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 2417f718b..236f5778e 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -17,6 +17,9 @@ module E = NCicEnvironment
 
 exception AssertFailure of string Lazy.t;;
 
+let debug = ref false;;
+let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+
 module type Strategy = sig
   type stack_term
   type env_term
@@ -58,7 +61,7 @@ module CallByValueByNameForUnwind' : Strategy = struct
    lazy (fst (reduce ~delta:0 c)), 
    (fun delta -> fst (reduce ~delta c)),
    lazy (unwind c)
-  let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta 
+  let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
   let from_stack_list_for_unwind ~unwind:_ l = 
    List.map (fun (_,_,c) -> Lazy.force c) l
   let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
@@ -266,12 +269,14 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 =
        when (Ref.eq r1 r2 && 
          List.length (E.get_relevance r1) >= List.length tl1) ->
      let relevance = E.get_relevance r1 in
+(* if the types were convertible the following optimization is sound
      let relevance = match r1 with
          | Ref.Ref (_,Ref.Con (_,_,lno)) ->
              let _,relevance = HExtlib.split_nth lno relevance in
                HExtlib.mk_list false lno @ relevance
          | _ -> relevance
      in
+*)
      (try
          HExtlib.list_forall_default3_var
           (fun t1 t2 b -> not b || aux true context t1 t2 )
@@ -428,6 +433,7 @@ type machine = int * environment_item list * NCic.term * stack_item list
 
 let reduce_machine = R.reduce
 let from_stack = RS.from_stack
+let from_env = RS.from_env
 let unwind = R.unwind
 
 let _ =