initial implementation of `ncoercion name : type := body on name : pat to pat`

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.mli

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index 86ede901cdaf5797afe50b50026261d2bbb3cec2..ecb5926820a16be025e14c0f34f80037c2a53d56 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -31,7 +31,7 @@ val disambiguate_term :
   context:Cic.context ->
   metasenv:Cic.metasenv -> 
   subst:Cic.substitution ->
-  ?goal:int ->
+  expty:Cic.term option ->
   ?initial_ugraph:CicUniv.universe_graph -> 
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->