diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 16 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 4 |
4 files changed, 10 insertions, 14 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 225aa4728..3b7081012 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -236,7 +236,7 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids + [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids | -> [] ] ] ; simple_tactic: diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 40a292ca1..c45dc332f 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -234,7 +234,7 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids + [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids | -> [] ] ] ; simple_tactic: diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9c23d0ba5..0382a2fdb 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -130,24 +130,20 @@ let pr_bindings prc prlc = function let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) -let pr_with_names = function - | [] -> mt () - | ids -> spc () ++ str "as [" ++ - hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ") - (prlist_with_sep spc pr_id) ids ++ str "]") - let rec pr_intro_pattern = function | IntroOrAndPattern pll -> str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) ++ str "]" -(* - | IntroAndPattern pl -> - str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" -*) | IntroWildcard -> str "_" | IntroIdentifier id -> pr_id id +let pr_with_names = function + | [] -> mt () + | ids -> spc () ++ str "as [" ++ + hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ") + (prlist_with_sep spc pr_intro_pattern) ids ++ str "]") + let pr_hyp_location pr_id = function | InHyp id -> spc () ++ pr_id id | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")" diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index cf59d9a97..f5ebd8fcf 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -376,13 +376,13 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacNewInduction (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in + let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> | Tacexpr.TacOldDestruct h -> <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacNewDestruct (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in + let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >> (* Context management *) |