From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Dec 2008 20:44:31 +0000 (+0000)
Subject: Stupid bug fixed: checkin the type in place of the sort during the refinement
X-Git-Tag: make_still_working~4367
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77b7183419692c82f47edb94826d0015634444cc;p=helm.git

Stupid bug fixed: checkin the type in place of the sort during the refinement
of axioms.
---

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 "")))