new tactic constructor: @[n]

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index c84bf99fa1f250a336c79d80e6c3a85dad0af451..1d3b21392045d561ef21f7c59050790f6194e5ec 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -55,6 +55,7 @@ type ntactic =
    | NCases of loc * CicNotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term
+   | NConstructor of loc * int option
    | NElim of loc * CicNotationPt.term * npattern  
    | NGeneralize of loc * npattern
    | NId of loc

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 89c4e369901fa464e2c15070e93ff04340ededaf..0ec8b91756c9e83da6e08d27bf08988dc85e1af3 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -98,6 +98,8 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
+  | NConstructor (_,None) -> "@"
+  | NConstructor (_,Some x) -> "@" ^ string_of_int x
   | NCase1 (_,n) -> "*" ^ n ^ ":"
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index d0d58a6fe50dc83f770ee010bdbb4c8695ef81e9..2a04b7470249205b4e39af535b8bab1a16813d70 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -653,6 +653,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NConstructor (_loc,num) -> NTactics.constructor_tac ?num
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index c92e3175f45d9f84d80aa4c88df4272db669a2bb..8232aa672abda946479f7d75ab9ed44275b49005 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -253,6 +253,9 @@ EXTEND
         G.NCases (loc, what, where)
     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
         G.NChange (loc, what, with_what)
+    | SYMBOL "@"; num = OPT NUMBER -> 
+        G.NConstructor (loc,
+           match num with None -> None | Some x -> Some (int_of_string x))
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 152c729d0d0f50ffdcc3d28c0f85c98aa1a32bd3..d8a9fba5ed84bcb0203832f97b029192ebac591b 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -573,6 +573,16 @@ let case1_tac name =
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
+let constructor ?(num=1) status goal = 
+  if num < 1 then fail (lazy "constructor numbers begin with 1");
+  let gty = get_goalty status goal in
+  let status, (r,_,_,_) = analyse_indty status gty in
+  let ref = NReference.mk_constructor num r in
+  exec (apply_tac ("",0,Ast.NRef ref)) status goal
+;;
+
+let constructor_tac ?num = distribute_tac (constructor ?num);;
+
 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
  let eq status ctx t1 t2 =

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index c81b1dd0bab0ae8e202d1dab47a1f9e5261df5ff..b282b04cace74fee82423b151dffa320b4eef57a 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -59,3 +59,5 @@ val assert_tac:
 val auto_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
+
+val constructor_tac : ?num:int -> 's NTacStatus.tactic