- 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).

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index ab6342b55892acf917bea708f444123b0e6dc5a7..f45a92c1ab81c355c86128a99fc7d58737d0c3a3 100644 (file)
--- 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 3163dfe09bf21804932f3a4cabefad32745e1752..3c6f4129ac805a0d2b8075b9b9db83d831b33992 100644 (file)
--- 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