diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-22 08:26:17 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-01 16:20:15 +0000 |
| commit | e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee (patch) | |
| tree | 4ed4ae97644642de2cda5eca4fd329889754e9b4 /plugins/ssr | |
| parent | c658141acff6d1b7f610960dd39998385c7e8806 (diff) | |
[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Diffstat (limited to 'plugins/ssr')
| -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 c0479dd24..d74ad06b3 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 |