added support for open terms in check

[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 1e4914e7f9bbbf250830d44654710119e3df65c0..b60abf25886ea34a60658fba9f21d7926a180e5d 100644 (file)
--- 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))