coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[vernac] use plain strings as attribute names	Vincent Laporte	2018-07-03
\| \| \| \|	The concrete syntax is still restricted to identifiers.
*	[vernac] Generic syntax for flags/attributes	Vincent Laporte	2018-07-03
\|
*	[vernac] Add a “deprecated” attribute	Vincent Laporte	2018-07-03
\|
*	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
\| \| \| \| \| \| \| \| \| \| \|	This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
*	Remove reference name type.	Maxime Dénès	2018-06-18
\| \| \| \| \| \| \| \|	reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
\| \| \| \|	We move the last 3 types to more adequate places.
*	Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Pierre-Marie Pédrot	2018-06-04
\|\
* \	Merge PR #7657: Fix a couple typos in deprecation messages	Pierre-Marie Pédrot	2018-06-04
\|\ \
\| * \|	Fix a couple typos in deprecation messages	Armaël Guéneau	2018-05-31
\| \| \|
\| \| *	Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Armaël Guéneau	2018-05-31
\| \|/
* /	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
\|/ \| \| \| \| \| \| \|	Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
*	Merge PR #6969: [api] Remove functions deprecated in 8.8	Maxime Dénès	2018-05-31
\|\
* \|	Move interning the [hint_pattern] outside the Typeclasses hooks.	Gaëtan Gilbert	2018-05-30
\| \| \| \| \| \| \| \| \| \| \| \|	Close #7562. [api] move hint_info ast to tactics.
\| *	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
\|/ \| \| \| \| \| \| \| \| \| \| \| \|	We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
*	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
	We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.