coq/ltac, branch master The formal proof system Revert "Add empty ltac_plugin file for forward compatibility." 2017-02-24T11:27:47+00:00 Maxime Dénès 2017-02-24T11:27:47+00:00 04d086e21cdf28c4029133a0f8fd1720d13544e8 This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only. 
This reverts commit e8137ae63b3b19436755f372b595e7343e942894,
was meant for 8.6 branch only.
Merge branch 'v8.6' 2017-02-22T12:44:16+00:00 Pierre-Marie Pédrot 2017-02-22T12:44:16+00:00 38c773f2053dd5ba27ae889bb4299ed90b9cc319 






Add empty ltac_plugin file for forward compatibility.
2017-02-21T07:09:56+00:00

Maxime Dénès

2017-02-21T07:09:56+00:00

e8137ae63b3b19436755f372b595e7343e942894

This is in preparation for landing of PR#309: Ltac as a plugin





This is in preparation for landing of PR#309: Ltac as a plugin







Ltac as a plugin.
2017-02-17T10:52:38+00:00

Pierre-Marie Pédrot

2016-10-06T14:59:27+00:00

653de32139ecee3114779a5ee2961c58793889e5

This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.





This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.







[misc] Remove unused binding.
2017-02-14T22:29:53+00:00

Emilio Jesus Gallego Arias

2016-10-10T15:09:24+00:00

0ca1717a3a1243d3fd905bb2f6c3d427f1f98dc6












Merge branch 'v8.6'
2017-02-01T09:54:53+00:00

Pierre-Marie Pédrot

2017-02-01T09:52:28+00:00

c17c3faee20251cd5c7168246e9ffcd12d557f85












Merge branch 'v8.5' into v8.6
2017-02-01T09:48:25+00:00

Pierre-Marie Pédrot

2017-02-01T09:36:24+00:00

568b38e1d599f8bac5adf140f5a114f2871bc436












Revert "Process Next Obligation proofs in parallel (fix #5314)"
2017-01-21T06:51:15+00:00

Enrico Tassi

2017-01-21T06:51:15+00:00

6ff62ec78d5517ec5905041fa2e4926e15ff89f0

This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.

It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.





This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.

It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.







Process Next Obligation proofs in parallel (fix #5314)
2017-01-20T13:14:24+00:00

Enrico Tassi

2017-01-20T12:51:37+00:00

1d4c34c79624fb81e64dfed8874b2fc9fa66c070












Merge branch 'v8.6'
2016-12-07T11:28:14+00:00

Pierre-Marie Pédrot

2016-12-07T11:28:14+00:00

ad768e435a736ca51ac79a575967b388b34918c7