Permalink
Switch branches/tags
Commits on Jul 6, 2017
  1. Merge PR #853: Clean 'with Definition' implementation.

    maximedenes committed Jul 6, 2017
Commits on Jul 5, 2017
Commits on Jul 4, 2017
  1. Merge branch 'v8.6'

    ppedrot committed Jul 4, 2017
  2. Bump year in headers.

    ppedrot committed Jul 4, 2017
  3. Removing dead code in Subtyping.

    ppedrot committed Jul 4, 2017
    This code was a sketch of what to do when we properly implement module-level
    handling of instanciation of definitions by inductive types. It was completely
    dead code, called after an error, and somewhat incorrect. Instead of letting
    it bitrot, we remove it.
Commits on Jul 3, 2017
  1. Removing a few suspicious functions from the kernel.

    ppedrot committed Jul 3, 2017
    These functions were messing with the deferred universe constraints in an
    error-prone way, and were only used for printing as of today. We inline
    the one used by the printer instead.
  2. Do not add original constraints to the environment in 'with Definitio…

    ppedrot committed Jul 3, 2017
    …n' check.
    
    This was useless, because immediate constraints are assumed to already be in
    the current environment, while deferred constraints are useless for the
    conversion check of the definition types, as they only appear in the opaque
    body.
    
    This also clarifies a bit what is going on in the typing of module constraints
    w.r.t. global universes.
Commits on Jul 2, 2017
Commits on Jul 1, 2017
Commits on Jun 30, 2017
  1. Document an example `Makefile` for `coq_makefile`

    JasonGross committed Jun 16, 2017
    We document an example `Makefile` which does not include the generated
    `CoqMakefile`, but instead invokes arbitrary targets in it.
  2. Also quote $(COQLIB)/grammar

    JasonGross committed Jun 28, 2017
    In case COQLIB has backslashes, as it does on Windows, or spaces
Commits on Jun 29, 2017
  1. closing bug #5618 introduce by PR 828

    Julien Forest
    Julien Forest committed Jun 29, 2017
Commits on Jun 27, 2017
  1. Merge PR#731: Mini-cleaning around OCaml file names

    maximedenes committed Jun 27, 2017
    This is only a partial merge, we stick with using the standard OCaml
    (un)capitalize functions.
  2. A cleaning phase about ocaml file names.

    herbelin authored and maximedenes committed May 14, 2017
    Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_.
    
    We take this constraint into account in tools manipulating Ocaml file
    names.
Commits on Jun 26, 2017