Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Commits on Nov 26, 2015
  1. @herbelin

    v8.3: Quick fix so that we can give option -lablgtkdir and the

    herbelin committed
    escaping of quotes is always done for (not very moral
    though, that a string containing a "-I dir" string is hard-wired in which is supposed to be at a different level of
    abstraction than the level of ocaml executable syntax).
  2. @herbelin

    v8.3: supporting compilation of coqide with lablgtk 2.16 and 2.18.

    herbelin committed
    Collapsing new Gtk modifiers to MOD5 for compatibility with lablgtk 2.14.
    Not sure that this is the optimal thing to do, but, at least, this
    does not seem to be changing the use of CoqIDE wrt to it was when
    using lablgtk 2.14.
Commits on Nov 23, 2015
  1. @herbelin
Commits on Sep 9, 2015
  1. @maximedenes

    Fix a bug in 31 bit arithmetic, leading to failing conversion tests.

    maximedenes committed
    On 64 bits architectures, integers could have some of their 32 msb set to 1
    internally in the VM. When read back to a Coq term, this was not observable. But
    an equality test would fail. From the user point of view, the symptom was that
    vm_compute; reflexivity would succeed but the subsequent Qed would fail.
    Bug reported by Tahina Ramananandro.
  2. @catalin-hritcu @maximedenes

    Fixed critical bug in 31 bit arithmetic of VM

    catalin-hritcu committed with maximedenes
    ADDMULDIVINT31 was missing pops in some cases
Commits on Apr 9, 2015
  1. @letouzey

    update the changelog of v8.3

    letouzey committed
Commits on Apr 1, 2015
  1. @herbelin

    Reverting mistakenly committed attempt to support reduction of evar

    herbelin committed
    instances in cbv. Detected by Benjamin as it makes compilation of
    files such as BigN to explode.
  2. @bgregoir
Commits on Mar 16, 2015
  1. @clarus @aspiwack

    Gitattributes file added to generate archive.

    clarus committed with aspiwack
    Backport from v8.4 ( c1aabb1 ).
Commits on Mar 13, 2015
  1. @aspiwack

    Fix compilation with forthcoming Ocaml version 4.03.

    aspiwack committed
    Patch by Pierre Chambart, with the following comment:
     * OCaml runtime header files used to declare the int32, uint32, int64
    and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h.
    * OCaml now forbid declaring two exceptions with the same name in a compilation unit.
    (Trivial) backport from the v8.4 patch.
  2. @herbelin
  3. @herbelin
Commits on Jan 29, 2015
  1. @herbelin

    v8.3: backporting Pierre Boutillier's fix to #3843 part 2: "The .cmxs

    herbelin committed
    files for plugins must have x permission".
  2. @herbelin
Commits on Oct 22, 2014
  1. @maximedenes
Commits on Jun 21, 2014
  1. @herbelin
Commits on Jun 17, 2014
  1. @herbelin
Commits on Jun 13, 2014
  1. @herbelin
Commits on Apr 11, 2014
  1. @maximedenes

    Fix guard condition for nested cofixpoints in checker.

    maximedenes committed
  2. @maximedenes

    Fix guard condition for nested cofixpoints.

    maximedenes committed
    There were actually two problems, one of them being clearly unsound.
    To make sure that this does not show up somewhere else in the code, it would
    be better to resort to an abstraction keeping in sync the environment and the
    De Bruijn index of the current cofixpoints, like guard_env does for fixpoints.
Commits on Apr 5, 2014
  1. @herbelin
  2. @herbelin

    v8.3: Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not

    herbelin committed
    supporting metas/evars). Fix of #3169 is by calling pretyping retyper
    rather than the non evar-aware kernel type-checker (since argument of
    vm_compute is supposed to be already typable).
Commits on Mar 5, 2014
  1. @gares

    Fix (3243): univ constraints of module subtyping were not propagated

    gares committed
    Universe constraints coming from subtyping were not propagated
    to the outermost module and hence not stocked in the .vo file.
    Still, they were added to the interactive safe environment and
    hence checked for satisfiability.
Commits on Feb 26, 2014
  1. @maximedenes

    Fix for critical bug in arity check.

    maximedenes committed
    Fix partially blind because Coq 8.3 does not compile fully on my machine.
  2. @pirbo @maximedenes

    configure stript allows make v4.00

    pirbo committed with maximedenes
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Nov 25, 2013
  1. @herbelin
Commits on Nov 21, 2013
  1. @letouzey

    configure: CAML_LD_LIBRARY_PATH is enriched, not overwritten

    letouzey committed
     Keeping the earlier content of this variable is crucial for opam
     (at least).
     Thanks to François Bobot and Thomas Refis for this one...
Commits on Jun 12, 2013
  1. Lablgtk2 was not properly included at linking time by coqmktop becaus…

    mdenes committed
    …e of wrong
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 2, 2013
  1. v8.3: Fixing a typo in the documentation of discriminate.

    herbelin committed
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 18, 2013
  1. Coqc: accept -exclude-dir option (fix #3025)

    letouzey committed
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 25, 2013
  1. Typo in refman (fix #2962)

    letouzey committed
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Avoid using for Globrevtab (fix #2734)

    letouzey committed
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. Add the test-case of bug 2750 in the test-suite

    letouzey committed
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. Avoid Pervasives.(=) on some global_reference (fix #2750)

    letouzey committed
    This is actually a partial backport of trunk commit 15999
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 21, 2013
  1. Firstorder: record with defined field aren't conjonctions (fix #2629)

    letouzey committed
     The let-in in the type of constructor was perturbating the
     Hipattern.dependent check, leading firstorder to consider too much
     inductives as dependent-free conjonctions, ending with lift errors
     (UNBOUND_REL_-2, ouch).
     This patch is probably overly cautious : if the variable of the
     let-in is used, we consider the constructor to be dependent.
     If someday somebody feels it necessary, he/she could try to reduce
     the let-in's instead...
    git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
Something went wrong with that request. Please try again.