fix cache comparison relaxed to URI and not REFERENCE

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index d66f45bd1f821c8da4c202bcfac1788b970c3ed1..8298e65e3b4c14faa875a3fe6abb606ef789eb6e 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -281,8 +281,13 @@ let alpha t1 t2 ref ref' =
     | NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2
     | NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) -> 
          aux s1 s2; aux ty1 ty2; aux t1 t2
-    | NCic.Const r1, 
-      NCic.Const r2 when NReference.eq r1 ref && NReference.eq r2 ref' -> ()
+    | NCic.Const (NReference.Ref (_,uu1,_)), 
+      NCic.Const (NReference.Ref (_,uu2,_))  when 
+         let NReference.Ref (_,u1,_) = ref in
+         let NReference.Ref (_,u2,_) = ref' in
+           (uu1 == u1 && uu2 == u2) ||
+           (uu1 == u2 && uu2 == u1)
+      -> ()
     | NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> ()
     | NCic.Meta _,NCic.Meta _ -> ()
     | NCic.Implicit _,NCic.Implicit _ -> ()
@@ -321,15 +326,13 @@ let find_in_cache name obj ref =
 prerr_endline ("!!!!!!!!!!! CACHE HIT !!!!!!!!!!\n" ^
 NReference.string_of_reference ref ^ "\n" ^
 NReference.string_of_reference ref' ^ "\n"); 
-*)
+ *)
        raise (Found ref'));
-
 (*
 prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref');
-*)
-
+ *)
   ) (Hashtbl.find_all cache name);
-(*  prerr_endline "<<< CACHE MISS >>>";  *)
+(*   prerr_endline "<<< CACHE MISS >>>";   *)
   begin
     match obj, ref with 
     | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , NReference.Ref (x,y,NReference.Fix _) ->
@@ -632,7 +635,14 @@ let convert_obj_aux uri = function
             ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
          itl ([],[])
      in
-     NCic.Inductive(ind, leftno + List.length vars, itl, (`Provided, `Regular)),
+     NCic.Inductive(ind, leftno + List.length 
+       (List.filter (fun v -> 
+          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
+             Cic.Variable (_,Some _,_,_,_) -> false
+           | Cic.Variable (_,None,_,_,_) -> true
+           | _ -> assert false)
+          vars)
+       , itl, (`Provided, `Regular)),
      fix_itl
  | Cic.Variable _ 
  | Cic.CurrentProof _ -> assert false