coq/interp, branch master The formal proof system 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
Merge PR #13911: Remove the :> type cast? 2021-04-21T14:58:51+00:00 coqbot-app[bot] 2021-04-21T14:58:51+00:00 f9996cdaf0b6aee12c5b71432b1edb90dffb569a Reviewed-by: mattam82 Ack-by: Zimmi48 
Reviewed-by: mattam82
Ack-by: Zimmi48
[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: remove confusing sharing
2021-04-07T17:59:46+00:00

Enrico Tassi

2021-03-19T11:47:43+00:00

eec8ba3a0e807e8de038eb0feaf5db003f423e62












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












Remove the :> type cast
2021-03-30T16:51:56+00:00

Jim Fehrle

2021-03-07T18:15:11+00:00

eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf












[recordops] complete API rewrite; the module is now called [structures]
2021-03-26T14:19:19+00:00

Enrico Tassi

2021-03-18T18:15:39+00:00

34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a












Remove useless libobject for Implicit Type
2021-03-19T13:43:44+00:00

Gaëtan Gilbert

2020-10-19T13:27:44+00:00

f2b780ab087f8d107820f2fa6f789b83df23d056

cache_function is called from add_leaf and after discharging sections,
but default_object is section local.





cache_function is called from add_leaf and after discharging sections,
but default_object is section local.







Merge PR #13840: [notation] option to fine tune printing of literals
2021-03-10T13:53:55+00:00

coqbot-app[bot]

2021-03-10T13:53:55+00:00

317db327c21ac78bd921020118b19afaf1c02350

Reviewed-by: SkySkimmer
Ack-by: jfehrle





Reviewed-by: SkySkimmer
Ack-by: jfehrle







Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)
2021-03-05T18:04:27+00:00

Pierre-Marie Pédrot

2021-03-05T18:04:27+00:00

aacf8f1756fa5a289f27485a1951392505edfc53

Reviewed-by: Zimmi48
Reviewed-by: ppedrot





Reviewed-by: Zimmi48
Reviewed-by: ppedrot