New tactic clear; new syntax # _; to introduce and immediately clear an

hypothesis.

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 660edb2f59b7408e9cc7acdc1fedca119c02be07..8121968e98a26e1c58cd7e25d809ffdd284e44d9 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend
+++ b/helm/software/components/binaries/transcript/.depend
@@ -1,5 +1,10 @@
 v8Parser.cmi: types.cmo 
 grafite.cmi: types.cmo 
+engine.cmi: 
+types.cmo: 
+types.cmx: 
+options.cmo: 
+options.cmx: 
 v8Parser.cmo: types.cmo options.cmo v8Parser.cmi 
 v8Parser.cmx: types.cmx options.cmx v8Parser.cmi 
 v8Lexer.cmo: v8Parser.cmi options.cmo 

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index b20ca85baa3c0e48fb7e04d2c0055590a610e510..8f37c918e83e8834446ddc667cb835dfc95bb04f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -189,6 +189,7 @@ EXTEND
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NElim (loc, what, where)
     | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+    | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
     | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
     | SYMBOL "*"; n=IDENT ->
         GrafiteAst.NCase1 (loc,n)

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 5d08f2d2176d9906347599fa00ff69130d86514e..bb269130e432e2a5fdb29bb602f804acc7c34483 100644 (file)
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -1,3 +1,4 @@
+nUri.cmi: 
 nReference.cmi: nUri.cmi 
 nCicUtils.cmi: nCic.cmo 
 nCicSubstitution.cmi: nCic.cmo 

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index f79b458419a9728421c21e814adf4054eade5cf0..8c5dcae76d0d700e5a93156faa32bdb5eae66ba0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -27,7 +27,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 22f896f21e12c13fa26fe2cb5d6133911385481a..3000b7311dca621bcedfc3464380621c13d3e2a6 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -86,7 +86,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let fix_sorts swap metasenv subst context meta t =
   let rec aux () = function

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 52a82af699febc4bdf9de0f50a03c6835cbba9e1..250d50ce39adb949482f89018b98c4f915cf82f4 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -305,10 +305,33 @@ let elim_tac ~what ~where status =
    status
 ;;
 
+let find_in_context name context =
+  let rec aux acc = function
+    | [] -> raise Not_found
+    | (hd,_) :: tl when hd = name -> acc
+    | _ :: tl ->  aux (acc + 1) tl
+  in
+  aux 1 context
+;;
+
+let clear name status goal =
+ let goalty = get_goalty status goal in
+ let j =
+  try find_in_context name (ctx_of goalty)
+  with Not_found -> fail (lazy ("hypothesis '" ^ name ^ "' not found")) in
+ let n,h,metasenv,subst,o = status.pstatus in
+ let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal [j] in
+  { status with pstatus = n,h,metasenv,subst,o }
+;;
+
+let clear_tac name = distribute_tac (clear name);;
+
 let intro_tac name =
- exact_tac
-  ("",0,(CicNotationPt.Binder (`Lambda,
-   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
+ block_tac
+  [ exact_tac
+    ("",0,(CicNotationPt.Binder (`Lambda,
+     (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)));
+    if name = "_" then clear_tac name else fun x -> x ]
 ;;
 
 let cases ~what status goal =