aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/newring.ml
Commit message (Expand)AuthorAge
...
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Removing tactic compatibility layers in setoid_ring.Gravatar Pierre-Marie Pédrot2016-06-24
* Merge remote-tracking branch 'github/evarunsafe' into trunkGravatar Matthieu Sozeau2016-06-14
|\
| * newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
* | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
|/
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
* 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
* 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
* 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
* 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
* Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
* Adding a proper interface to Newring.Gravatar Pierre-Marie Pédrot2015-01-25