- grammar of // changed to move the justification inside;

  reason: that brain damaged piece of software that is CAMLP5 does a
    lookahead and then it forgets to rollback the token (why??? is it
    a bug). As a consequence matita used to work (since it parses a
    statement at a time), but not matitac (since the lookahead destroyed
    the next command)
- core_notation.moo: \frac used to be at level 90, but this is incorrect
    during parsing and incompatible with the new syntax; \frac is now
    used only in output
- minor dead code removal here and there

diff --git a/matita/components/content_pres/cicNotationLexer.ml b/matita/components/content_pres/cicNotationLexer.ml
index 21031d002fc10fba43eb915623f054d45743ecd0..e0225d72ee32af20b01e00713ae6f65405986436 100644 (file)
--- a/matita/components/content_pres/cicNotationLexer.ml
+++ b/matita/components/content_pres/cicNotationLexer.ml
@@ -52,8 +52,6 @@ let regexp we_proved = "we" utf8_blank+ "proved"
 let regexp we_have = "we" utf8_blank+ "have"
 let regexp let_rec = "let" utf8_blank+ "rec" 
 let regexp let_corec = "let" utf8_blank+  "corec"
-let regexp nlet_rec = "nlet" utf8_blank+ "rec" 
-let regexp nlet_corec = "nlet" utf8_blank+  "corec"
 let regexp ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident_start = ident_letter 
@@ -307,8 +305,6 @@ and level2_ast_token =
   lexer
   | let_rec -> return lexbuf ("LETREC","")
   | let_corec -> return lexbuf ("LETCOREC","")
-  | nlet_rec -> return lexbuf ("NLETREC","")
-  | nlet_corec -> return lexbuf ("NLETCOREC","")
   | we_proved -> return lexbuf ("WEPROVED","")
   | we_have -> return lexbuf ("WEHAVE","")
   | utf8_blank+ -> ligatures_token level2_ast_token lexbuf

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 43d03b9af5b42fc8e986978add05344f6336c9ee..d383448249bf0743bbc172103e3bb917c3b5a42c 100644 (file)
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -63,22 +63,23 @@ let rec pp_ntactic ~map_unicode_to_tex =
          (String.concat "," (List.map NotationPp.pp_term l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
   | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term what ^
-      assert false ^ " " ^ assert false
+      "...to be implemented..." ^ " " ^ "...to be implemented..."
   | NConstructor (_,None,l) -> "@ " ^
       String.concat " " (List.map NotationPp.pp_term l)
   | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
       String.concat " " (List.map NotationPp.pp_term l)
   | NCase1 (_,n) -> "*" ^ n ^ ":"
-  | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
+  | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^ 
       " with " ^ NotationPp.pp_term wwhat
   | NCut (_,t) -> "ncut " ^ NotationPp.pp_term t
 (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t
   | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *)
   | NDestruct (_,dom,skip) -> "ndestruct ..." 
   | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^
-      assert false ^ " " ^ assert false
+      "...to be implemented..." ^ " " ^ "...to be implemented..."
   | NId _ -> "nid"
   | NIntro (_,n) -> "#" ^ n
+  | NIntros (_,l) -> "#" ^ String.concat " " l
   | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term t
@@ -86,19 +87,19 @@ let rec pp_ntactic ~map_unicode_to_tex =
      (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
      " " ^ NotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
   | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
-  | NDot _ -> "##."
-  | NSemicolon _ -> "##;"
-  | NBranch _ -> "##["
-  | NShift _ -> "##|"
-  | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
-  | NPosbyname (_, s) -> "##" ^ s ^ ":"
-  | NWildcard _ -> "##*:"
-  | NMerge _ -> "##]"
+  | NDot _ -> "."
+  | NSemicolon _ -> ";"
+  | NBranch _ -> "["
+  | NShift _ -> "|"
+  | NPos (_, l) -> String.concat "," (List.map string_of_int l)^ ":"
+  | NPosbyname (_, s) -> s ^ ":"
+  | NWildcard _ -> "*:"
+  | NMerge _ -> "]"
   | NFocus (_,l) -> 
-      Printf.sprintf "##focus %s" 
+      Printf.sprintf "focus %s" 
         (String.concat " " (List.map string_of_int l))
-  | NUnfocus _ -> "##unfocus"
-  | NSkip _ -> "##skip"
+  | NUnfocus _ -> "unfocus"
+  | NSkip _ -> "skip"
   | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
   | NAssumption _ -> "nassumption"
   | NBlock (_,l) -> 

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 22a8dd2248b7b28315a3b7b8d254f7157ae7f7fd..3a9e87eea0a785e3d9c50f33f558cea2625d2842 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -340,7 +340,6 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-        prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let index_obj =
@@ -390,6 +389,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                 if nstatus#ng_mode <> `CommandMode then
                   begin
                     (*HLog.warn "error in generating projection/eliminator";*)
+                    assert(status#ng_mode = `CommandMode);
                     status, uris
                   end
                 else

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index f0da64a51586c86ee93c4b71f64894127827fb9a..0679c889539ebb5fe0101897c8b4d971e4273681 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -218,28 +218,25 @@ EXTEND
         SYMBOL <:unicode<vdash>>;
         concl = tactic_term -> (List.rev hyps,concl) ] ->
          G.NTactic(loc,[G.NAssert (loc, seqs)])
-    | IDENT "auto"; params = auto_params -> 
-        G.NTactic(loc,[G.NAuto (loc, params)])
+    (*| IDENT "auto"; params = auto_params -> 
+        G.NTactic(loc,[G.NAuto (loc, params)])*)
     | SYMBOL "/"; num = OPT NUMBER ; 
-       params = nauto_params; SYMBOL "/" ; 
-       just = OPT [ IDENT "by"; by = 
-         [ univ = tactic_term_list1 -> `Univ univ
-         | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
-         | SYMBOL "_" -> `Trace ] -> by ] ->
+       just_and_params = auto_params; SYMBOL "/" ->
+       let just,params = just_and_params in
        let depth = match num with Some n -> n | None -> "1" in
        (match just with
        | None -> 
-          G.NTactic(loc,
-            [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
+                G.NTactic(loc,
+            [G.NAuto(loc,(None,["depth",depth]@params))])
        | Some (`Univ univ) ->
-          G.NTactic(loc,
-            [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
+                G.NTactic(loc,
+            [G.NAuto(loc,(Some univ,["depth",depth]@params))])
        | Some `EmptyUniv ->
-          G.NTactic(loc,
-            [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
+                G.NTactic(loc,
+            [G.NAuto(loc,(Some [],["depth",depth]@params))])
        | Some `Trace ->
-          G.NMacro(loc,
-             G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
+                G.NMacro(loc,
+             G.NAutoInteractive (loc, (None,["depth",depth]@params))))
     | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc)
     | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
     | IDENT "screenshot"; fname = QSTRING -> 
@@ -310,18 +307,10 @@ EXTEND
          i = auto_fixed_param -> i,""
        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
               string_of_int v | v = IDENT -> v ] -> i,v ]; 
-      tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
-      (* (match tl with Some l -> l | None -> []), *)
-      params
-   ]
-];
-  nauto_params: [
-    [ params = 
-      LIST0 [
-         i = auto_fixed_param -> i,""
-       | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
-              string_of_int v | v = IDENT -> v ] -> i,v ] ->
-      params
+      just = OPT [ IDENT "by"; by = 
+        [ univ = tactic_term_list1 -> `Univ univ
+        | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
+        | SYMBOL "_" -> `Trace ] -> by ] -> just,params
    ]
 ];
 

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 5080e34bf49a66ef57ffb51fe38dd52b112dbc46..95a9e713d7390a0c2b424deaf3562ae304588336 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1740,7 +1740,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
                 oldstatus#set_status s 
   in
   let s = up_to depth depth in
-    print (print_stat statistics);
+    debug_print (print_stat statistics);
     debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
     debug_print(lazy

diff --git a/matita/matita/core_notation.moo b/matita/matita/core_notation.moo
index 6f5d78d033bcbd223e2ba1e36f759e0451289ab2..8ba56a73de06f9c459c44b7ea5ec7da42dab0e9f 100644 (file)
--- a/matita/matita/core_notation.moo
+++ b/matita/matita/core_notation.moo
@@ -163,7 +163,7 @@ notation "hvbox(a break \mod b)"
   left associative with precedence 55
 for @{ 'module $a $b }.
 
-notation "a \frac b" 
+notation < "a \frac b" 
   non associative with precedence 90
 for @{ 'divide $a $b }.