coq/test-suite/check, branch master

Clean-up dead file in test-suite.

2018-05-18T13:41:41+00:00

No more coqtop.opt, produce directly a coqtop binary

2012-08-23T12:52:47+00:00

 We now always produce two binaries, coqtop and coqtop.byte :
 - If ocamlopt is available, coqtop is directly what used to be coqtop.opt,
   no more symlinks needed.
 - Otherwise, coqtop is a copy of coqtop.byte.

 The same for coqchk and coqide...

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

Use the Makefile in test-suite/check

2010-04-10T19:07:03+00:00

The output format is preserved, but not the dynamics (results are
showed all at once at the end).  This script could be removed
altogether once the main Makefile (and daily bench) are fixed.

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

Fix typos in test-suite script

2010-04-10T19:06:53+00:00

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

Continuing r12485-12486 and r12549 (cleaning around name generation)

2009-12-02T21:41:06+00:00

- fixed misunderstanding of the role of nenv while simplifying code of
  occur_id in namegen.ml,
- documented the possible incompatibilites in CHANGES
- fixed output/Naming.v test, and fixed the count of misc. tests in
  test-suite/check.

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

Remove interface plugin

2009-12-02T08:36:14+00:00

It has moved to the contribs (Sophia-Antipolis/Interface).

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

Fixing xml theory file export (was not consistent with coqdoc file

2009-11-26T16:28:17+00:00

naming heuristic). Added a corresponding test.
Note: maybe should the generated .v file for exporting the theory be made
of a valid ident if ever coqdoc eventually follows coq convention:
currently it has name foo.theory.v which is not coqc-compilable.

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

Improved the treatment of Local/Global options (noneffective Local on

2009-10-25T07:36:43+00:00

Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).

Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).



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

Nettoyage des variables Coq et amélioration de coqmktop. Les

2008-12-19T15:30:49+00:00

principaux changements sont:
  - coqtop (et coqc) maintenant insensible aux variables
    d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
    librairies Coq peut être spécifié par l'option -coqlib
  - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
    -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
    chemins des exécutables OCaml; en dehors du mode boot, coqmktop
    cherche les exécutables OCaml dans PATH
  - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
    étant installé en copiant l'architecture des sources (ie lib.cmxa
    est installé dans COQLIB/lib/lib.cmxa)
  - coq_makefile prend maintenant 3 paramètres sous forme de variables
    d'environnement: COQBIN pour dire où trouver les exécutables Coq,
    CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
    chemins vers les librairies sont déduits en utilisant -where

Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...). 




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

Add new directory for pre-compilation of files needed for further tests.

2008-12-02T22:37:24+00:00

Application to the test of notation import from within a section.


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