coq/plugins/pluginsdyn.itarget, branch master

Officially discontinue the experimental coq build via ocamlbuild

2016-06-08T12:32:56+00:00

 It has been accidentaly broken since early 2014 (and especially
 in 8.5), no easy repair, I won't devote any more hours to this stuff.
 Moreover no one seems to care apart from Emilio, but he's ok to work
 on this in a separate repository or branch.
 I left a dev/doc/ocamlbuild.txt file with a few words about this
 experiment.

Derive -> derive occurences

2015-01-12T18:07:55+00:00

Removing the XML plugin.

2014-09-08T16:46:25+00:00

Left a README, just in case someone will discover the remnants of it
decades from now.

Derive plugin.

2013-12-04T13:14:33+00:00

A small plugin to support program deriving (à la Richard Bird) in Coq.

It's fairly simple:

  Require Coq.Derive.Derive.

  Derive f From g Upto eq As h.

Produces a goal (actually two, but the first one is automatically shelved):

  |- eq g ?42

And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).

Remove the Dp plugin.

2012-04-17T14:50:28+00:00

Why2 has not been maintained for the last few years and the Why3 plugin should
be a suitable replacement in most cases.
    
Removed tactics: simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy.
Removed commands: Dp_hint, Dp_timeout, Dp_prelude, Dp_predefined, Dp_debug,
  Dp_trace.
    
Note that the "admit" tactic was actually provided by the Dp plugin. It has
been moved to extratactics.ml4.

Ported from v8.4 r15186.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15189 85f007b7-540e-0410-9357-904b9bb8a0f7

Added a Btauto plugin, that solves boolean tautologies.

2012-01-13T18:38:38+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7

Revert "syntax for exponents"

2011-02-25T14:19:39+00:00

This reverts pottier's commit r13849. It references a
ncring_plugin.cma for which there is no rule. I guess he forgot to
commit something...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7

syntax for exponents

2011-02-22T14:00:38+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7

plugin groebner updated and renamed as nsatz; first version of the doc of nsatz in the refman

2010-06-03T09:27:00+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7

Misc small fixes : warning, dep cycles, ocamlbuild...

2010-04-26T16:22:03+00:00

 - git ignore g_decl_mode.ml
 - exhaustive match for pp_vernac (BeginSubproof, ...)
 - for ocamlbuild, remove a spurious cycle in recordops.mli
   (unnecessary open of Classops), and fixes of *.itargets and _tags

 The compilation via ocamlbuild still need some work, since
 plugin firstorder now depends on the new plugin decl_mode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7