diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-29 23:15:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-29 23:15:03 +0000 |
| commit | e7707310e3138c4fc455d26d5b06f372a5760bdd (patch) | |
| tree | d534f49850754e03e6b6d08a2e9d8f828adcd993 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 2 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 3 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 5 |
4 files changed, 5 insertions, 7 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 827409218..c578c66b3 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -185,7 +185,7 @@ GEXTEND Gram | IDENT "Fold"; cl = LIST1 constr -> Fold cl | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl | IDENT "Vm_compute" -> CbvVm - | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ] + | s = IDENT; OPT constr -> ExtraRedExpr s ] ] ; hypident: [ [ id = id_or_meta -> id,[],(InHyp,ref None) diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index dfb90f610..49dd4fa30 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -218,7 +218,7 @@ GEXTEND Gram | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl - | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ] + | s = IDENT -> ExtraRedExpr s ] ] ; hypident: [ [ id = id_or_meta -> id,(InHyp,ref None) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index c76de59f1..c3d865c0e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -370,8 +370,7 @@ let pr_red_expr (pr_constr,pr_ref) = function | Fold l -> hov 1 (str "Fold" ++ prlist (pr_arg pr_constr) l) | Pattern l -> hov 1 (str "Pattern " ++ prlist (pr_occurrences 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" diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a7c4a12af..37dcc22b1 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -257,9 +257,8 @@ let mlexpr_of_red_expr = function let f = mlexpr_of_list mlexpr_of_occ_constr in <:expr< Rawterm.Pattern $f l$ >> | Rawterm.CbvVm -> <:expr< Rawterm.CbvVm >> - | Rawterm.ExtraRedExpr (s,c) -> - let l = mlexpr_of_constr c in - <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ $l$ >> + | Rawterm.ExtraRedExpr s -> + <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ >> let rec mlexpr_of_argtype loc = function | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> |