diff options
Diffstat (limited to 'plugins/ltac/extraargs.ml4')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 53b726432..aa81f148e 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -228,11 +228,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Loc.ghost,id),InHyp) ] + [ HypLocation ((Loc.tag id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ] + [ HypLocation ((Loc.tag id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.ghost,id),InHypValueOnly) ] + [ HypLocation ((Loc.tag id),InHypValueOnly) ] END |