coq/plugins/funind, branch master The formal proof system Merge PR #13965: [abbreviation] user syntax to set interp scope of argument 2021-04-23T14:33:27+00:00 Pierre-Marie Pédrot 2021-04-23T14:33:27+00:00 a0c3ebf4a6357a5140b98b4b40c71133c53d802e Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot 
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Merge PR #13911: Remove the :> type cast? 2021-04-21T14:58:51+00:00 coqbot-app[bot] 2021-04-21T14:58:51+00:00 f9996cdaf0b6aee12c5b71432b1edb90dffb569a Reviewed-by: mattam82 Ack-by: Zimmi48 
Reviewed-by: mattam82
Ack-by: Zimmi48
Check for existence before using `Global.lookup_constant` instead of catching `Not_found` 2021-04-19T10:46:13+00:00 Lasse Blaauwbroek 2021-04-19T09:08:03+00:00 e50a6195097c0d15c839c5403c1d02511afd54e4 `Global.lookup_constant` fails with an assertion instead of `Not_found`. Some code relied upon `Not_found`. 
`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
cleanup: less exceptions, removal of try_interp_name_alias 2021-04-07T17:59:46+00:00 Enrico Tassi 2021-03-19T11:27:14+00:00 b47931125432df88171c7e8a879294508a603aa9 






Remove the :> type cast
2021-03-30T16:51:56+00:00

Jim Fehrle

2021-03-07T18:15:11+00:00

eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf












[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.







Fix #13739 - disable some warnings when calling Function.
2021-02-03T16:15:01+00:00

Pierre Courtieu

2021-01-22T13:45:08+00:00

570744638ab4b08286562c0f4d45a7928ed008b0

Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.





Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.







Change the representation of kernel case.
2021-01-04T13:00:20+00:00

Pierre-Marie Pédrot

2019-03-03T20:03:37+00:00

d72e5c154faeea1d55387bc8c039d97f63ebd1c4

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.





We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.







Move evaluable_global_reference from Names to Tacred.
2020-12-21T12:55:32+00:00

Pierre-Marie Pédrot

2020-10-29T12:59:45+00:00

63332cbd4ac59b39fdce63d9872aa52dd8a2fec6

It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.

In any case this type does not belong to the kernel.





It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.

In any case this type does not belong to the kernel.







Fix a bug in funind.
2020-12-01T21:29:57+00:00

Pierre-Marie Pédrot

2019-03-11T11:16:45+00:00

64de97e5f16d3c52f73fb126ca64c85382c2a3d4

It was generating a completely nonsense case branch, but for some reason
the proof still went trough.





It was generating a completely nonsense case branch, but for some reason
the proof still went trough.