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

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

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 =