From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 29 Sep 2009 14:48:11 +0000 (+0000)
Subject: The unification does not longer use the refiner (urrah!)
X-Git-Tag: make_still_working~3418
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1409a972815b8e4e697d9ad55c77d9292cbea787;p=helm.git

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 a74946f1e..656955808 100644
--- 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 3d89161b3..cf44ff470 100644
--- 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 c442306d7..13de7f443 100644
--- 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 *)