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

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.mli

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index 11fcbab1dd785294af545ba9745ddb5135d53276..6565a4d9f0e4887091929e8fec214662597d6a1f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -42,11 +42,11 @@ val disambiguate_tactic:
   Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
- NEstatus.extra_status ->
+ LexiconEngine.status as 'status ->
  ?baseuri:string ->
  Cic.metasenv ->
  ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
-  NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+  'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
  LexiconEngine.status ref ->
@@ -57,16 +57,16 @@ val disambiguate_macro:
 
 val disambiguate_nterm :
  NCic.term option -> 
- NEstatus.extra_status ->
+ (#NEstatus.status as 'status) ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  CicNotationPt.term Disambiguate.disambiguator_input ->
-   NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term
+   NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
- NEstatus.extra_status ->
+ #NEstatus.status as 'status ->
  ?baseuri:string ->
  (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
-  NEstatus.extra_status * NCic.obj
+  'status * NCic.obj
 
 type pattern = 
   CicNotationPt.term Disambiguate.disambiguator_input option *