From 5bd00cfdff937c2bb6c257f9c28b00ca027103e0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 26 Apr 2006 09:16:01 +0000 Subject: [PATCH] added a whd (nodelta) in the carr function used by the refiner (in the eat_prods case) to get the carrier of a coercion. this is useful in case of terms generated by paramodulation (and we want to refine the proof letting the refiner add symmetry steps) where we have ((\lambda x:A.P(x)) t) === P'(t) and P/P' is M=N/N=M --- helm/software/components/cic_unification/cicRefine.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 3443c9b6e..1f92a5fa8 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1182,7 +1182,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* we search a coercion from hety to s *) let coer, tgt_carr = let carr t subst context = - CicMetaSubst.apply_subst subst t + CicReduction.whd ~delta:false + context (CicMetaSubst.apply_subst subst t ) in let c_hety = carr hety subst context in let c_s = carr s subst context in -- 2.39.2