diff options
| author | Maxime Dénès | 2018-02-05 10:47:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-05 10:47:44 +0100 |
| commit | 55b2a4e0c24d691b71256c91ed54e245efce340b (patch) | |
| tree | 25c65622b9e9e83271d321f399981438b83ff053 /plugins | |
| parent | f5cf5e062bdc6264dc3c398ad76559ec188cde47 (diff) | |
| parent | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (diff) | |
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index c0479dd24b..d74ad06b34 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -553,7 +553,7 @@ GEXTEND Gram let s = coerce_reference_to_id qid in Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None), d) + ((Loc.tag (Name s)),None), d) ]]; END |