index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
setoid_ring
/
newring.ml4
Commit message (
Expand
)
Author
Age
*
Univs: fix evar_map initialization in newring.
Matthieu Sozeau
2015-10-02
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)
Hugo Herbelin
2015-02-12
*
Capital letter in plugins.
Hugo Herbelin
2015-02-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Feedback message: hold extra info to help routing
Enrico Tassi
2014-10-31
*
Removing an Evd.merge in Newring.
Pierre-Marie Pédrot
2014-10-27
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-08-18
*
STM: VtQuery holds the id of the state it refers to
Carst Tankink
2014-08-04
*
Qualified ML tactic names. The plugin name is used to discriminate
Pierre-Marie Pédrot
2014-07-27
*
Now parsing rules of ML-declared tactics are only made available after the
Pierre-Marie Pédrot
2014-05-12
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
Rework handling of universes on top of the STM, allowing for delayed
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove unused lookup table.
Guillaume Melquiond
2014-04-28
*
Removing useless try-with clauses in Goal.enter variants.
Pierre-Marie Pédrot
2014-04-25
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
add "Print Ring" and "Print Field" vernacular commands
gareuselesinge
2013-08-30
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Fixing an incompleteness of the ring/field tactics
amahboub
2013-08-23
*
Vernac classification streamlined (handles VERNAC EXTEND)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Now, idtac closures use maps instead of association list.
ppedrot
2013-06-22
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Hiding tactic value representations.
ppedrot
2013-06-10
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
newring.ml4: interp constr arg at interp time (not parse time)
gareuselesinge
2013-05-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
[next]