coq/vernac, branch master The formal proof system Merge PR #14075: New level of abstraction for streams with (non-canonical) location function 2021-04-23T21:38:26+00:00 Pierre-Marie Pédrot 2021-04-23T21:38:26+00:00 d9e9a63f9f49768eee8b239812365ad1115b964f Reviewed-by: ppedrot 
Reviewed-by: ppedrot
Merge PR #13965: [abbreviation] user syntax to set interp scope of argument 2021-04-23T14:33:27+00:00 Pierre-Marie Pédrot 2021-04-23T14:33:27+00:00 a0c3ebf4a6357a5140b98b4b40c71133c53d802e Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot 
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Relying on the abstract notion of streams with location for parsing. 2021-04-23T13:34:29+00:00 Hugo Herbelin 2021-04-05T14:40:10+00:00 e07efb3798c7c6ec54aac9093ab50fddfc6c6a5b We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml). 
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
Merge PR #14112: Cleanup useless environment manipulation in Class declaration 2021-04-18T14:13:11+00:00 coqbot-app[bot] 2021-04-18T14:13:11+00:00 469e594d276b55c3419b5c56d110adf675f571dc Reviewed-by: ejgallego 
Reviewed-by: ejgallego
Cleanup useless environment manipulation in Class declaration 2021-04-14T12:09:07+00:00 Gaëtan Gilbert 2021-04-14T12:09:07+00:00 ad380aca8cad3329c9a3db4b65b933b1179ed6a2 






Remove remote counter system
2021-04-14T10:54:38+00:00

Gaëtan Gilbert

2021-03-26T14:34:59+00:00

3efee577b4c92b38a987b40e555fae2c0a2023c4












Put async worker id in universe names
2021-04-14T10:54:05+00:00

Gaëtan Gilbert

2021-04-01T17:35:27+00:00

004bf5770bdcdd1b35dd27f683c733505823e741

This removes the need for the remote counter.





This removes the need for the remote counter.







[abbreviation] allow the user to set arguments scope
2021-04-07T17:59:46+00:00

Enrico Tassi

2021-03-19T13:29:07+00:00

d3963fc6b6dad5a0cf79815f31b2035ca8b3de25












cleanup: less exceptions, removal of try_interp_name_alias
2021-04-07T17:59:46+00:00

Enrico Tassi

2021-03-19T11:27:14+00:00

b47931125432df88171c7e8a879294508a603aa9












Missing dot in an error message.
2021-04-06T15:40:53+00:00

Hugo Herbelin

2020-10-31T21:15:33+00:00

bf6a5e1c7b10d6ff5686cc4a3e71eb105d7a0473