From 4495bd142fb9f80b66f712ec8264f97b8ec1c258 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 17 Feb 2004 10:48:11 +0000 Subject: [PATCH] - double_type_of: sort_of_prod modified to expect also a meta - cic2acic: string_of_sort badly patched to return a "?" when a meta is found. Note: this solution is not admissible, since it generates non-valid XML files (and it may also break other things). --- helm/ocaml/cic_omdoc/cic2acic.ml | 5 ++++- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 4 ++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index ab6342b55..f45a92c1a 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -109,7 +109,10 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts C.Sort C.Prop -> "Prop" | C.Sort C.Set -> "Set" | C.Sort C.Type -> "Type" - | C.Sort C.CProp -> "CProp" + | C.Sort C.CProp -> "CProp" + | C.Meta _ -> +prerr_endline "Cic2acic: string_of_sort applied to a meta" ; + "?" | _ -> assert false in let ainnertypes,innertype,innersort,expected_available = diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 3163dfe09..3c6f4129a 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -672,6 +672,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) C.Sort s2 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (C.Meta _, C.Sort _) -> t2' + | (C.Meta _, (C.Meta (_,_) as t)) + | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> + t2' | (_,_) -> raise (NotWellTyped -- 2.39.2