coq/plugins/extraction, branch master The formal proof system 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`.
Fixing #13581: missing support for let-ins in arity of inductive types. 2021-04-04T09:01:25+00:00 Hugo Herbelin 2020-12-06T02:03:12+00:00 a265c1ad912b4940861ec27efd09e5b20d33233c At first view, the fix takes care about when to use the number of assumptions and when to also include local definitions, but I don't know all the details of the implementation to be absolutely sure. 
At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.
[recordops] complete API rewrite; the module is now called [structures] 2021-03-26T14:19:19+00:00 Enrico Tassi 2021-03-18T18:15:39+00:00 34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a 






Do not match on record types with mutable fields in function arguments.
2021-03-23T09:26:34+00:00

Guillaume Melquiond

2021-03-23T09:20:10+00:00

01b061f0082a70f66016e78075a5952af8ed5431

This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.

Example:

    let foo {bar} x = ...

is compiled as

    let foo y = match y with {bar} -> fun x -> ...





This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.

Example:

    let foo {bar} x = ...

is compiled as

    let foo y = match y with {bar} -> fun x -> ...







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







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.







Fix comparison of extracted array literals
2020-11-23T15:08:37+00:00

Gaëtan Gilbert

2020-11-23T15:08:37+00:00

60ed425ffc8bc30c11a3a8e542a9bfb0a0a06471

Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
  let o = optims () in
  let rec norm a =
    let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
    if eq_ml_ast a a' then a else norm a'
  in norm a
~~~
the `eq_ml_ast` was always returning `false`.





Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
  let o = optims () in
  let rec norm a =
    let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
    if eq_ml_ast a a' then a else norm a'
  in norm a
~~~
the `eq_ml_ast` was always returning `false`.







Introduce an Ind module in the Names API.
2020-10-21T10:22:12+00:00

Pierre-Marie Pédrot

2020-09-23T10:42:21+00:00

bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc

This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.





This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.







Deprecate the non-qualified equality functions on kerpairs.
2020-10-21T10:19:02+00:00

Pierre-Marie Pédrot

2020-09-22T08:44:51+00:00

2b91a8989687e152f7120aa6c907ffeba8495bab

This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.





This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.







Dropping the misleading int argument of Pp.h.
2020-10-08T21:47:14+00:00

Hugo Herbelin

2020-10-05T20:21:04+00:00

db278921c54201a01543953cc0986fc0fb126615

An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.

We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.





An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.

We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.