X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaCicMisc.mli;h=3d0de435fa83961b518238a431923818a6011c65;hb=7deafec4fd4b2eebf4d4061f21ee5c47bd15b062;hp=61111aaf18a2eb01dac2c06f6fb71db5fffe33f6;hpb=51971de8dfcf257680cf38f01f9bf53d9912a498;p=helm.git

diff --git a/helm/matita/matitaCicMisc.mli b/helm/matita/matitaCicMisc.mli
index 61111aaf1..3d0de435f 100644
--- a/helm/matita/matitaCicMisc.mli
+++ b/helm/matita/matitaCicMisc.mli
@@ -37,12 +37,12 @@ val canonical_context: int -> (int * 'a * 'b) list -> 'a
   * metasenv as needed *)
 val disambiguate :
   disambiguator:MatitaTypes.disambiguator ->
-  currentProof:MatitaTypes.currentProof ->
+  currentProof:#MatitaTypes.currentProof ->
   DisambiguateTypes.term ->
     DisambiguateTypes.environment * Cic.metasenv * Cic.term *
     CicUniv.universe_graph
 
 val get_context_and_metasenv:
-  currentProof:MatitaTypes.currentProof ->
+  currentProof:#MatitaTypes.currentProof ->
     Cic.context * Cic.metasenv