aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
Commit message (Expand)AuthorAge
* 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
* Ring_polynom : shorter proof for Psub_okGravatar letouzey2013-08-22
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* newring.ml4: interp constr arg at interp time (not parse time)Gravatar gareuselesinge2013-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 12:03:57 +0000