From f2a53622595de308048f5aaac6fe22d9ac42279d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 9 Mar 2005 10:24:03 +0000 Subject: [PATCH] added support for open terms in check --- helm/ocaml/cic_omdoc/cic2acic.ml | 2 +- helm/ocaml/cic_transformations/acic2Ast.ml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) 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)) -- 2.39.2