aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
Commit message (Expand)AuthorAge
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Revert "Adding printers for ring and field commands."Gravatar Hugo Herbelin2016-04-27
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
* Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
* Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Getting rid of dynamic hacks in Setoid_newring.Gravatar Pierre-Marie Pédrot2015-12-04
* | Removing the last use of tacticIn in setoid_ring.Gravatar Pierre-Marie Pédrot2015-12-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
| * Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| * Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* | Adding a proper interface to Newring.Gravatar Pierre-Marie Pédrot2015-01-25
* | Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Ring: prevent an error message to show in case of success.Gravatar Arnaud Spiwack2014-08-05
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* Fix to make Coq compile, I think this should still be accepted.Gravatar Matthieu Sozeau2014-08-03
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06