coq/API, branch master The formal proof system [API] remove large file containing duplicate interfaces 2017-12-27T13:19:59+00:00 Enrico Tassi 2017-12-22T13:11:55+00:00 b37d3f199e4521e2ae20cc96f0f2b04acc36c7cc ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. 
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds. 2017-12-27T09:19:29+00:00 Maxime Dénès 2017-12-27T09:19:29+00:00 f6857ce53ecf64b0086854495b4a8451f476d5b4 






Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.typeclass
2017-12-27T08:48:38+00:00

Maxime Dénès

2017-12-27T08:48:38+00:00

9a8737360c72735e2099e4d81c9448f37311b498












[api] Also deprecate constructors of Decl_kinds.
2017-12-23T18:50:55+00:00

Emilio Jesus Gallego Arias

2017-12-15T18:09:15+00:00

21750c40ee3f7ef3103121db68aef4339dceba40

Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.

In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.





Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.

In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.







Separate vernac controls and regular commands.
2017-12-20T15:52:43+00:00

Maxime Dénès

2017-11-23T10:38:55+00:00

28d45c2413ad24c758fca5cfb00ec4ba20935f39

Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.

Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.

This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.





Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.

Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.

This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.







Merge PR #6419: [vernac] Split `command.ml` into separate files.
2017-12-18T08:38:18+00:00

Maxime Dénès

2017-12-18T08:38:18+00:00

3da76841125ef48889c8eceb134116e2d0bd7a2e












Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
2017-12-18T08:36:50+00:00

Maxime Dénès

2017-12-18T08:36:50+00:00

0168ee0b6463a9ef44d768b0020b34785986c1cb












[flags] Make program_mode a parameter for commands in vernac.
2017-12-17T09:56:07+00:00

Emilio Jesus Gallego Arias

2017-12-13T20:26:48+00:00

1172b52735a299dfc91aee36b30b576dfeff581c

This is useful as it allows to reflect program_mode behavior as an attribute.





This is useful as it allows to reflect program_mode behavior as an attribute.







[vernac] Split `command.ml` into separate files.
2017-12-17T09:56:04+00:00

Emilio Jesus Gallego Arias

2017-12-13T06:18:22+00:00

7a5688f6e2421a706c16e23e445d42f39a82e74b

Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.

We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.

This patch depends on #6413.





Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.

We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.

This patch depends on #6413.







[econstr] Switch constrintern API to non-imperative style.
2017-12-15T16:45:55+00:00

Emilio Jesus Gallego Arias

2017-12-13T00:38:39+00:00

53f5cc210da4debd5264d6d8651a76281b0b4256

We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.





We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.