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

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

identity. Add notations for compatibility and support for
understanding these notations in the ml files.



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

- 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

- Added "simple apply in" (cf wish 1917) + conversion and descent
  under conjunction + contraction of useless beta-redex in "apply in"
  + support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
  is type-checked using a kernel conversion in the opposite side of what
  the proof indicated (hence leading to a potential unexpected penalty
  at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
  temporary evars as intermediate steps but this was too long to implement.

Smoother API in tactics.mli for assert_by/assert_as/pose_proof.



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

- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
  quotations de tactiques pour simuler les métas des constr - quitte à devoir
  utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
  des Meta [pretyping]



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

- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour
  éviter la confusion avec le Rlt_not_le de RIneq.
- Quelques variantes de lemmes en plus dans RIneq.
- Déplacement des énoncés de sigT dans sig (y compris la complétude)
  et utilisation de la notation { l:R | }.
- Suppression hypothèse inutile de ln_exists1.
- Ajout notation ² pour Rsqr.

Au passage:
- Déplacement de dec_inh_nat_subset_has_unique_least_element
  de ChoiceFacts vers Wf_nat.
- Correction de l'espace en trop dans les notations de Specif.v liées à "&".
- MAJ fichier CHANGES

Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne
sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1"
non prouvé).



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

... After sending a "yakafokon" email, let's start a code-cleanup session...




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

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

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