EXPERIMENTAL COMMIT (by CSC,actuall :-)

[helm.git] / helm / software / components / ng_refiner / nCicUnifHint.ml

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 9bd934c3b05ba86927634e925555a7bb84aba0a8..9532ba985e67553e771ec495c032757226ea22fd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -62,9 +62,7 @@ let index_hint hdb context t1 t2 precedence =
 
 let empty_db = DB.empty ;;
 
-let user_db = ref empty_db ;;
-
-let add_user_provided_hint t precedence =
+let add_user_provided_hint db t precedence =
   let u = UriManager.uri_of_string "cic:/foo/bar.con" in
   let c, a, b = 
     let rec aux ctx = function
@@ -80,7 +78,7 @@ let add_user_provided_hint t precedence =
     in
       aux [] (fst (OCic2NCic.convert_term u t))
   in
-  user_db := index_hint !user_db c a b precedence
+   index_hint db c a b precedence
 ;;
 
 let db () = 
@@ -139,10 +137,13 @@ let db () =
           else [])
       [] (CoercDb.to_list (CoercDb.dump ()))
   in
+  prerr_endline "MISTERO";
+  assert false (* ERA
   List.fold_left 
     (fun db -> function 
      | (ctx,b1,b2) -> index_hint db ctx b1 b2 0)
     !user_db (List.flatten hints)
+*)
 ;;
 
 let saturate ?(delta=0) metasenv subst context ty goal_arity =