From: Claudio Sacerdoti Coen Date: Wed, 23 Mar 2011 01:28:29 +0000 (+0000) Subject: Use jmeq from lib. X-Git-Tag: make_still_working~2548 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=14b8be2d1011ed155513aeda78b2e525d66db45f;p=helm.git Use jmeq from lib. --- diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index 4645e6f6e..5727dae67 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/components/ng_refiner/nCicRefiner.ml @@ -598,8 +598,8 @@ and try_coercions status in (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*) - let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in - let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in + let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in + let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in let add_params metasenv subst context cty outty mty m i =