From f90fde30288f67b167b68bfd32363eaa20644c5f Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 27 Apr 2009 13:43:41 +0000 Subject: - 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 --- plugins/interface/debug_tac.ml4 | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'plugins/interface/debug_tac.ml4') 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] -> -- cgit v1.2.3