index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
glondu
2010-12-25
*
Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands
glondu
2010-12-25
*
Rename mkR* smart constructors (mostly in funind)
glondu
2010-12-25
*
s/raw/glob/g in decl_interp.ml for more consistency
glondu
2010-12-24
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename files in funind to respect new conventions
glondu
2010-12-24
*
Remove obsolete script univdot, update dev doc about universes
glondu
2010-12-24
*
tactics/eqdecide.ml4: avoid a useless argument in decideEquality
glondu
2010-12-24
*
Precision in documentation of "decide equality"
glondu
2010-12-24
*
Remove the two-argument variant of "decide equality"
glondu
2010-12-23
*
Fix diagram in genarg.mli
glondu
2010-12-23
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Prepare change of nomenclature rawconstr -> glob_constr
glondu
2010-12-23
*
More precise documentation for instantiate
glondu
2010-12-23
*
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
letouzey
2010-12-21
*
Fixing bug #2454: inversion predicate strategy for inferring the type
herbelin
2010-12-19
*
Univ: try to avoid a few lookup in the universe graph
letouzey
2010-12-18
*
Univ.constraints made fully abstract instead of being a Set of abstract stuff
letouzey
2010-12-18
*
Revert last commit 13723 on Univ : minor gains and more complex code
letouzey
2010-12-18
*
Univ: an attempt to lazily compact chains of Equiv in a functionnal way
letouzey
2010-12-17
*
NPeano.modulo : another trick a la "minus" for having a decreasing arg
letouzey
2010-12-17
*
Cosmetic : let's take advantage of the n-ary exists notation
letouzey
2010-12-17
*
Nicer log2 function for nat (suggested by Hugo)
letouzey
2010-12-17
*
Univ: two improvements (speed + space)
letouzey
2010-12-16
*
Clenv.connect_clenv without its Evd.fold
letouzey
2010-12-15
*
Evar-related speed-up and clarifications in Class_tactics and Rewrite
letouzey
2010-12-15
*
Misc improvements about evar_map
letouzey
2010-12-15
*
Add improved indenters that rely on the current proof state to choose the ind...
gmelquio
2010-12-14
*
Add navigation items for quickly moving between word occurrences.
gmelquio
2010-12-14
*
Improved the search/replace dialog box:
gmelquio
2010-12-14
*
Fix mutex being released from a different thread than it is acquired from.
gmelquio
2010-12-14
*
Remove an unused function with a Evd.fold in subtac
letouzey
2010-12-13
*
Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined
letouzey
2010-12-13
*
Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometry
letouzey
2010-12-13
*
Avoid silent loss of data when closing an unsaved buffer.
gmelquio
2010-12-13
*
Sorry for the mistake in r13702
pboutill
2010-12-12
*
Attempt to preserve casts during a refine, especially VMcast
letouzey
2010-12-10
*
First release of Vector library.
pboutill
2010-12-10
*
Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.
herbelin
2010-12-09
*
In passing, very quick uniformization of coqdoc headers in a few files.
herbelin
2010-12-09
*
ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2
letouzey
2010-12-09
*
Example of a simple ML tactic (Hello world).
fkirchne
2010-12-09
*
Fixed status of ÷ and × in coqdoc (they were seen as letter instead of symb...
herbelin
2010-12-06
*
Numbers and bitwise functions.
letouzey
2010-12-06
*
Use !Pp_control.std_ft for printing grammars
glondu
2010-12-06
*
Made new comm. model between coq and coqide support '-R foo ""'-style option.
herbelin
2010-12-04
*
Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).
herbelin
2010-12-04
*
Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).
herbelin
2010-12-04
*
Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,
herbelin
2010-12-04
[prev]
[next]