Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Commits on Sep 15, 2012
  1. Port rewrites of tactic documentation from branch 8.4.

    gmelquio authored
    This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277,
    r15278, r15337. The merge did not go without troubles, but hopefully none
    of the changes were lost in process.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 12, 2012
  1. @pirbo

    Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRS

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Aug 23, 2012
  1. No more states/initial.coq, instead coqtop now requires Prelude.vo

    letouzey authored
     For starting a bare coqtop, the recommended option is now "-noinit"
     that skips the load of Prelude.vo. Option "-nois" is kept for
     compatibility, it is now an alias to "-noinit".
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. No more coqtop.opt, produce directly a coqtop binary

    letouzey authored
     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
  3. configure: get rid of the -src option and of ${COQSRC}

    letouzey authored
     The -src option was antic and probably broken (many references
     to source files without the $COQRSC prefix). Instead, it's quite
     simpler to refer to paths in relative way (and safer in win32
     where the base path may include spaces and other horrors).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. Port from 8.4 branch some build fixes concerning win32 :

    letouzey authored
     r15722:
       - CAMLBIN was cygwin-specific, leading to issues with coqmktop
       - A missing Filename.quote on the temp file used in coqmktop
       - Try to shorten the cmdline passed to Sys.command in coqmktop:
         way too many includes were passed to coqmktop -boot
    
     r15724: Coqmktop: the +compiler-libs for ocaml4 is back
     r15725: Coqmktop: better detection of ocaml 4 and above
     r15739: ocamlbuild : a missing include for camlp4
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15744 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Aug 22, 2012
  1. Do not forget to build the unicode libraries, necessary to compile an…

    msozeau authored
    …d launch coqtop in utf mode.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15743 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Aug 8, 2012
  1. @pirbo

    Fixup for macOS 10.8 & Ocaml 4.0

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15704 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jul 5, 2012
  1. Legacy Ring and Legacy Field migrated to contribs

    letouzey authored
     One slight point to check someday : fourier used to
     launch a tactic called Ring.polynom in some cases.
     It it crucial ? If so, how to replace with the setoid_ring
     equivalent ?
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 22, 2012
  1. @ppedrot

    Added an indirection with respect to Loc in Compat. As many [open Com…

    ppedrot authored
    …pat]
    
    were closed (i.e. the only remaining ones are those of printing/parsing).
    Meanwhile, a simplified interface is provided in loc.mli.
    
    This also permits to put Pp in Clib, because it does not depend on
    CAMLP4/5 anymore.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 20, 2012
  1. @pirbo

    Install compat5 module with grammar.cma

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15456 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 29, 2012
  1. place all pretty-printing files in new dir printing/

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. place all files specific to camlp4 syntax extensions in grammar/

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. Vernacexpr is now a mli-only file, locality stuff now in locality.ml

    letouzey authored
     Adds a directory ./intf for pure interfaces.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 23, 2012
  1. @pirbo

    Revert copy/pasted function in to minilib thanks to clib.cma

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 15, 2012
  1. Makefile: Really avoid locales in $(DATE)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 10, 2012
  1. @aspiwack

    Addedum to documentation of bullets: I now use the dedicated coq_example

    aspiwack authored
    environment to display the example.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 17, 2012
  1. Remove the Dp plugin.

    gmelquio authored
    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
Commits on Apr 12, 2012
  1. @pirbo

    lib directory is cut in 2 cma.

    pirbo authored
     - Clib that does not depend on camlpX and is made to be shared by all coq
       tools/scripts/...
     - Lib that is Coqtop specific
    
    As a side effect for the build system :
     - Coq_config is in Clib and does not appears in makefiles
     - only the BEST version of coqc and coqmktop is made
     - ocamlbuild build system fails latter but is still broken
    
    (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 14, 2012
  1. Final part of moving Program code inside the main code. Adapted add_d…

    msozeau authored
    …efinition/fixpoint and parsing of the "Program" prefix.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 2, 2012
  1. @pirbo

    Noise for nothing

    pirbo authored
    Util only depends on Ocaml stdlib and Utf8 tables.
    Generic pretty printing and loc functions are in Pp.
    Generic errors are in Errors.
    
    + Training white-spaces, useless open, prlist copies random erasure.
    Too many "open Errors" on the contrary.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 13, 2012
  1. @ppedrot

    Added a Btauto plugin, that solves boolean tautologies.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Dec 6, 2011
  1. fix Makefile.common handling of -byte-only

    gareuselesinge authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14770 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Nov 24, 2011
  1. @ppedrot

    Moving XML handling to lib directory

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14723 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Nov 6, 2011
  1. @ppedrot

    Added XML dependencies into Makefile

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

    Added XML manipulation tools to compilation chain

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14632 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 17, 2011
  1. Various fixes in the Makefiles

    letouzey authored
     After a successful build, re-doing make world should almost do nothing.
     For that:
      - Many targets added to .PHONY, especially "tools" since a "tools"
        directory exists. And anyway this is said to speed-up make a bit.
      - Concerning fake_ide, mentionning the .cm* instead of the .ml*
        avoid rebuilding these .cm*, and hence possibly many other things.
      - in Makefile.doc: fix the rule building index_url.txt
      - coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP)
        (which is the symlink). This avoids a situation where a first
        "make" could redo just a few files while a second "make" will
        rebuild many more. Typical scenario : touch the Makefile,
        1st make was re-doing tolink.ml and then coqmktop, but no more,
        a 2nd make was then detecting that coqtop and the stdlib was to
        be redone
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14476 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 6, 2011
  1. make world now builds fake_ide (to please coq-bench)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14462 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 13, 2011
  1. @aspiwack

    A new mechanism to handle errors.

    aspiwack authored
    Instead of the monolitic Cerrors, I introduce a lightweight Errors module
    whose error message can be expanded by module introducing exceptions.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 9, 2011
  1. remove useless dependancy for csdpcert

    fbesson authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14115 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 28, 2011
  1. Ide: restaure compilation of ide/macjokes.c removed by mistake

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13936 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 25, 2011
  1. Ide: more reorganisation and cleanup

    letouzey authored
     - Avoid using Util which depends on Compat and hence Camlp4
     - Instead, a small Minilib module specific to coqide, which
       duplicate 5 functions from Util (50 lines)
     - some dead code removal
     - the coqlib variable is asked to coqtop
     - remove obsolete Util.check_for_interrupt
    
     This way, coqide only depends on 3 files outside ide/ :
     Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted
     accordingly.
    
    TODO: how should we signal coqide error, warnings, etc ?
     For the moment, some Printf.eprintf, some failwith.
     To uniformize later...
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 23, 2011
  1. Ide: stronger separation from coqtop

    letouzey authored
     Former module Ide_blob is now divided in Ide_intf (linked both
     by coqtop and coqide) and Ide_slave (now only in coqtop).
     Ide_intf has almost no dependencies, we can now compile coqide
     with only coq_config.cm* and lib.cm(x)a
    
     TODO:
      - Devise a better way to display whether coqide is byte or opt
        in the about message (instead of Mltop.is_native, I display
        now the executable name, which hopefully contains opt or byte)
      - Check the late error handling in ide/coq.ml
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Feb 25, 2011
  1. Revert "syntax for exponents"

    glondu authored
    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
Commits on Feb 22, 2011
  1. syntax for exponents

    pottier authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7
Something went wrong with that request. Please try again.