From ab8e7d8565ef3840362bc3913e1a01f4824ee209 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 May 2008 09:43:47 +0000 Subject: [PATCH] the type of the match was obtained reducing the outtype applied to right + matched with whd ~delta:true that is not what you want. replaced with head_beta_reduce. --- 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 04d9d7224..a1a7bdea8 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -801,7 +801,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci in C.Appl (outtype'::args) in - CicReduction.whd ~subst context appl + CicReduction.head_beta_reduce ~delta:false + ~upto:(List.length args) appl in try fo_unif_subst subst context metasenv instance instance' -- 2.39.2