From 1409a972815b8e4e697d9ad55c77d9292cbea787 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 29 Sep 2009 14:48:11 +0000 Subject: [PATCH] The unification does not longer use the refiner (urrah!) --- helm/software/components/ng_refiner/nCicRefiner.ml | 2 -- helm/software/components/ng_refiner/nCicUnification.ml | 5 ----- helm/software/components/ng_refiner/nCicUnification.mli | 7 ------- 3 files changed, 14 deletions(-) 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 *) -- 2.39.2