From 7168611756f3a4c5793cbe978805bb2e93c66cdc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 May 2008 09:12:51 +0000 Subject: [PATCH] added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now is full whd --- .../components/cic_unification/cicUnification.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index ff5f39605..c1e9ea6bc 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -511,6 +511,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ in fo_unif_subst test_equality_only subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 + | (C.Prod _, _) -> + (match CicReduction.whd ~subst context t2 with + | C.Prod _ as t2 -> + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product")))) + | (_, C.Prod _) -> + (match CicReduction.whd ~subst context t1 with + | C.Prod _ as t1 -> + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product")))) | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> let subst',metasenv',ugraph1 = fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph -- 2.39.2