From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 9 Mar 2005 10:24:03 +0000 (+0000)
Subject: added support for open terms in check
X-Git-Tag: old_htmls~7
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2a53622595de308048f5aaac6fe22d9ac42279d;p=helm.git

added support for open terms in check
---

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index cf9760c25..c2a832cbe 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -116,7 +116,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
         | C.Sort (C.Type _) -> "Type" (* TASSI OK*)
         | C.Sort C.CProp -> "CProp"
         | C.Meta _       ->
-prerr_endline "Cic2acic: string_of_sort applied to a meta" ;
+(* prerr_endline "Cic2acic: string_of_sort applied to a meta" ; *)
            "?"
         | t              ->
 prerr_endline ("Cic2acic: string_of_sort applied to: " ^ CicPp.ppterm t) ;
diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 1e4914e7f..b60abf258 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -34,6 +34,7 @@ let sort_of_string = function
   | "Set" -> `Set
   | "Type" -> `Type
   | "CProp" -> `CProp
+  | "?" -> `Meta
   | _ -> assert false
 
 let get_types uri =
@@ -86,7 +87,7 @@ let ast_of_acic ids_to_inner_sorts acic =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type | `Meta -> `Pi
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))