coq/proofs, branch master The formal proof system More efficient variable membership check for Logic.move. 2021-04-20T08:54:34+00:00 Pierre-Marie Pédrot 2020-12-24T19:27:42+00:00 9caadc38de0e1c7b3362081da9482fc4455220a7 Instead of repeatedly crawling the same hypothesis again and again we only iter the term once. 
Instead of repeatedly crawling the same hypothesis again and again we
only iter the term once.
Do not construct intermediate lists in Logic.move. 2021-04-20T08:54:34+00:00 Pierre-Marie Pédrot 2020-12-24T19:06:33+00:00 4bdd1242d22e0870f2f0c97a83ece7e7eeeea7a1 






Specialize the code of Logic.move.
2021-04-20T08:54:34+00:00

Pierre-Marie Pédrot

2020-12-24T17:00:52+00:00

7ffd746e9156de69affaa3f284fce631ae0d6ef8












Preserve the context_val structure as much as possible in Logic.move.
2021-04-20T08:54:34+00:00

Pierre-Marie Pédrot

2020-12-24T16:21:13+00:00

89c1ac8061dd044b1625a4b5f2ca65226f3826ee

Instead of going back and forth between the representations, we take
advantage of the fact we always leave context suffixes untouched.





Instead of going back and forth between the representations, we take
advantage of the fact we always leave context suffixes untouched.







One catch-all's missing a noncritical; another is now useless (see 7efaf86).
2021-04-06T15:40:53+00:00

Hugo Herbelin

2020-11-04T06:30:40+00:00

9374aeeda2a3bc64774753862eae39a8e8539bb7












Factorize goal selector handling
2021-03-22T12:04:20+00:00

Gaëtan Gilbert

2021-03-22T11:42:02+00:00

cbe88ec043df8dff118e437f00c0299a464c8e8a

As a bonus ltac2 can produce bullet suggestions.





As a bonus ltac2 can produce bullet suggestions.







Add noncritical constraint to exception catching in solve_constraints
2021-03-04T19:48:36+00:00

Lasse Blaauwbroek

2021-03-04T19:47:24+00:00

75ebf1540b1e53a8ffae43beb5311695bdce8b41












[build] Split stdlib to it's own opam package.
2021-03-03T15:06:14+00:00

Emilio Jesus Gallego Arias

2020-06-22T15:52:18+00:00

ab98d847d237af3cd0e46edef42218be65cfc98f

We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.





We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.







Avoid using "subgoals" in the UI, it means the same as "goals"
2021-01-13T23:24:23+00:00

Jim Fehrle

2020-12-17T23:04:36+00:00

3da2dbe9728ae7f5b1860a8e3a6c458e6d976f84












Fix behaviour of destruct after change of case representation.
2021-01-04T13:01:46+00:00

Pierre-Marie Pédrot

2019-03-18T23:22:14+00:00

b6d5332c6e3127ba3fec466abe502ee40c031ed2

We ensure not to generate dummy beta-cuts in case branches generated
by destruct. There was seemingly code trying to perform this but in
an akward way.





We ensure not to generate dummy beta-cuts in case branches generated
by destruct. There was seemingly code trying to perform this but in
an akward way.