aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Allow empty instance parsing @{}Gravatar Matthieu Sozeau2017-09-19
* Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\
* | Fix CHANGES after merge of PR #1025.Gravatar Théo Zimmermann2017-09-15
* | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Gravatar Maxime Dénès2017-09-15
|\ \ \
* \ \ \ Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \ \ \
* \ \ \ \ Merge PR #1046: Better error messages, fix for BZ#5723Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1045: Remove unneeded fix for BZ#1715Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1042: Fixing minor typos in stm/coqideGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1000: Update CREDITS on a best-effort basis.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #1025: BZ#5716, read flags from project file for Compile BufferGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #990: Prevent warning about DSTROOT being undefined.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #962: Move dev/doc/changes to Markdown.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #938: [parsing] Remove hacks for reduced Prelude.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | * | | Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | Merge PR #981: Miscellaneous fixes for notationsGravatar Maxime Dénès2017-09-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | * Fix GitLab CIGravatar Gaëtan Gilbert2017-09-13
| * | | | | | | | | | | | | | | | | Fixing bug #5693 (treating empty notation format as any format).Gravatar Hugo Herbelin2017-09-12
| * | | | | | | | | | | | | | | | | Adding a missing period in a notation warning.Gravatar Hugo Herbelin2017-09-12
| * | | | | | | | | | | | | | | | | Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.Gravatar Hugo Herbelin2017-09-12
| * | | | | | | | | | | | | | | | | Don't exclude a priori CLocalDef to be treated by ppconstr.ml.Gravatar Hugo Herbelin2017-09-12
| * | | | | | | | | | | | | | | | | Fixing a typo in printing notations with recursive binders.Gravatar Hugo Herbelin2017-09-12
| * | | | | | | | | | | | | | | | | Fixing a bug of recursive notations introduced in dfdaf4de.Gravatar Hugo Herbelin2017-09-12
| * | | | | | | | | | | | | | | | | Fixing little inaccuracy in coercions to ident or name.Gravatar Hugo Herbelin2017-09-12
|/ / / / / / / / / / / / / / / / /
| | | | | | | | | | | | | | * / / Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | Better error messages, fix for BZ#5723Gravatar Paul Steckler2017-09-11
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificial...Gravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * | | Remove unneeded fix for BZ#1715Gravatar Gaëtan Gilbert2017-09-11
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR #1032: Make our CI policy clearer and more explicitGravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Gravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1035: Fix the introduction of SSR refman chapter.Gravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1029: Fix a refine anomaly "Evar defined twice".Gravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1014: Add option index entry for NativeCompute ProfilingGravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1004: Document primitive projections in more detailGravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #987: In Array.smartmap, read and write from same arrayGravatar Maxime Dénès2017-09-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | * | | In stm, fixing a typo about flushing debugging messages.Gravatar Hugo Herbelin2017-09-11
| | | | | | | | | | | | | | | | | | | * | | Typo in the header of ide_slave.ml.Gravatar Hugo Herbelin2017-09-11
| | | | | | | | | | | | | | | | | | | * | | Coqide: adding a separating space in some debugging messages.Gravatar Hugo Herbelin2017-09-11
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | * | | | | | | | | | | | | | | Fix Typo in Doc for `Set Parsing Explicit`Gravatar staffehn2017-09-08
| |_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | Fix the introduction of SSR refman chapter.Gravatar Théo Zimmermann2017-09-08
| |_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | Move README.ci and link to it from CONTRIBUTING.Gravatar Théo Zimmermann2017-09-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:16:39 +0000