diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
| commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
| tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/interface/debug_tac.ml4 | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/interface/debug_tac.ml4')
| -rw-r--r-- | contrib/interface/debug_tac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index 56abfb82..e1b8e712 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -239,9 +239,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 = rawwit_tactic Pcoq.Tactic.tactic_main_level -let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level -let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level +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 on_then = function [t1;t2;l] -> |