From 1c950d8cfe400f6b68eee7a67c555549db3a4d36 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 6 Apr 2009 20:40:43 +0000
Subject: [PATCH] New tactic clear; new syntax # _; to introduce and
 immediately clear an hypothesis.

---
 .../components/binaries/transcript/.depend    |  5 ++++
 .../grafite_parser/grafiteParser.ml           |  1 +
 helm/software/components/ng_kernel/.depend    |  1 +
 .../components/ng_refiner/nCicRefiner.ml      |  2 +-
 .../components/ng_refiner/nCicUnification.ml  |  2 +-
 .../components/ng_tactics/nTactics.ml         | 29 +++++++++++++++++--
 6 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 660edb2f5..8121968e9 100644
--- 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 b20ca85ba..8f37c918e 100644
--- 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 5d08f2d21..bb269130e 100644
--- 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 f79b45841..8c5dcae76 100644
--- 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 22f896f21..3000b7311 100644
--- 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 52a82af69..250d50ce3 100644
--- 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 =
-- 
2.39.2