diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-04 16:52:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-04 16:52:48 +0000 |
| commit | 26295c8765560d57c16d7e530f81743d0a69b20a (patch) | |
| tree | 197e430ef7409debd6b7f654c106d8438057818f /translate | |
| parent | a99c0dfe6cc3baabc6f4a61103322e1740b020d9 (diff) | |
Ajout constructeur External pour appel outil externe à Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6678 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/pptacticnew.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 0dbf05aac..33784c1b1 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -818,6 +818,9 @@ and pr_tacarg env = function | ConstrMayEval c -> pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c | TacFreshId sopt -> str "fresh" ++ pr_opt qsnew sopt + | TacExternal (_,com,req,la) -> + str "external" ++ spc() ++ qsnew com ++ spc() ++ qsnew req ++ spc() ++ + prlist_with_sep spc (pr_tacarg env) la | (TacCall _|Tacexp _|Integer _) as a -> str "ltac:" ++ pr_tac env (latom,E) (TacArg a) |