cicNotationUtil: in fresh_name_generator, "\eta" replaced with "eta", which is an...

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.

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index a994c9fd166b83feb063e6e27a4cca1eed38ebaa..45fa23a0d01d3bc10329801ffccbb7b313d1c5fc 100644 (file)
--- 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 48258d7bafffc17a66d23846cdc2f2fcdb1ceb35..60fe6357d5f1c4c878187f12e086c6ce49cd3006 100644 (file)
--- 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 fc6a15b06ab989e7af19d203cecc276bd81960c9..94b38082be07c401f72fcf198a78f03d48fbb581 100644 (file)
--- 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 31cd9c576c236355b73e9335319c88c9b97d1c95..2a5af4406f5ec99fd9b3988e41eb6dc753c708bc 100644 (file)
--- 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 a941bf0883476f87144b7fdafcb3dab8ff59725d..9fb92c274f60367287ec20849e6c2ace90001c62 100644 (file)
--- 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")