aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-05 04:23:01 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-05 04:23:01 +0000
commitf8e42d82ce5f9e8f3a8cc1294f3b9b8fab3cea50 (patch)
tree1f28eb9c881e1c6f613921b7a64627e7ee184563
parentdf2a8d8307f7594464f97bc8fda50e65eee01f8c (diff)
Fix [autounfold] to accept general [in] clauses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12843 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tactics/eauto.ml425
-rw-r--r--tactics/eauto.mli2
2 files changed, 18 insertions, 9 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index e89b61d46..0a5a9c481 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -396,7 +396,7 @@ END
let cons a l = a :: l
-let autounfold db cl =
+let autounfolds db occs =
let unfolds = List.concat (List.map (fun dbname ->
let db = try searchtable_map dbname
with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
@@ -404,7 +404,15 @@ let autounfold db cl =
let (ids, csts) = Hint_db.unfolds db in
Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts
(Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db)
- in unfold_option unfolds cl
+ in unfold_option unfolds
+
+let autounfold db cls gl =
+ let cls = concrete_clause_of cls gl in
+ let tac = autounfolds db in
+ tclMAP (function
+ | OnHyp (id,occs,where) -> tac occs (Some (id,where))
+ | OnConcl occs -> tac occs None)
+ cls gl
let autosimpl db cl =
let unfold_of_elts constr (b, elts) =
@@ -419,12 +427,13 @@ let autosimpl db cl =
unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
in unfold_option unfolds cl
+open Extraargs
+
TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) "in" hyp(id) ] ->
- [ autounfold (match db with None -> ["core"] | Some x -> x) (Some (id, InHyp)) ]
-| [ "autounfold" hintbases(db) ] ->
- [ autounfold (match db with None -> ["core"] | Some x -> x) None ]
- END
+| [ "autounfold" hintbases(db) in_arg_hyp(id) ] ->
+ [ autounfold (match db with None -> ["core"] | Some x -> x)
+ (glob_in_arg_hyp_to_clause id) ]
+END
let unfold_head env (ids, csts) c =
let rec aux c =
@@ -498,7 +507,7 @@ TACTIC EXTEND autounfoldify
let db = match kind_of_term x with
| Const c -> string_of_label (con_label c)
| _ -> assert false
- in autounfold ["core";db] None ]
+ in autounfold ["core";db] onConcl ]
END
TACTIC EXTEND unify
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index b708949e0..9c23be6f0 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -36,4 +36,4 @@ val eauto_with_bases :
bool * int ->
Term.constr list -> Auto.hint_db list -> Proof_type.tactic
-val autounfold : hint_db_name list -> Tacticals.goal_location -> tactic
+val autounfold : hint_db_name list -> Tacticals.clause -> tactic