]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.mli
paths trough terms implemented with a nice hack :)
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli
index ac9b977927bb9c69a86c64198949fba1cadb4ab8..b659b38ffac13a4828ac69c8bc76364740d1c39f 100644 (file)
@@ -29,6 +29,11 @@ open DisambiguateTypes
 
 exception NoWellTypedInterpretation
 
+val interpretate:   
+    context:Cic.name list ->
+    env:DisambiguateTypes.environment -> 
+    CicAst.term -> Cic.term
+
 module type Disambiguator =
 sig
   val disambiguate_term :