aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/newring.ml
Commit message (Expand)AuthorAge
* 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