index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
*
Printers for ltac environments.
Hugo Herbelin
2014-04-05
*
A debug printer for Evd.Filter.t
Pierre Boutillier
2014-04-02
*
Updated debugging printers
Hugo Herbelin
2014-04-01
*
Adding a canary library. This canary is imperfect. It allows serialization
Pierre-Marie Pédrot
2014-03-05
*
Added a new module HMap. It works (almost) like Map, except that it expects
Pierre-Marie Pédrot
2014-03-05
*
Adding a CSet module in Coq lib.
Pierre-Marie Pédrot
2014-03-05
*
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
*
Set officially the minimal OCaml requirement to 3.12.1
Pierre Letouzey
2014-03-02
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Makefile: re-introduce 2 phases to avoid make strange -include's
Pierre Letouzey
2014-02-27
*
Code refactoring thanks to the new Monad module.
Arnaud Spiwack
2014-02-27
*
Remove unsafe code (Obj.magic) in Tacinterp.
Arnaud Spiwack
2014-02-27
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
app_node, stack, state printers
Pierre Boutillier
2014-02-24
*
'Pretty' printer for wf_paths
Pierre
2014-01-11
*
Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd
Pierre Letouzey
2014-01-08
*
Aux_file: cache information at compile time for later (re)use
Enrico Tassi
2014-01-04
*
Support for evars and metas in native compiler.
Maxime Dénès
2013-12-30
*
Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at
Pierre-Marie Pédrot
2013-12-22
*
configure.ml: our configure script is now written in ML :-)
Pierre Letouzey
2013-12-20
*
Adding printing of ltac envs to debugger.
Pierre-Marie Pédrot
2013-11-30
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-25
*
A file listing old svn branches and tags
letouzey
2013-11-18
*
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...
aspiwack
2013-11-02
*
Removes Refine from the dev tools now that the module has been deleted.
aspiwack
2013-11-02
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
- install evar printer for debugging
msozeau
2013-10-29
*
Ephemeron: marshaling friendly keys
gareuselesinge
2013-10-18
*
Adding evar printing to debugger.
ppedrot
2013-09-24
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Moving Searchstack to CStack, and normalizing names a bit.
ppedrot
2013-09-06
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Fix compilation of dev/printres.cma
gareuselesinge
2013-08-20
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Future library to represent pure computations
gareuselesinge
2013-08-08
*
Small cleaning of printing coercion failures in Ltac interpretation.
ppedrot
2013-08-04
*
Removing SortArgType.
ppedrot
2013-07-05
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Adding genarg printer to debugger.
ppedrot
2013-06-19
*
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
2013-06-18
*
Added Genarg as generic argument type.
ppedrot
2013-06-12
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
Adding a persistent stream data structure.
ppedrot
2013-05-28
*
Gmap is now useless, hail to Map!
ppedrot
2013-05-14
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
[next]