coq/plugins/groebner, branch master

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

Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way

2010-05-19T15:29:32+00:00

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

Factorisation between Makefile and ocamlbuild systems : .vo to compile are in //vo.itarget

2009-12-09T16:45:42+00:00

 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

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

Delete trailing whitespaces in all .{v,ml} files

2009-09-17T15:58:14+00:00

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

Use camlp4 to accept some specific non-exhaustive patterns in groebner

2009-07-20T13:03:25+00:00

 The camlp4 extension "refutpat" provides a syntax let* for pattern
 that are non-exhaustive on purpose (e.g. let* x::l = foo in ...).
 A Failure is raised if the pattern doesn't match the expression.

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

Move some examples for groebner into a test-suite file

2009-07-20T09:26:46+00:00

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

nouvelle version de la tactique groebner proposee par Loic:

2009-04-16T17:27:00+00:00

- algo de Janet (finalement pas utilise)
- le hash-cons des certificats de Benjamin et Laurent pas encore integre
- traitement des puissances jusqu'a 6 (methode totalement naive)



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

GroebnerZ: no more admitted lemmas

2009-03-27T13:39:46+00:00

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

Many changes in the Makefile infrastructure + a beginning of ocamlbuild

2009-03-20T20:50:44+00:00

 * generalize the use of .mllib to build all cma, not only in plugins/
 * the .mllib in plugins/ now mention Bruno's new _mod.ml files
 * lots of .cmo enumerations in Makefile.common are removed, since
   they are now in .mllib
 * the list of .cmo/.cmi can be retreive via a shell script line,
   see for instance rule install-library
 * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
   _files_
 * a -I option to coqdep_boot allows to control piority of includes
   (some files with the same names in kernel and checker ...)

 This is quite a lot of changes, you know who to blame / report to
 if something breaks.

 ... and last but not least I've started playing with ocamlbuild.
 The myocamlbuild.ml is far from complete now, but it already allows
 to build coqtop.{opt,byte} here. See comments at the top of
 myocamlbuild.ml, and don't hesitate to contribute, either for completing
 or simplifying it !

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

Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

2009-03-20T01:22:58+00:00

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