aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Expand)AuthorAge
* Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...Gravatar Maxime Dénès2017-05-26
|\
* \ Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\ \
* \ \ Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* | | | | [location] Renaming "CAst.ast" to "CAst.t"Gravatar Matej Košík2017-05-24
* | | | | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \ \
| | * | | | coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
| | * | | | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | * | | | ocamlfind: coqtop -config prints ocamlfind as found by ./configureGravatar Enrico Tassi2017-05-23
| | * | | | print_config: print COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-05-23
| | * | | | Put the list of Coq sources subdirectories in one placeGravatar Enrico Tassi2017-05-23
| | * | | | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| | * | | | CoqProject_file: document in API deprecated featuresGravatar Enrico Tassi2017-05-23
| | * | | | CoqProject_file: API and code cleanup (tuples -> records)Gravatar Enrico Tassi2017-05-23
| | * | | | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
| |/ / / /
| | | | * Bigint.euclid: clarify which sign convention is usedGravatar Pierre Letouzey2017-05-23
| | |_|/ | |/| |
| | | * Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
| | * | [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| |/ /
| * | Documenting Option.List.find.Gravatar Hugo Herbelin2017-05-05
| * | Cosmetic: unifying style within option.ml.Gravatar Hugo Herbelin2017-05-05
| * | Upgrading some local function as a general-purpose combinator Option.List.map.Gravatar Hugo Herbelin2017-05-05
| |/
| * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| * Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
* | [location] Cleanup.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Document changes.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/
* [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
* Merge PR#502: [pp] Add anomaly header to error messages.Gravatar Maxime Dénès2017-04-04
|\
* \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
|\ \
| | * [pp] Add anomaly header to anomaly error messages.Gravatar Emilio Jesus Gallego Arias2017-03-22
| |/ |/|
* | [pp] Hide the internal representation of `std_ppcmds`.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] Debug feeder is not needed anymore.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21