coq/plugins/decl_mode, branch master

Farewell decl_mode

2017-03-07T10:18:29+00:00

This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.

Moving the Ltac plugin to a pack-based one.

2017-02-17T10:52:38+00:00

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.

Moving Ltac-specific parsing API to ltac/ folder.

2016-09-14T16:22:38+00:00

Merge PR #244.

2016-09-08T13:41:16+00:00

Merge branch 'v8.6'

2016-09-07T15:46:53+00:00

Merge branch 'v8.5' into v8.6

2016-09-07T15:43:39+00:00

Fixing what is probably a typo in Strict Proofs mode (#5062).

2016-09-03T09:46:15+00:00

CLEANUP: using |> operator more consistently

2016-08-30T08:47:37+00:00

CLEANUP: minor readability improvements

2016-08-24T19:12:29+00:00

mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.

If multiple modules define a function with a same name, e.g.:

	Context.{Rel,Named}.get_type

those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.

CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function

2016-08-24T15:35:20+00:00