From 77b7183419692c82f47edb94826d0015634444cc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Dec 2008 20:44:31 +0000 Subject: [PATCH] Stupid bug fixed: checkin the type in place of the sort during the refinement of axioms. --- helm/software/components/cic_unification/cicRefine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index cf7e582e6..245c88e00 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1973,10 +1973,10 @@ let typecheck metasenv uri obj ~localization_tbl = let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph | Cic.Constant (name,None,ty,args,attrs) -> - let ty',_,metasenv,ugraph = + let ty',sort,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in - (match CicReduction.whd [] ty' with + (match CicReduction.whd [] sort with Cic.Sort _ | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph | _ -> raise (RefineFailure (lazy ""))) -- 2.39.2