index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
Commit message (
Expand
)
Author
Age
*
Simple machinery to detect EXTEND that interpret during parsing
gareuselesinge
2013-08-08
*
Coqide ported to STM
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Vcs data structure (Git inspired builder for Dag)
gareuselesinge
2013-08-08
*
Dag data structure
gareuselesinge
2013-08-08
*
Searchable stack data structure
gareuselesinge
2013-08-08
*
Future library to represent pure computations
gareuselesinge
2013-08-08
*
Small fix in IStream interface.
ppedrot
2013-08-08
*
Added more flags choice in desambiguating printer. The code is
ppedrot
2013-08-06
*
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
*
Using functors to reduce the boilerplate used in registering
ppedrot
2013-06-30
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Changing the type of Ltac values. Now they are toplevel generic
ppedrot
2013-06-12
*
Flags V8_4 for compatibility infrastructure.
herbelin
2013-06-02
*
More clever implemenation for IStream.
ppedrot
2013-05-29
*
Setting "appcontext" as the default behaviour in Ltac matching.
ppedrot
2013-05-28
*
Adding a persistent stream data structure.
ppedrot
2013-05-28
*
Fixing #3042
ppedrot
2013-05-23
*
Fixing Pp.strbrk which was reversing words.
ppedrot
2013-05-16
*
std_ppcmds is persistent, errors can be printed twice
gareuselesinge
2013-05-16
*
Gmap is now useless, hail to Map!
ppedrot
2013-05-14
*
Removing Fmap from libraries, it is not used anymore.
ppedrot
2013-05-14
*
Removing Fset, since it is not used anymore.
ppedrot
2013-05-12
*
Removing the use of Fset/Fmap from Trie. There was actually only
ppedrot
2013-05-12
*
Added a generic notion of hook. Hooks are functions to be set
ppedrot
2013-05-12
*
Documenting the Tries module, uniformizing the names according to
ppedrot
2013-05-09
*
Getting rid of module Gmapl.
ppedrot
2013-05-09
*
Xml_datatype.mli ships the xml type
gareuselesinge
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Fixing ocamldoc compilation.
ppedrot
2013-05-06
*
New module Xml_printer (dual to Xml_parser)
gareuselesinge
2013-05-06
*
Now printing body of abbreviations (i.e. notation with a name) with
herbelin
2013-05-05
*
Coqide: Globalization feedback (proof of concept)
gareuselesinge
2013-04-25
*
Flag ide_slave moved into Flags module
gareuselesinge
2013-04-25
*
raise UnsafeSuccess -> feedback AddedAxiom
gareuselesinge
2013-04-25
*
Coqide: new feedback mechanism for structured content
gareuselesinge
2013-04-25
*
Fix indentation
gareuselesinge
2013-04-25
*
Remove deprecated option -no-hash-consing (currently doing nothing)
letouzey
2013-04-23
*
interface.mli and serialize.ml reworked to avoid copy/paste of types
gareuselesinge
2013-04-19
*
More in IArray
ppedrot
2013-04-16
*
votour: a small tool for guided tours of .vo
letouzey
2013-04-15
*
More functional implementation of locality_flag and program_mode
gareuselesinge
2013-04-15
*
Added a module of immutable arrays. Not as full as CArray, but should
ppedrot
2013-04-09
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Removing mandatory suffixes for library files.
ppedrot
2013-03-21
*
Checker: simplify a bit its exception handler
letouzey
2013-03-17
*
Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical
letouzey
2013-03-14
[next]