- sync with the new ApplyTransformation API

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 03803c2b94073eb3e5a72517fcda403e6b36516e..1086d5a667c2efa53aa673bb7ea98b2b25df7cc6 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -105,8 +105,8 @@ class proof_viewer obj =
     method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
       let uri = unopt_uri uri_opt in
       let obj = cicCurrentProof proof in
-      let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
-           ids_to_hypotheses)) =
+      let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+           ids_to_hypotheses,_,_))) =
         ApplyTransformation.mml_of_cic_object uri obj
       in
       current_infos <- Some (ids_to_terms, ids_to_father_ids,
@@ -176,7 +176,7 @@ class sequent_viewer obj =
     in
 *)
     let sequent = CicUtil.lookup_meta metano metasenv in
-    let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses)) =
+    let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);