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
*
Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...
Maxime Dénès
2017-05-26
|
\
*
\
Merge PR#655: Extra functions exported in EConstr
Maxime Dénès
2017-05-26
|
\
\
*
\
\
Merge PR#645: [stm] Tweak debug options.
Maxime Dénès
2017-05-25
|
\
\
\
*
\
\
\
Merge PR#406: coq makefile2
Maxime Dénès
2017-05-25
|
\
\
\
\
*
|
|
|
|
[location] Renaming "CAst.ast" to "CAst.t"
Matej Košík
2017-05-24
*
|
|
|
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
\
\
\
|
|
*
|
|
|
coq_makefile: avoid spurious ./ in generated .conf file
Enrico Tassi
2017-05-23
|
|
*
|
|
|
enters coq_makefile2
Enrico Tassi
2017-05-23
|
|
*
|
|
|
ocamlfind: coqtop -config prints ocamlfind as found by ./configure
Enrico Tassi
2017-05-23
|
|
*
|
|
|
print_config: print COQ_SRC_SUBDIRS
Enrico Tassi
2017-05-23
|
|
*
|
|
|
Put the list of Coq sources subdirectories in one place
Enrico Tassi
2017-05-23
|
|
*
|
|
|
Usage.print_config moved to Envars
Enrico Tassi
2017-05-23
|
|
*
|
|
|
CoqProject_file: document in API deprecated features
Enrico Tassi
2017-05-23
|
|
*
|
|
|
CoqProject_file: API and code cleanup (tuples -> records)
Enrico Tassi
2017-05-23
|
|
*
|
|
|
ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli
Enrico Tassi
2017-05-23
|
|
/
/
/
/
|
|
|
|
*
Bigint.euclid: clarify which sign convention is used
Pierre Letouzey
2017-05-23
|
|
|
_
|
/
|
|
/
|
|
|
|
|
*
Moving "sym" on "eq" type to lib/util.ml.
Hugo Herbelin
2017-05-19
|
|
*
|
[stm] Tweak debug options.
Emilio Jesus Gallego Arias
2017-05-18
|
|
/
/
|
*
|
Documenting Option.List.find.
Hugo Herbelin
2017-05-05
|
*
|
Cosmetic: unifying style within option.ml.
Hugo Herbelin
2017-05-05
|
*
|
Upgrading some local function as a general-purpose combinator Option.List.map.
Hugo Herbelin
2017-05-05
|
|
/
|
*
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
|
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
|
*
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
|
*
Remove unused [rec] keywords
Gaetan Gilbert
2017-04-27
|
*
Locally disable some warnings.
Gaetan Gilbert
2017-04-27
*
|
[location] Cleanup.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Document changes.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Remove `Loc.internal_ghost`
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Move Glob_term.cases_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-24
|
/
*
[flags] Deprecate is_silent/is_verbose in favor of single flag.
Emilio Jesus Gallego Arias
2017-04-21
*
[flags] Documentation and a minor tweak.
Emilio Jesus Gallego Arias
2017-04-12
*
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-12
*
[stm] Remove edit_id.
Emilio Jesus Gallego Arias
2017-04-12
*
[toplevel] Remove exception error printer in favor of feedback printer.
Emilio Jesus Gallego Arias
2017-04-05
*
Merge PR#502: [pp] Add anomaly header to error messages.
Maxime Dénès
2017-04-04
|
\
*
\
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-24
|
\
\
|
|
*
[pp] Add anomaly header to anomaly error messages.
Emilio Jesus Gallego Arias
2017-03-22
|
|
/
|
/
|
*
|
[pp] Hide the internal representation of `std_ppcmds`.
Emilio Jesus Gallego Arias
2017-03-21
*
|
[pp] [ide] Minor cleanups in pp code.
Emilio Jesus Gallego Arias
2017-03-21
*
|
[pp] Move terminal-specific tagging to the toplevel.
Emilio Jesus Gallego Arias
2017-03-21
*
|
[pp] Remove special tag type and handler from Pp.
Emilio Jesus Gallego Arias
2017-03-21
*
|
[pp] Debug feeder is not needed anymore.
Emilio Jesus Gallego Arias
2017-03-21
*
|
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-03-21
[next]