diff options
| author | Gaëtan Gilbert | 2020-02-21 13:24:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-21 13:24:53 +0100 |
| commit | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (patch) | |
| tree | f4c205e5d98700c0b118efe09498e22aff44adfb /parsing/notation_gram.ml | |
| parent | 4b6e6c6c187441f928921cbdd14093e296682f40 (diff) | |
| parent | 7489014fa6053c28e09852b0bf0602f2160cdda5 (diff) | |
Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'parsing/notation_gram.ml')
0 files changed, 0 insertions, 0 deletions