aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Expand)Author
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-04Getting rid of dynamic hacks in Setoid_newring.Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix evar_map initialization in newring.Matthieu Sozeau
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-01-25Adding a proper interface to Newring.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-27Removing an Evd.merge in Newring.Pierre-Marie Pédrot
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-05Ring: prevent an error message to show in case of success.Arnaud Spiwack
2014-08-05Better fix of e5c025Pierre Boutillier
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-08-03Fix to make Coq compile, I think this should still be accepted.Matthieu Sozeau
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Fix Field_tac to get fast reification again, with the fix on template univers...Matthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 16:27:33 +0000