From f524a0d716de2bdc0874aace8f82f6289034eccf Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 28 Apr 2009 19:30:21 +0000
Subject: [PATCH] cicNotationUtil: in fresh_name_generator, "\eta" replaced
 with "eta", which is an identifier cicNotationPp: debug mode turned off
 logic/cprop_connectives.ma: duplicate lines removed matitaScript: missing
 "\n\n" added in front of inline output core_notation.moo: the "default"
 notation directive has a bug. Commented out.

---
 .../components/acic_content/cicNotationPp.ml  |  2 +-
 .../acic_content/cicNotationUtil.ml           |  3 +-
 helm/software/matita/core_notation.moo        | 54 ++++++++++++++++++-
 .../matita/library/logic/cprop_connectives.ma |  6 ---
 helm/software/matita/matitaScript.ml          |  2 +-
 5 files changed, 56 insertions(+), 11 deletions(-)

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index a994c9fd1..45fa23a0d 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -34,7 +34,7 @@ module Env = CicNotationEnv
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = true
+let debug_printing = false
 
 let pp_binder = function
   | `Lambda -> "lambda"
diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 48258d7ba..60fe6357d 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -362,7 +362,8 @@ let fresh_id () =
   !fresh_index
 
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name () = "η" ^ string_of_int (fresh_id ())
+  (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in
diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index fc6a15b06..94b38082b 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -1,28 +1,78 @@
+(* exists *******************************************************************)
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*
 notation < "hvbox(\exists ident i opt (: ty) break . p)"
-  right associative with precedence 20
+  with precedence 20
 for @{ 'exists ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
+*)
 
+notation > "\exists list1 ident x sep , : T. term 19 Px"
+  with precedence 20
+for 
+  @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }.
+
+notation > "\exists list1 ident x sep , . term 19 Px"
+  with precedence 20
+for 
+  @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }.
+
+(*
 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
   with precedence 20
   for ${ default
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
        }.
+*)
+
+(* sigma ********************************************************************)
 
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
-  right associative with precedence 20
+  with precedence 20
 for @{ 'sigma ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
+*)
 
+notation > "\Sigma list1 ident x sep , : T. term 19 Px"
+  with precedence 20
+for 
+  @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }.
+
+notation > "\Sigma list1 ident x sep , . term 19 Px"
+  with precedence 20
+for 
+  @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }.
+
+(*
 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
   with precedence 20
   for ${ default
           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
        }.
+*)
+
+(* other notations **********************************************************)
 
 notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
 with precedence 90 for @{ 'pair $a $b}.
diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma
index 31cd9c576..2a5af4406 100644
--- a/helm/software/matita/library/logic/cprop_connectives.ma
+++ b/helm/software/matita/library/logic/cprop_connectives.ma
@@ -75,11 +75,6 @@ interpretation "logical iff type1" 'iff1 x y = (Iff1 x y).
 
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
-  
-notation "\ll term 19 a, break term 19 b \gg" 
-with precedence 90 for @{'dependent_pair $a $b}.
-interpretation "dependent pair" 'dependent_pair a b = 
-  (ex_introT _ _ a b).
 
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 
@@ -88,7 +83,6 @@ with precedence 90 for @{'dependent_pair $a $b}.
 interpretation "dependent pair" 'dependent_pair a b = 
   (ex_introT _ _ a b).
 
-
 definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
 definition pi2exT ≝ 
   λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a941bf088..9fb92c274 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -569,7 +569,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
           raise exn
           (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
   | TA.Inline (_,style,suri,prefix,flavour) ->
-       let str = 
+       let str = "\n\n" ^ 
          ApplyTransformation.txt_of_inline_macro
           ~map_unicode_to_tex:(Helm_registry.get_bool
             "matita.paste_unicode_as_tex")
-- 
2.39.2