diff options
| author | herbelin | 2009-04-27 13:43:41 +0000 |
|---|---|---|
| committer | herbelin | 2009-04-27 13:43:41 +0000 |
| commit | f90fde30288f67b167b68bfd32363eaa20644c5f (patch) | |
| tree | 00faf9b0c6aa8749d3ec67b8fdc4f14044535b1c /plugins/interface/debug_tac.ml4 | |
| parent | 3f40ddb52ed52ea1e1939feaecf952269335500f (diff) | |
- Cleaning (unification of ML names, removal of obsolete code,
reorganization of code) and documentation (in pcoq.mli) of the code
for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
Notation, Notation); merged the two copies of interp_entry_name to
avoid they diverge.
- Added support in Tactic Notation for ne_..._list_sep in general and
for (ne_)ident_list(_sep) in particular.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/debug_tac.ml4')
| -rw-r--r-- | plugins/interface/debug_tac.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/interface/debug_tac.ml4 b/plugins/interface/debug_tac.ml4 index aad3a765de..79c5fe8a8e 100644 --- a/plugins/interface/debug_tac.ml4 +++ b/plugins/interface/debug_tac.ml4 @@ -9,6 +9,7 @@ open Util;; open Proof_type;; open Tacexpr;; open Genarg;; +open Extrawit;; let pr_glob_tactic = Pptactic.pr_glob_tactic (Global.env()) @@ -239,9 +240,9 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti by the list of integers given as extra arguments. *) -let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level -let globwit_main_tactic = Pcoq.globwit_tactic Pcoq.tactic_main_level -let wit_main_tactic = Pcoq.wit_tactic Pcoq.tactic_main_level +let rawwit_main_tactic = rawwit_tactic tactic_main_level +let globwit_main_tactic = globwit_tactic tactic_main_level +let wit_main_tactic = wit_tactic tactic_main_level let on_then = function [t1;t2;l] -> |