index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
setoid_ring
Commit message (
Expand
)
Author
Age
*
Ncring_initial: avoid a notation overriding
Pierre Letouzey
2016-09-29
*
Ring_theory: avoid overriding a few notations
Pierre Letouzey
2016-09-28
*
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Removing tactic compatibility layers in setoid_ring.
Pierre-Marie Pédrot
2016-06-24
*
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
Adding printers for ring and field commands.
Hugo Herbelin
2016-06-16
*
Remove inappropriate comment.
Maxime Dénès
2016-06-16
*
Merge remote-tracking branch 'github/evarunsafe' into trunk
Matthieu Sozeau
2016-06-14
|
\
|
*
newring: fix for hack using evars as integers.
Matthieu Sozeau
2016-06-09
*
|
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-06-08
|
/
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Revert "Adding printers for ring and field commands."
Hugo Herbelin
2016-04-27
*
Adding printers for ring and field commands.
Hugo Herbelin
2016-04-27
*
Getting rid of the "_mods" parsing entry.
Pierre-Marie Pédrot
2016-04-01
*
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
Removing useless grammar.cma dependencies.
Pierre-Marie Pédrot
2016-03-06
*
Making parentheses mandatory in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
External tactics and notations now accept any tactic argument.
Pierre-Marie Pédrot
2015-12-30
*
|
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
Getting rid of dynamic hacks in Setoid_newring.
Pierre-Marie Pédrot
2015-12-04
*
|
Removing the last use of tacticIn in setoid_ring.
Pierre-Marie Pédrot
2015-12-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
|
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
*
Univs: fix evar_map initialization in newring.
Matthieu Sozeau
2015-10-02
*
|
Merge v8.5 into trunk
Hugo Herbelin
2015-05-15
|
\
|
|
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
|
*
Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)
Hugo Herbelin
2015-02-12
|
*
Capital letter in plugins.
Hugo Herbelin
2015-02-12
*
|
Adding a proper interface to Newring.
Pierre-Marie Pédrot
2015-01-25
*
|
Embedding the index of the ML tactic entry in the Tacexpr AST.
Pierre-Marie Pédrot
2015-01-21
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Feedback message: hold extra info to help routing
Enrico Tassi
2014-10-31
*
Removing an Evd.merge in Newring.
Pierre-Marie Pédrot
2014-10-27
*
Fix some typos in comments.
Guillaume Melquiond
2014-10-27
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Fix cbn behavior wrt simpl no match
Pierre Boutillier
2014-10-01
[next]