aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Generate more user-readable tactic notation kernel names.Gravatar Pierre-Marie Pédrot2016-05-16
* Merge pull request #170 from relrod/patch-1Gravatar Pierre-Marie Pédrot2016-05-16
|\
| * Fix a really small doc typoGravatar Ricky Elrod2016-05-15
|/
* Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Gravatar Pierre-Marie Pédrot2016-05-14
* Dyn: simplify API introducing an Easy submoduleGravatar Enrico Tassi2016-05-13
* More informative error message when interpreting ltac variables in terms.Gravatar Pierre-Marie Pédrot2016-05-13
* Thorough rewriting of the Pcoq API towards safety and static invariants.Gravatar Pierre-Marie Pédrot2016-05-11
|\
| * The grammar_extend function now registers unsynchronized extensions.Gravatar Pierre-Marie Pédrot2016-05-11
| * Making the grammar command extend API purely functional.Gravatar Pierre-Marie Pédrot2016-05-11
| * Moving the constr empty entry registering to the state-based API.Gravatar Pierre-Marie Pédrot2016-05-11
| * Turning the grammar extend command API into a state-passing one.Gravatar Pierre-Marie Pédrot2016-05-11
| * Moving the grammar summary to Pcoq.Gravatar Pierre-Marie Pédrot2016-05-11
| * Delimiting the use of unsafe code in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
| * Overlooked use of Gram instead of G module in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
| * Further tidying of the constr extension code.Gravatar Pierre-Marie Pédrot2016-05-10
| * Type-safe constr notations.Gravatar Pierre-Marie Pédrot2016-05-10
| * AlistNsep token now accepts an arbitrary separator.Gravatar Pierre-Marie Pédrot2016-05-10
| * Simpler data structure for Arules token.Gravatar Pierre-Marie Pédrot2016-05-10
| * Purer implementation of empty level registering in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
| * Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
| * Hardening the obsolete unsafe_grammar_statement API.Gravatar Pierre-Marie Pédrot2016-05-10
| * Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-05-10
|/
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
* STM: code cleanupGravatar Enrico Tassi2016-05-10
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Fix bug #3887: Better error message for "More than one program with unsolved ...Gravatar Pierre-Marie Pédrot2016-05-09
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| * Fix typo in configure's option description.Gravatar Guillaume Melquiond2016-05-09
| * Use "md5 -q" on FreeBSD architectures (bug #4719).Gravatar Guillaume Melquiond2016-05-09
| * Use the actual location of an error in the error pane (bug #4169).Gravatar Guillaume Melquiond2016-05-09
* | Exposing structure of the entries to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
|\ \
| * | Actually using the symbol information to print Tactic Notations properly.Gravatar Pierre-Marie Pédrot2016-05-08
| * | Removing dead code in Pptactic.Gravatar Pierre-Marie Pédrot2016-05-08
| * | Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
|/ /
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Change the toplevel representation of Ltac values to an untyped one.Gravatar Pierre-Marie Pédrot2016-05-08
|\ \
| | * Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Gravatar Pierre-Marie Pédrot2016-05-08
| * | Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
| | * typoGravatar Enrico Tassi2016-05-04
| | * NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
| * | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
| * | Removing the Value.of_* API for parameterized types.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Do not generate generic arguments for data which only requires toplevel values.Gravatar Pierre-Marie Pédrot2016-05-04
| * | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Simplifying the code of Tacinterp.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
| * | Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 05:21:17 +0000