coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès	2018-03-08
\| \| \| \| \| \| \| \| \|	Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| \| \| \| \| \| \| \| \|	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\| \| \| \| \|	To this extent we factor out the relevant bits to a new file, ltac_pretype.
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| \| \| \| \|	The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
*	Move type_uconstr to Tacinterp.	Maxime Dénès	2017-08-01
\|
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Merge PR#600: Some factorizations of ltac interpretation functions between ↵	Maxime Dénès	2017-06-06
\|\ \| \| \| \| \| \|	ssreflect and coq code
\| *	Factorizing interp_gen through a function interpreting glob_constr.	Hugo Herbelin	2017-05-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure.
\| *	Splitting interp_open_constr into two variants, with or without type classes.	Hugo Herbelin	2017-05-31
\|/ \| \| \| \| \| \|	This simplifies the API as before, inference of instances of type classes was iff a type constraint was given. We then export these both versions of interp_open_constr.
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \|
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ \| \| \|	Now it is a private field, locations are optional.
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\|
*	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.