diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 07:04:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 07:04:56 +0000 |
| commit | 8a1ddc270137f40cd8bbff20de4f41e284055891 (patch) | |
| tree | d3d41549bcd3cff2bbd0db1fb7824e05851941dd /parsing/pptactic.ml | |
| 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/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9c27cb65b..67033d008 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 |