Commits on Mar 2, 2016
  1. @herbelin

    Ensuring that sed does not use a specific locale for characters >= 128,

    so that it does not fail on files containing latin1 characters,
    e.g. g_omega.ml4.
    herbelin committed Mar 2, 2016
Commits on Jan 13, 2016
  1. @herbelin

    v8.2: Fix for #4467 (missing shadowing of variables in cases pattern).

    Backported from v8.4.
    herbelin committed Jan 13, 2016
Commits on Dec 2, 2015
  1. @herbelin
  2. @herbelin

    Updating INSTALL about 3.08.3.

    Coq loops on Ring_polynom.v with (at least) this version.
    herbelin committed Dec 2, 2015
Commits on Nov 29, 2015
  1. @herbelin
  2. @herbelin

    Updating CHANGES.

    herbelin committed Nov 28, 2015
  3. @herbelin

    Test for critical bug #4157.

    herbelin committed Nov 28, 2015
Commits on Nov 26, 2015
  1. @herbelin
  2. @aspiwack @herbelin

    v8.2: Backporting Arnaud's fix for compilation with Ocaml version 4.03.

    Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsole
    
    * 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 on
    aspiwack committed with herbelin Mar 13, 2015
  3. @herbelin

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

    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.
    herbelin committed Nov 26, 2015
  4. @herbelin
Commits on Sep 9, 2015
  1. @maximedenes

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

    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.
    maximedenes committed Sep 6, 2015
  2. @catalin-hritcu @maximedenes

    Fixed critical bug in 31 bit arithmetic of VM

    ADDMULDIVINT31 was missing pops in some cases
    catalin-hritcu committed with maximedenes Sep 5, 2015
Commits on Apr 1, 2015
  1. @bgregoir
Commits on Jan 29, 2015
  1. @herbelin

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

    files for plugins must have x permission".
    herbelin committed Jan 29, 2015
  2. @herbelin
Commits on Apr 11, 2014
  1. @maximedenes

    Fix guard condition for nested cofixpoints in checker.

    Conflicts:
    	checker/inductive.ml
    maximedenes committed Apr 10, 2014
  2. @maximedenes

    Fix guard condition for nested cofixpoints.

    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.
    
    Conflicts:
    	kernel/inductive.ml
    maximedenes committed Apr 10, 2014
Commits on Mar 5, 2014
  1. @gares

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

    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.
    gares committed Mar 5, 2014
Commits on Feb 26, 2014
  1. @maximedenes

    Fix for critical bug in arity check.

    Fix partially blind because Coq 8.2 does not compile with latest lablgtk.
    maximedenes committed Feb 25, 2014
  2. @pirbo @maximedenes

    configure stript allows make v4.00

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17042 85f007b7-540e-0410-9357-904b9bb8a0f7
    pirbo committed with maximedenes Nov 3, 2013
Commits on Nov 29, 2013
  1. @herbelin

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

    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).
    herbelin committed Nov 29, 2013
Commits on Nov 25, 2013
  1. @herbelin
Commits on Jun 2, 2013
  1. v8.2: Fixing a typo in the documentation of discriminate.

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16554 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Jun 2, 2013
Commits on Feb 5, 2013
  1. Fixed #2839 and #2981 (anomaly NotASort in retyping). Was due to

    collision between two variables of same name, but finally made a
    slightly different implementation of sort_of_atomic_type.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16188 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Feb 5, 2013
Commits on Jan 28, 2013
  1. v8.2: Fixed bug #2966 (de Bruijn error in computation of heads for co…

    …ercions).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16171 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Jan 28, 2013
Commits on Jan 27, 2013
  1. v8.2: Fixed bug #2967 (missing check on ill-formed recursive notation…

    … strings).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16158 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Jan 27, 2013
Commits on Oct 17, 2012
  1. v8.2: Removed mention of configure's option -nowarning in INSTALL file.

    This option had actually never been released (it only existed for 2
    days long in August 1999).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15904 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Oct 17, 2012
Commits on Sep 5, 2012
  1. v8.2: A few fixes in configure file:

    - Fixing parsing of option -custom
    - More precise documentation of which option expects an argument
    - Deprecation of obviously obsolete -emacs option
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15776 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Sep 5, 2012
Commits on Aug 3, 2012
  1. Bigint: adds a missing -1 in hugo's last commit 15659

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15670 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Aug 3, 2012
Commits on Jul 29, 2012
  1. v8.2: Better fixing propagation of carry in sub_mult used for euclidian

    division over unbounded integers (thanks again to L. Théry for
    pointing out the remaining problem in r15640).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15662 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Jul 29, 2012
Commits on Jul 25, 2012
  1. Compatibility with camlp5 6.05 (Closes: #2728)

    Adapted from commit r15025.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15652 85f007b7-540e-0410-9357-904b9bb8a0f7
    glondu committed Jul 25, 2012
  2. Fix compilation with camlp5 in strict mode (Closes: #2487)

    Patch from Daniel de Rauglaudre.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15651 85f007b7-540e-0410-9357-904b9bb8a0f7
    glondu committed Jul 25, 2012
Commits on Jul 21, 2012
  1. v8.2: Fixing unchecked overflow in sub_mult used for euclidian divisi…

    …on over
    
    unbounded integers (thanks to L. Théry for pointing out the problem).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15640 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Jul 21, 2012
Commits on Apr 19, 2012
  1. v8.2: Supporting optional byte-mark order in utf-8 files (bug #2757).

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15222 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Apr 19, 2012