X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_cic_content%2FnTermCicContent.mli;h=d691acdec402bd11cc3f56f173dc47383065d2fc;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=2a1d7bcc7c613dd1c07c7652d5cf15eef438a0d5;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli
index 2a1d7bcc7..d691acdec 100644
--- a/matita/components/ng_cic_content/nTermCicContent.mli
+++ b/matita/components/ng_cic_content/nTermCicContent.mli
@@ -31,15 +31,15 @@ type interpretation_id
 
 val add_interpretation:
   string ->                                       (* id / description *)
-  string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
-  CicNotationPt.cic_appl_pattern ->               (* level 3 pattern *)
+  string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
+  NotationPt.cic_appl_pattern ->               (* level 3 pattern *)
     interpretation_id
 
   (** @raise Interpretation_not_found *)
 val lookup_interpretations:
   string -> (* symbol *)
-    (string * CicNotationPt.argument_pattern list *
-      CicNotationPt.cic_appl_pattern) list
+    (string * NotationPt.argument_pattern list *
+      NotationPt.cic_appl_pattern) list
 
 exception Interpretation_not_found
 
@@ -56,9 +56,9 @@ val set_active_interpretations: interpretation_id list -> unit
 
 val ast_of_acic:
   output_type:[`Pattern|`Term] ->
-  (Cic.id, CicNotationPt.sort_kind) Hashtbl.t ->    (* id -> sort *)
+  (Cic.id, NotationPt.sort_kind) Hashtbl.t ->    (* id -> sort *)
   Cic.annterm ->                                    (* acic *)
-    CicNotationPt.term                              (* ast *)
+    NotationPt.term                              (* ast *)
     * (Cic.id, UriManager.uri) Hashtbl.t            (* id -> uri *)
 
   (** {2 content -> acic} *)
@@ -69,7 +69,7 @@ val instantiate_appl_pattern:
   mk_appl:('term list -> 'term) -> 
   mk_implicit:(bool -> 'term) ->
   term_of_uri : (UriManager.uri -> 'term) ->
-  (string * 'term) list -> CicNotationPt.cic_appl_pattern ->
+  (string * 'term) list -> NotationPt.cic_appl_pattern ->
     'term
 
 val push: unit -> unit
@@ -80,18 +80,20 @@ val pop: unit -> unit
 val nast_of_cic :
  output_type:[`Pattern | `Term ] ->
   subst:NCic.substitution -> context:NCic.context -> NCic.term ->
-   CicNotationPt.term
+   NotationPt.term
 *)
 
 type id = string
 
+val hide_coercions: bool ref
+
 val nmap_sequent:
  #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   int * NCic.conjecture ->
-   CicNotationPt.term Content.conjecture *
+   NotationPt.term Content.conjecture *
     (id, NReference.reference) Hashtbl.t    (* id -> reference *)
 
 val nmap_obj:
  #NCicCoercion.status -> NCic.obj ->
-  CicNotationPt.term Content.cobj *
+  NotationPt.term Content.cobj *
    (id, NReference.reference) Hashtbl.t    (* id -> reference *)