parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_acic / cic2acic.mli

diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli
index b63a585e6bab0aafaa6cfc8faba6bace779f3cf6..0bf874e86fd45ae6bab8564d1ea98ed3b271b59e 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.mli
+++ b/helm/software/components/cic_acic/cic2acic.mli
@@ -31,7 +31,7 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
 
 val string_of_sort: sort_kind -> string
 (*val sort_of_string: string -> sort_kind*)
@@ -59,3 +59,10 @@ val asequent_of_sequent :
     (Cic.id, Cic.hypothesis) Hashtbl.t)    (* ids_to_hypotheses *)
 
 val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj
+
+val acic_term_of_cic_term :
+  ?eta_fix: bool ->                       (* perform eta_fixing; default: true*)
+  Cic.context -> Cic.term ->               (* term and context *)
+   Cic.annterm *                            (* annotated term *)
+    (Cic.id, sort_kind) Hashtbl.t *         (* ids_to_inner_sorts *)
+    (Cic.id, anntypes) Hashtbl.t            (* ids_to_inner_types *)