1. ported to camlp5

2. added a boolean to qed to governe indexing
   the syntax for disabling indexing is "qed-"

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index e34b690d311a37f16e76891c0fc6a8950d6d8d5f..4894218e8fa28ad10f78c67bc6c2ba027ca055ab 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -321,9 +321,9 @@ let extract_term_production status pattern =
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
           | Ast.List0 (_, Some l) -> 
-              Gramext.Slist0sep (s, gram_of_literal status l, true)
+              Gramext.Slist0sep (s, gram_of_literal status l)
           | Ast.List1 (_, Some l) -> 
-              Gramext.Slist1sep (s, gram_of_literal status l, true)
+              Gramext.Slist1sep (s, gram_of_literal status l)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),

diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml
index 0db31e94dd9e104cc754196796353c7f1eee0cec..bb496f2c02678a512694bcc6df43ae79853f5256 100644 (file)
--- a/matitaB/components/grafite/grafiteAst.ml
+++ b/matitaB/components/grafite/grafiteAst.ml
@@ -105,7 +105,7 @@ type command =
   | NCoercion of loc * string *
       (NotationPt.term * NotationPt.term *
         (string * NotationPt.term) * NotationPt.term) option
-  | NQed of loc
+  | NQed of loc * bool
   (* ex lexicon commands *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 

diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml
index c4993712754443227cec682337fbbc64567be17f..78bb51971e1ab5ec595f370be2b519d831d6bf95 100644 (file)
--- a/matitaB/components/grafite/grafiteAstPp.ml
+++ b/matitaB/components/grafite/grafiteAstPp.ml
@@ -167,7 +167,7 @@ let pp_ncommand status = function
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
   | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
-  | NQed (_) -> "nqed"
+  | NQed (_,_) -> "nqed"
   | NCopy (_,name,uri,map) -> 
       "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ 
         String.concat " and " 

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index c0d9baee7e56c814773cdc993337d778cba68bf3..1aa23421137610ce4943e9159581f35106946582 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -524,7 +524,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
-  | GrafiteAst.NQed loc ->
+  | GrafiteAst.NQed (loc,index) ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")
      else
@@ -559,7 +559,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
-        let index_obj =
+        let index_obj = index &&
          match obj_kind with
             NCic.Constant (_,_,_,_,(_,`Example,_))
           | NCic.Fixpoint (_,_,(_,`Example,_)) -> false
@@ -625,7 +625,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                        let _,_,menv,_,_ = invobj in
                         (match menv with
                              [] -> eval_ncommand ~include_paths opts status
-                                    ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+                                    ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
                       with _ -> (*HLog.warn "error in generating inversion principle"; *)
@@ -699,7 +699,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let status = status#set_stack ninitial_stack in
        let status = subst_metasenv_and_fix_names status in
        let status = status#set_ng_mode `ProofMode in
-       eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+       eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
   | GrafiteAst.NObj (loc,obj) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
@@ -715,7 +715,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let status = status#set_ng_mode `ProofMode in
       (match nmenv with
           [] ->
-           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,true))
         | _ -> status)
   | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
       if status#ng_mode <> `CommandMode then
@@ -776,7 +776,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        (match menv with
           [] ->
             eval_ncommand ~include_paths opts status
-             ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+             ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
         | _ -> assert false)
   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
       eval_add_constraint status [`Type,u1] [`Type,u2]

diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml
index 3e77258e0f0e2843d20dc98f0f0c96ac3190de3b..1010e2c83975fb7616bca27e58353b15887a3da1 100644 (file)
--- a/matitaB/components/grafite_parser/grafiteParser.ml
+++ b/matitaB/components/grafite_parser/grafiteParser.ml
@@ -536,7 +536,8 @@ EXTEND
      ]];
 
   grafite_ncommand: [ [
-      IDENT "qed" -> G.NQed loc
+      IDENT "qed" ;  b = OPT SYMBOL "-" -> 
+        let b = match b with None -> true | Some _ -> false in G.NQed (loc,b)
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))

diff --git a/matitaB/components/grafite_parser/print_grammar.ml b/matitaB/components/grafite_parser/print_grammar.ml
index 6bcc1468730dc9e2ef5cce86a486dccd45c9ca12..5bc87f247296fba632b30781bcef587f4a6256b3 100644 (file)
--- a/matitaB/components/grafite_parser/print_grammar.ml
+++ b/matitaB/components/grafite_parser/print_grammar.ml
@@ -87,7 +87,7 @@ and is_symbol_dummy = function
   | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
   | Snterm e | Snterml (e, _) -> is_entry_dummy e
   | Slist1 x | Slist0 x -> is_symbol_dummy x
-  | Slist1sep (x,y,_) | Slist0sep (x,y,_) -> is_symbol_dummy x && is_symbol_dummy y
+  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
   | Sopt x -> is_symbol_dummy x
   | Sself | Snext -> false
   | Stree t -> is_tree_dummy t
@@ -186,7 +186,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]} @ ";
         todo
-    | Slist0sep (symbol,sep,_) ->
+    | Slist0sep (symbol,sep) ->
         Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "{@[<hov2> ";
@@ -200,7 +200,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]}+ @ ";
         todo 
-    | Slist1sep (symbol,sep,_) ->
+    | Slist1sep (symbol,sep) ->
         let todo = visit_symbol symbol todo is_son  in
         Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol sep todo is_son in