coq/test-suite/ltac2, branch master The formal proof system remove `with hintdb` variant of Ltac2 `unify`, because 2021-04-08T23:41:18+00:00 Samuel Gruetter 2021-04-08T23:41:18+00:00 807ea5f44ca74c2b2743ed0719e3cbdc46639da7 passing one single hintdb is not quite the right API, we should pass a transparent state instead, but that would require an API for manipulating hintdbs and transparent states, postponing 
passing one single hintdb is not quite the right API, we should
pass a transparent state instead, but that would require an API
for manipulating hintdbs and transparent states, postponing
unify for Ltac2 2021-04-08T01:02:10+00:00 Samuel Gruetter 2021-04-08T01:02:10+00:00 fb63ec7c10076d156caa43f73bad4f69653862a6 Fixes #14083 
Fixes #14083
Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2 2021-03-24T10:22:14+00:00 Pierre-Marie Pédrot 2021-03-24T10:22:14+00:00 ccb078536c89a9c36f32c416495de222faf5fd79 Reviewed-by: ppedrot 
Reviewed-by: ppedrot
Merge PR #13914: Allow the presence of type casts for return values in Ltac2. 2021-03-23T20:52:04+00:00 Michael Soegtrop 2021-03-23T20:52:04+00:00 fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48 
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
implement is_const, is_var, ... etc and has_evar for Ltac2 2021-03-19T20:31:35+00:00 Samuel Gruetter 2021-03-19T20:31:35+00:00 2420764db089d731635787bc11bd9ab312250fe7 Fixes #13963 
Fixes #13963
Slightly richer API allowing to shift the inductive in a block. 2021-03-16T19:02:56+00:00 Pierre-Marie Pédrot 2021-03-12T12:17:59+00:00 22be1892ee1b6030cfe9406bf72bb320dbe68be7 






Add tests for the new Ltac2 Ind API.
2021-03-16T19:02:56+00:00

Pierre-Marie Pédrot

2021-03-10T12:57:38+00:00

2915154835b8d0a90a5c3ca79c37d66142dc9a33












Adding a parsing test.
2021-03-10T11:16:19+00:00

Pierre-Marie Pédrot

2021-03-08T17:47:10+00:00

e17a1a832a077793a662d817c40e2a3b5bc1ed9c












Add tests for the printf feature.
2021-01-22T10:55:21+00:00

Pierre-Marie Pédrot

2021-01-21T13:26:19+00:00

56e2c0391dda94b80fab8c8993ea17ea5d807797












Add test for this new function.
2020-11-30T17:46:50+00:00

Pierre-Marie Pédrot

2020-11-21T18:43:44+00:00

bf111baffe75ebc1fc57aeb163e56a344d0632b8