From 14b8be2d1011ed155513aeda78b2e525d66db45f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 23 Mar 2011 01:28:29 +0000 Subject: [PATCH] Use jmeq from lib. --- matita/components/ng_refiner/nCicRefiner.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 = -- 2.39.5