aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
Commit message (Expand)AuthorAge
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Ring: prevent an error message to show in case of success.Gravatar Arnaud Spiwack2014-08-05
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* Fix to make Coq compile, I think this should still be accepted.Gravatar Matthieu Sozeau2014-08-03
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
* Fix Field_tac to get fast reification again, with the fix on template univers...Gravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove unused lookup table.Gravatar Guillaume Melquiond2014-04-28
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Field_theory: nicer notations for constants 0 1 ...Gravatar Pierre Letouzey2013-11-21
* More Proofview.Goal.enter.Gravatar aspiwack2013-11-02
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* add "Print Ring" and "Print Field" vernacular commandsGravatar gareuselesinge2013-08-30
* Fixing the code of field_simplify_eq.Gravatar amahboub2013-08-30
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Fixing an incompleteness of the ring/field tacticsGravatar amahboub2013-08-23
* Correcting misplaced Proof command.Gravatar amahboub2013-08-22
* Fixing a significant efficiency leak in the code of the field tactic.Gravatar amahboub2013-08-22
* Field_theory : faster and nicer proofs + nice notations.Gravatar letouzey2013-08-22