index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
Age
Commit message (
Expand
)
Author
2017-05-26
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-25
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-24
[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-23
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-19
Moving "sym" on "eq" type to lib/util.ml.
Hugo Herbelin
2017-05-18
[stm] Tweak debug options.
Emilio Jesus Gallego Arias
2017-05-05
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-04-27
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-25
[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-24
[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-21
[flags] Deprecate is_silent/is_verbose in favor of single flag.
Emilio Jesus Gallego Arias
2017-04-12
[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-05
[toplevel] Remove exception error printer in favor of feedback printer.
Emilio Jesus Gallego Arias
2017-04-04
Merge PR#502: [pp] Add anomaly header to error messages.
Maxime Dénès
2017-03-24
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-22
[pp] Add anomaly header to anomaly error messages.
Emilio Jesus Gallego Arias
2017-03-21
[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
[next]