New tactic intro. Syntax: "# n".

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index eada3bedc7a670235830309ca4cfa6d84a7bf213..4f86ff6eb06e24a74948926f906ee1a7e378fdcf 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -54,6 +54,7 @@ type ntactic =
    | NChange of loc * npattern * CicNotationPt.term
    | NElim of loc * CicNotationPt.term * npattern  
    | NId of loc
+   | NIntro of loc * string
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Higher order tactics (i.e. tacticals) *)

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index f3e3362771feea06e7f34419ffb946d732ed2619..6a493f834a1fe24b6d866c1421741dfa1cc9c809 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -96,6 +96,7 @@ let pp_ntactic ~map_unicode_to_tex = function
   | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
+  | NIntro (_,n) -> n
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ade6a3350c32090b35943f61fae9b6d698247e49..b3560150e0c9931496a5b087dd6fd4241b94e680 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -593,7 +593,8 @@ let eval_ng_tac (text, prefix_len, tac) =
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
-  | GrafiteAst.NId _ -> fun x -> x
+  | GrafiteAst.NId _ -> (fun x -> x)
+  | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 8e67c0f3e96cf0525c091a294d33a00229f880f2..821d2909a65697d365ddfa7369b34dc6ec5b79e3 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -186,6 +186,7 @@ EXTEND
         GrafiteAst.NChange (loc, what, with_what)
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NElim (loc, what, where)
+    | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
     ]
   ];
   tactic: [

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 2521498ba8f71115d0cb44638bed8be6051f226f..40a490d6bb5941bf736edbd61532e769f49acf7e 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -448,6 +448,8 @@ let exact t status goal =
  instantiate status goal t
 ;;
 
+let exact_tac t = distribute_tac (exact t) ;;
+
 let reopen status =
  let n,h,metasenv,subst,o = status.pstatus in
  let subst, newm = 
@@ -515,4 +517,8 @@ let elim_tac ~what ~where status =
    status
 ;;
 
-
+let intro_tac name =
+ exact_tac
+  ("",0,(CicNotationPt.Binder (`Lambda,
+   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
+;; 

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 6c318798e18dc7c90fc87693c57582e23c5737c0..de8c24738b1e3d177073961a7672f16e9532ac89 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -46,6 +46,6 @@ val block_tac: tactic list -> tactic
 val apply_tac: tactic_term -> tactic
 val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic
 val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic
-
+val intro_tac: string -> tactic
 
 val pp_tac_status: tac_status -> unit