From 4a3a4a798967ddea5c537ed09e91c7218a5f67b3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 11:22:55 +0000 Subject: [PATCH] Refinement of CurrentProof did not check whether the type is a type. As a consequence it was possible to do "theorem t: 0" :-) --- helm/ocaml/cic_unification/cicRefine.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 42069ff5c..47d186dcb 100644 --- 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 -- 2.39.2