snapshot, notably:

[helm.git] / helm / matita / matitaCicMisc.mli

diff --git a/helm/matita/matitaCicMisc.mli b/helm/matita/matitaCicMisc.mli
index 61111aaf18a2eb01dac2c06f6fb71db5fffe33f6..3d0de435fa83961b518238a431923818a6011c65 100644 (file)
--- 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