diff options
| author | herbelin | 2008-07-18 10:06:36 +0000 |
|---|---|---|
| committer | herbelin | 2008-07-18 10:06:36 +0000 |
| commit | ccff0b020b3a0950a6358846b6a40b8cd7a96562 (patch) | |
| tree | 79512d1401e69130c4f0bc15cd4fe26ba6f3300b /parsing | |
| parent | c24154216b7ef81e85ca2dead4429c3595aa9e93 (diff) | |
Modification rapide du message d'erreur lorsqu'un _ ne peut être
effacé dans un intro-pattern (suggéré par ssreflect).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 10 |
2 files changed, 6 insertions, 6 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a1fd1649e3..092dc9f884 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -251,7 +251,7 @@ GEXTEND Gram | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l] | t::q -> IntroOrAndPattern [[t;pairify q]] in pairify (si::tc) - | "_" -> IntroWildcard + | "_" -> IntroWildcard loc | prefix = pattern_ident -> IntroFresh prefix | "?" -> IntroAnonymous | id = ident -> IntroIdentifier id diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6bd795ed5f..66a74ad162 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -62,12 +62,16 @@ let mlexpr_of_reference = function | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> +let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> + +let mlexpr_of_loc loc = <:expr< $dloc$ >> + let mlexpr_of_by_notation f = function | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> let mlexpr_of_intro_pattern = function - | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> + | Genarg.IntroWildcard loc -> <:expr< Genarg.IntroWildcard $mlexpr_of_loc loc$ >> | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >> | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >> | Genarg.IntroIdentifier id -> @@ -85,10 +89,6 @@ let mlexpr_of_quantified_hypothesis = function | Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >> | Rawterm.NamedHyp id -> <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >> -let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> - -let mlexpr_of_loc loc = <:expr< $dloc$ >> - let mlexpr_of_or_var f = function | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >> | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> |