Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / grafite_parser / matitaDisambiguator.ml

diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.ml b/helm/ocaml/grafite_parser/matitaDisambiguator.ml
index 88ef32b7ae1a6816eef7d0607a7f7f6b24e9d366..5258a4963631a5662797d6f6b0ac1137534c882d 100644 (file)
--- a/helm/ocaml/grafite_parser/matitaDisambiguator.ml
+++ b/helm/ocaml/grafite_parser/matitaDisambiguator.ml
@@ -94,8 +94,8 @@ let disambiguate_thing ~aliases ~universe
       (true, library, true);
     ]
   in
-  let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
-    CoercDb.use_coercions := use_coercions;
+  let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
+    CicRefine.insert_coercions := insert_coercions;
     f ~fresh_instances ~aliases ~universe thing
   in
   let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
@@ -120,13 +120,13 @@ let disambiguate_thing ~aliases ~universe
          aux (errors @ [newerrors]) tl)
     | [] -> assert false
   in
-  let saved_use_coercions = !CoercDb.use_coercions in
+  let saved_insert_coercions = !CicRefine.insert_coercions in
   try
     let res = aux [] passes in
-    CoercDb.use_coercions := saved_use_coercions;
+    CicRefine.insert_coercions := saved_insert_coercions;
     res
   with exn ->
-    CoercDb.use_coercions := saved_use_coercions;
+    CicRefine.insert_coercions := saved_insert_coercions;
     raise exn
 
 type disambiguator_thing =