Refinement of CurrentProof did not check whether the type is a type.

As a consequence it was possible to do "theorem t: 0" :-)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 42069ff5cb92ef6d6c7266d15c0725acc737937c..47d186dcb27425dfb7cf4aab0b2b5362fd8105fd 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -995,7 +995,15 @@ let typecheck metasenv uri obj =
      assert (metasenv' = metasenv);
      (* Here we do not check the metasenv for correctness *)
      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
-     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     begin
+      match sort with
+         Cic.Sort _
+       (* instead of raising Uncertain, let's hope that the meta will become
+          a sort *)
+       | Cic.Meta _ -> ()
+       | _ -> raise (RefineFailure "The term provided is not a type")
+     end;
      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
      let bo' = CicMetaSubst.apply_subst subst bo' in
      let ty' = CicMetaSubst.apply_subst subst ty' in