coq/contrib/romega, branch master

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

Makefile: ml dependencies of contribs are moved to .mllib files

2009-03-14T11:29:46+00:00

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

Take advantage of natdynlink when available: almost all contribs become loadable plugins

2008-12-16T13:56:19+00:00

- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
  when launching coqtop (see Coqtop.load_initial_plugins):
     extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
     quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
  one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
  is explicitely given to configure, coqtop is statically linked with all of
  the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
  and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
  same location as the .v during the build, but can be moved later in any place of
  the ml loadpath.

This is clearly an experimentation. Feedback most welcome...

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

ROmega : make it work even if no Require Import ZArith has been done

2008-07-16T14:34:15+00:00

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

Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]

2008-05-09T14:40:04+00:00

pour les listes (trop contraignant)


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

Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la

2008-04-29T19:07:00+00:00

syntaxe interne de ring_lookup et field_lookup qui n'était pas assez
robuste pour supporter une syntaxe [ ... ] dans constr.  
Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]"
au niveau 0.



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

Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicit

2008-04-09T21:15:42+00:00

loading and exporting of Setoid to ROmega which uses it for iff.


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

small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is

2007-11-06T22:46:21+00:00

more general.



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

Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;

2007-08-16T11:16:43+00:00

modification de interp_ltac_reference pour passer les ids utilisées
dans le contexte d'appel d'une tactique.



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

A generic preprocessing tactic zify for (r)omega

2007-07-18T22:38:06+00:00

------------------------------------------------

See file PreOmega for more details and/or test-suite/succes/*Omega*.v

The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.

Integration with omega and romega:
(r)omega : the earlier tactics, 100% compatible
(r)omega with * : full zify applied before the (r)omega run
(r)omega with , where is a sub-list of {nat,N,positive,Z},
applies only specific parts of zify (btw "with Z" means take advantage
of Zmax, Zmin, Zabs and Zsgn).

As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it.

For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.

Even though zify is designed to help (r)omega, I think it might be
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet.

Side-effects:

- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated,
and this operation will be justified by means of decidability, it helps
to have as little as possible in the conclusion.

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