]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.mli
first moogle template checkin
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli
index 0e05413b8d68c0aeaaad68e2c2b221e949f29f69..640549544c45c460c9724a7a72b0b13fabb5930b 100644 (file)
@@ -37,8 +37,8 @@ module Make (C : Callbacks) :
       Cic.metasenv ->
       CicAst.term ->
       aliases:environment ->  (* previous interpretation status *)
-        environment *                   (* new interpretation status *)
-        Cic.metasenv *                  (* new metasenv *)
-        Cic.term                        (* disambiguated term *)
+        (environment *                   (* new interpretation status *)
+         Cic.metasenv *                  (* new metasenv *)
+         Cic.term) list                 (* disambiguated term *)
   end