From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Dec 2008 20:29:33 +0000 (+0000)
Subject: Refinement of axioms fixed. We did not check that the declared type must be
X-Git-Tag: make_still_working~4371
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77aad924b820f7e44b222bfb36afb0a2fb1c91e2;p=helm.git

Refinement of axioms fixed. We did not check that the declared type must be
a type.
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 7b26cf6db..ad4d01065 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1976,7 +1976,10 @@ let typecheck metasenv uri obj ~localization_tbl =
      let ty',_,metasenv,ugraph =
       type_of_aux' ~localization_tbl metasenv [] ty ugraph
      in
-      Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+      (match CicReduction.whd [] ty' 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 *)