diff options
| author | herbelin | 2004-03-02 07:04:56 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-02 07:04:56 +0000 |
| commit | 8a1ddc270137f40cd8bbff20de4f41e284055891 (patch) | |
| tree | d3d41549bcd3cff2bbd0db1fb7824e05851941dd /parsing | |
| parent | 1a29faa00f1e2a6f2d71088a769fe2fbc823244a (diff) | |
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 4 |
4 files changed, 6 insertions, 10 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 73718c6292..ae9fc2aedb 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -255,9 +255,7 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids - | "as"; "("; ids = LIST1 simple_intropattern SEP ","; ")" -> [ids] - | -> [] ] ] + [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] ; simple_tactic: [ [ diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 721697c9a5..e307f96f9e 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -298,9 +298,7 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids - | "as"; "("; ids = LIST1 simple_intropattern SEP ","; ")" -> [ids] - | -> [] ] ] + [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] ; simple_tactic: [ [ diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9c27cb65b2..67033d008e 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -141,8 +141,8 @@ let pr_with_constr prc = function | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) let pr_with_names = function - | [] -> mt () - | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids) + | None -> mt () + | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) let pr_hyp_location pr_id = function | id, _, (InHyp,_) -> spc () ++ pr_id id diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 87eb0784f3..9813b37740 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -394,13 +394,13 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$,ref []) >> | 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_intro_pattern) (fst ids) in + let ids = mlexpr_of_option mlexpr_of_intro_pattern (fst ids) in <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref [])>> | Tacexpr.TacSimpleDestruct h -> <:expr< Tacexpr.TacSimpleDestruct $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_intro_pattern) (fst ids) in + let ids = mlexpr_of_option mlexpr_of_intro_pattern (fst ids) in <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >> (* Context management *) |