diff options
| author | herbelin | 2004-12-29 23:15:03 +0000 |
|---|---|---|
| committer | herbelin | 2004-12-29 23:15:03 +0000 |
| commit | e7707310e3138c4fc455d26d5b06f372a5760bdd (patch) | |
| tree | d534f49850754e03e6b6d08a2e9d8f828adcd993 /translate | |
| parent | bcd079c448c946270cbf3c5323ac8cf185450b5f (diff) | |
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 9057730eec..846b6468c3 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -780,8 +780,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l) | Red true -> error "Shouldn't be accessible from user" - | ExtraRedExpr (s,c) -> - hov 1 (str s ++ pr_arg pr_constr c) + | ExtraRedExpr s -> str s | CbvVm -> str "vm_compute" let rec pr_may_eval test prc prlc pr2 = function |