aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-09-22Merge PR #1061: Fix appveyor buildMaxime Dénès
2017-09-21Do not reinstall preinstalled packages under AppVeyor.Maxime Dénès
It seems that reinstalling gcc can leave Cygwin in a strange state, where invocations of gcc fail suddenly. I haven't figure out exactly why, but this seems to fix it.
2017-09-21Print Cygwin setup output rather than logging in to a file.Maxime Dénès
2017-09-19Merge PR #1036: Unify EConstr.t equalityMaxime Dénès
2017-09-19Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Maxime Dénès
2017-09-19Merge PR #1043: Disable OSX signing for temporary artifacts.Maxime Dénès
2017-09-19Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.Maxime Dénès
2017-09-19Merge PR #920: kernel: bugfix in filter_stack_domain.Maxime Dénès
2017-09-18Add test-suite script by Cyprien ManginMatthieu Sozeau
2017-09-15Merge PR #979: Fix install-doc target and other gitlab failuresMaxime Dénès
2017-09-15Fix CHANGES after merge of PR #1025.Théo Zimmermann
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Maxime Dénès
top of the linking chain.
2017-09-15Merge PR #1051: Using an algebraic type for distinguishing toplevel input ↵Maxime Dénès
from location in file
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-15Merge PR #1046: Better error messages, fix for BZ#5723Maxime Dénès
2017-09-15Merge PR #1045: Remove unneeded fix for BZ#1715Maxime Dénès
2017-09-15Merge PR #1042: Fixing minor typos in stm/coqideMaxime Dénès
2017-09-15Merge PR #1000: Update CREDITS on a best-effort basis.Maxime Dénès
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-15Merge PR #1025: BZ#5716, read flags from project file for Compile BufferMaxime Dénès
2017-09-15Add debug output to brew update.Maxime Dénès
2017-09-15Switch Travis to OSX 10.12 and Xcode 8.3.3.Maxime Dénès
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Maxime Dénès
Inductive-keyworded record failing even on non-dependent goal)
2017-09-15Merge PR #990: Prevent warning about DSTROOT being undefined.Maxime Dénès
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Maxime Dénès
work better on them
2017-09-15Merge PR #962: Move dev/doc/changes to Markdown.Maxime Dénès
2017-09-15Merge PR #955: Do not hashcons universes beforehandMaxime Dénès
2017-09-15Merge PR #938: [parsing] Remove hacks for reduced Prelude.Maxime Dénès
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵Maxime Dénès
anonymous variables)
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-09-14Avoid extra failure in the "constructor" tactic (bug #5666).Guillaume Melquiond
This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n.
2017-09-13Merge PR #981: Miscellaneous fixes for notationsMaxime Dénès
2017-09-13Fix GitLab CIGaëtan Gilbert
- timing needs time and python - check for compiled files without source looks in the install directory (except for make -f Makefile.ci which doesn't check), as such the install directory has been renamed to _install_ci and isn't searched.
2017-09-12Fixing bug #5693 (treating empty notation format as any format).Hugo Herbelin
A trick in counting spaces in a format was making the empty notation not behaving correctly.
2017-09-12Adding a missing period in a notation warning.Hugo Herbelin
2017-09-12Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.Hugo Herbelin
Conditions for printing 'pat were incomplete.
2017-09-12Don't exclude a priori CLocalDef to be treated by ppconstr.ml.Hugo Herbelin
2017-09-12Fixing a typo in printing notations with recursive binders.Hugo Herbelin
Was causing a failure to print recursive binders used twice or more in the same notation.
2017-09-12Fixing a bug of recursive notations introduced in dfdaf4de.Hugo Herbelin
When a proper notation variable occurred only in a recursive pattern of the notation, the notation was wrongly considered non printable due (the side effect that function compare_glob_constr and that mk_glob_constr_eq does not do anymore was indeed done by aux' but thrown away). This fixes it.
2017-09-12Fixing little inaccuracy in coercions to ident or name.Hugo Herbelin
For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-09-11Better error messages, fix for BZ#5723Paul Steckler
2017-09-11Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right ↵Maxime Dénès
artificially restricted to a non-empty context).
2017-09-11Remove unneeded fix for BZ#1715Gaëtan Gilbert
It hasn't been necessary since 6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb introduced $(INSTALLLIB)
2017-09-11Merge PR #1032: Make our CI policy clearer and more explicitMaxime Dénès
2017-09-11Disable OSX signing for temporary artifacts.Maxime Dénès
The OSX binaries were signed twice with a fake identity, leading to some obscure errors on Travis in some cases. We disable code signing for Travis artifacts. For released packages, a proper signing will be applied manually.
2017-09-11Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Maxime Dénès
2017-09-11Merge PR #1035: Fix the introduction of SSR refman chapter.Maxime Dénès
2017-09-11Merge PR #1029: Fix a refine anomaly "Evar defined twice".Maxime Dénès
2017-09-11Merge PR #1014: Add option index entry for NativeCompute ProfilingMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 17:58:44 +0000