Cic2content split into Content and Cic2content.

[helm.git] / helm / ocaml / cic_transformations / cic2content.mli

diff --git a/helm/ocaml/cic_transformations/cic2content.mli b/helm/ocaml/cic_transformations/cic2content.mli
index 8e26bb897466a63782dcdc0f997437f21651aada..16eb5333f721cdc0973b27199bd2c56ffa361440 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2content.mli
+++ b/helm/ocaml/cic_transformations/cic2content.mli
@@ -23,84 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(**************************************************************************)
-(*                                                                        *)
-(*                           PROJECT HELM                                 *)
-(*                                                                        *)
-(*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             16/62003                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-type recursion_kind = NoRecursive | Recursive | CoRecursive;;
-
-type 
-      'term proof = 
-      { proof_name : string option;
-        proof_id   : string ;
-        proof_kind : recursion_kind ;
-        proof_context : ('term context_element) list ;
-        proof_apply_context: ('term proof) list;
-        proof_conclude : 'term conclude_item;
-      }
-and
-      'term context_element = 
-         Declaration of 'term declaration
-       | Hypothesis of 'term declaration
-       | Proof of 'term proof
-       | Definition of 'term definition
-       | Joint of 'term joint
-and
-      'term declaration =
-       { dec_name : string option;
-         dec_id : string ;
-         dec_inductive : bool;
-         dec_aref : string;
-         dec_type : 'term 
-       }
-and
-      'term definition =
-       { def_name : string option;
-         def_id : string ;
-         def_aref : string ;
-         def_term : 'term 
-       }
-and
-      'term joint =
-       { joint_id : string ;
-         joint_kind : recursion_kind ;
-         joint_defs : 'term context_element list
-       }
-and 
-      'term conclude_item =
-       { conclude_id :string; 
-         conclude_aref : string;
-         conclude_method : string;
-         conclude_args : ('term arg) list ;
-         conclude_conclusion : 'term option 
-       }
-and 
-      'term arg =
-         Aux of int
-       | Premise of premise
-       | Term of 'term
-       | ArgProof of 'term proof
-       | ArgMethod of string (* ???? *)
-and 
-      premise =
-       { premise_id: string;
-         premise_xref : string ;
-         premise_binder : string option;
-         premise_n : int option;
-       }
-;;
- 
-val acic2content : 
-    int ref ->                                (* seed *)
-    ?name:string option ->                    (* name *)
-    ids_to_inner_sorts:(Cic.id, string) Hashtbl.t ->             
-                                              (* ids_to_inner_sorts *)
-    ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t ->  
-                                              (* ids_to_inner_types *)
-    Cic.annterm ->                            (* annotated term *)
-    Cic.annterm proof
+val annobj2content :
+  ids_to_inner_sorts:(string, string) Hashtbl.t ->
+  ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t ->
+  Cic.annobj ->
+  Cic.annterm Content.cobj