coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-05	Merge numeral and string notation plugins	Pierre Roux

2020-11-05	[numeral notation] Handle implicit arguments	Pierre Roux

2020-11-04	[numeral notation] Adding the via ... using ... option	Pierre Roux
	This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R.
2020-10-30	Renaming numnotoption into number_modifier	Pierre Roux

2020-10-27	Rename misc nonterminals	Jim Fehrle

2020-09-11	Rename Numeral Notation command to Number Notation	Pierre Roux
	Keep Numeral Notation wit a deprecation warning.
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
	Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22	Adding bignat to parse positive numbers; bigint now includes negative ints.	Hugo Herbelin
	Warning: in notations, the name "bigint" actually meant "bignat". A clarification will eventually be needed.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-05-24	Use global env in numeral and string notations	Maxime Dénès
	Since their introduction, these notations were incorrectly using the proof-local environment.
2019-05-03	Fix #10054: Numeral Notations without the ltac plugin.	Pierre-Marie Pédrot
	It was fairly easy, the plugin defined an argument that was only used in a vernacular extension. Thus marking it as VERNAC was enough not to link to Ltac.
2019-03-27	[coqpp] [ltac] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
	We add state handling to tactics. TODO: - [rewrite] `add_morphism_infer` creates problems as it opens a proof. - [g_obligations] with_tac
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
	This should make https://github.com/coq/coq/pull/9129 easier.
2018-11-02	coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax	Gaëtan Gilbert
	I think for instance the new code in this diff is cleaner and more systematic: ~~~diff VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -\| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +\| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function \| TacticDefinition ({CAst.v=r},_) -> r \| TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater } -> { - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END ~~~
2018-11-02	Command driven attributes.	Gaëtan Gilbert
	Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes.
2018-11-02	Move attributes out of vernacinterp to new attributes module	Gaëtan Gilbert

2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot
	Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code.