X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=a2c7707493bb82baafc0561e7f6418a02ea41483;hb=9a1fa3669e18e6316df66c76a7316aa6a1826157;hp=7b26cf6db06e0666c1f92dda0e8f3bd2020bf675;hpb=567275a08875a20fa417429ecceb62df70ecbd53;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 7b26cf6db..a2c770749 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1444,11 +1444,19 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 let newt,newhety,subst,metasenv,ugraph = 
                  type_of_aux subst metasenv context c ugraph in
                 let newt, newty, subst, metasenv, ugraph = 
-                 avoid_double_coercion context subst metasenv ugraph newt expty 
+                  avoid_double_coercion context subst metasenv ugraph newt
+                    expty 
                 in
                 let subst,metasenv,ugraph = 
-                  fo_unif_subst subst context metasenv newhety expty ugraph in
-                 Some ((newt,newty), subst, metasenv, ugraph)
+                  fo_unif_subst subst context metasenv newhety expty ugraph
+                in
+                let b, ugraph =
+                  CicReduction.are_convertible ~subst context infty expty ugraph
+                in
+                if b then 
+                  Some ((t,infty), subst, metasenv, ugraph)
+                else 
+                  Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None
                | RefineFailure _ -> None)
@@ -1973,10 +1981,13 @@ 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
-      Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+      (match CicReduction.whd [] sort with
+          Cic.Sort _
+        | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+        | _ -> raise (RefineFailure (lazy "")))
   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
      assert (metasenv' = metasenv);
      (* Here we do not check the metasenv for correctness *)