The unification does not longer use the refiner (urrah!)

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index a74946f1e24580f03b34cdc8f3685979925f801a..656955808d5abaa231668c99ede556c9325627ac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -811,6 +811,4 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
-NCicUnification.set_refiner_typeof typeof;;
-
 (* vim:set foldmethod=marker: *)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 3d89161b3220a770e69582e09da11271267377f5..cf44ff4708946917e62fd397479caea6af471365 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -15,11 +15,6 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
-let refiner_typeof =
- ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);;
-let set_refiner_typeof f = refiner_typeof := f
-;;
-
 let (===) x y = Pervasives.compare x y = 0 ;;
 
 let uncert_exc metasenv subst context t1 t2 = 

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index c442306d7a9c4517d3e363ca9a6d25a4d7923af3..13de7f4433337c21babf78856df4686091d94b4e 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -15,13 +15,6 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
-val set_refiner_typeof:
- (NRstatus.status ->
-   ?localise:(NCic.term -> Stdpp.location) ->
-   NCic.metasenv -> NCic.substitution -> NCic.context ->
-   NCic.term -> NCic.term option -> (* term, expected type *)
-     NCic.metasenv * NCic.substitution * NCic.term * NCic.term) -> unit
-
 val unify :
   #NRstatus.status ->
   ?test_eq_only:bool -> (* default: false *)