aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Expand)Author
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
2014-04-28Remove unused lookup table.Guillaume Melquiond
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-08Less dependencies in Omega.Pierre-Marie Pédrot
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-11-21Field_theory: nicer notations for constants 0 1 ...Pierre Letouzey
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 11:31:22 +0000