From: Stefano Zacchiroli Date: Tue, 1 Feb 2005 17:56:54 +0000 (+0000) Subject: removed useless parameter uri from mml_of_cic_object X-Git-Tag: V_0_1_0~67 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f38e8fafcf040258b54b4032562753a876a8a94e;p=helm.git removed useless parameter uri from mml_of_cic_object --- diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index 4d1a65069..6c0b0cddf 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -48,9 +48,8 @@ let mml_of_cic_sequent metasenv sequent = Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (asequent, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) -;; -let mml_of_cic_object uri obj = +let mml_of_cic_object obj = let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli index f7d3d2da2..fc5fd547a 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.mli +++ b/helm/ocaml/cic_transformations/applyTransformation.mli @@ -33,7 +33,7 @@ (* *) (***************************************************************************) -val mml_of_cic_sequent : +val mml_of_cic_sequent: Cic.metasenv -> (* metasenv *) Cic.conjecture -> (* sequent *) Gdome.document * (* Math ML *) @@ -43,9 +43,8 @@ val mml_of_cic_sequent : (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) (Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *) -val mml_of_cic_object : - UriManager.uri -> (* object uri *) - Cic.obj -> (* uri *) +val mml_of_cic_object: + Cic.obj -> (* object *) Gdome.document * (* Math ML *) (Cic.annobj * (* annobj *) ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)