aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Expand)Author
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
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-08-30add "Print Ring" and "Print Field" vernacular commandsgareuselesinge
2013-08-30Fixing the code of field_simplify_eq.amahboub
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-23Fixing an incompleteness of the ring/field tacticsamahboub
2013-08-22Correcting misplaced Proof command.amahboub
2013-08-22Fixing a significant efficiency leak in the code of the field tactic.amahboub
2013-08-22Field_theory : faster and nicer proofs + nice notations.letouzey
2013-08-22Ring_polynom : shorter proof for Psub_okletouzey
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-06-22Now, idtac closures use maps instead of association list.ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:38:06 +0000