- Add pretty-printers for Idpred, Cpred and transparent_state, used for

  debugging and printing hint databases
- Typeclasses unfold now correctly adds _global_ unfold hints.
- New tactic autosimpl to do simplification using the declared unfold
  hints in given hint databases.
- Work on auto-modulo-some-delta (the declared Unfold constants),
  actually used mostly if the goal contains evars, as Hint_db.map_auto
  does not work up-to any conversions (yet).
- Fix GenMul which was using the old semantics of failing early because
  of variance checks, which is not possible in the new implementation.
- Restrict when reflexive_morphism may be used using an extern tactic.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 0 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0facf2393..03b29d523 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -384,3 +384,20 @@ TACTIC EXTEND dfs_eauto
       hintbases(db) ] ->
     [ gen_eauto false (true, make_depth p) lems db ]
 END
+
+let autosimpl db cl =
+  let unfold_of_elts constr (b, elts) =
+    if not b then 
+      List.map (fun c -> [], constr c) elts
+    else []
+  in
+  let unfolds = List.concat (List.map (fun dbname -> 
+    let ((ids, csts), _) = searchtable_map dbname in
+      unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
+      unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
+  in unfold_option unfolds cl
+
+TACTIC EXTEND autosimpl
+| [ "autosimpl" hintbases(db) ] ->
+    [ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
+END