aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
| | | | | | | | We don't want "Anomaly: Returned a functional value in a type not recognized as a product type.. Please report at http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional value in a type not recognized as a product type. Please report at http://coq.inria.fr/bugs/."
* Merge PR#720: Reformat Makefile.ciGravatar Maxime Dénès2017-06-02
|\
* \ Merge PR#708: [ide] Correct merging error.Gravatar Maxime Dénès2017-06-02
|\ \
* \ \ Merge PR#691: [travis] Add OSX test-suite checking.Gravatar Maxime Dénès2017-06-02
|\ \ \
* \ \ \ Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \ \ \
* \ \ \ \ Merge PR#499: Drop all "theories/*/vo.itarget" files and compute the ↵Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | corresponding information automatically.
* \ \ \ \ \ Merge PR#515: extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | "plugins/micromega/MExtraction.v"
* \ \ \ \ \ \ Merge PR#711: [gitlab] Artifact test suite logs on failure.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \ \
| | | | | * | | [travis] Add OSX test-suite checking.Gravatar Maxime Dénès2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a first step towards getting Travis build our OSX package, but is also useful immediately (c.f. the recent breakage of the coq_makefile test-suite under OSX).
| | | | | * | | Test-suite: do not test native compiler if disabled by configure.Gravatar Maxime Dénès2017-06-01
| | | | | | | |
| | | * | | | | drop vo.itarget files and compute the corresponding the corresponding values ↵Gravatar Matej Kosik2017-06-01
| | |/ / / / / | | | | | | | | | | | | | | | | | | | | | automatically instead
* | | | | | | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#670: Postponing of universe constraints unification in term equality.Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \
| | | | | * | | | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
* | | | | | | | | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \
* | | | | | | | | | Remove a post merge warning.Gravatar Maxime Dénès2017-06-01
| | | | | | | | | |
* | | | | | | | | | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | Fix coq_makefile uninstall target under OSX.Gravatar Maxime Dénès2017-06-01
| | | | | | | |/ / /
* | | | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | recursive notations) (bis)
| | | | | | | * | | Break circular dependency in MExtractionGravatar Jason Gross2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Described in https://github.com/coq/coq/pull/515#discussion_r119230833
| | | | | | | * | | a solution that works also with make 3.81Gravatar Matej Kosik2017-06-01
| | | | | | | | | |
| | | | | | | * | | extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Matej Kosik2017-06-01
| |_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | "plugins/micromega/MExtraction.v"
* | | | | | | | | Merge PR#704: Fix empty parentheses display in test-suiteGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#701: [readlink -f] doesn't work on OSXGravatar Maxime Dénès2017-05-31
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * Reformat Makefile.ciGravatar Jason Gross2017-05-31
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
* | | | | | | | | | Merge PR#248: Adding eassert, eset, epose, etc.Gravatar Maxime Dénès2017-05-31
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | Makefile.build: test-suite all = run + report, so don't report againGravatar Gaëtan Gilbert2017-05-31
| | | | | | | | | | |
| | | | | | | | | * | [travis] print failing test suite logs on failureGravatar Gaëtan Gilbert2017-05-31
| | | | | | | | | | |
| | | | | | | | * | | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| | | | | | | | | | |
| | | | | | | | * | | Documenting the new behaviour of specialize.Gravatar Pierre Courtieu2017-05-31
| | | | | | | | | | |
| | | | | | | | * | | Make specialize smarter.Gravatar Pierre Courtieu2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now when a partial with-binding is given the unsolved parameters are left quantified. A letin is added when mixing (fun x => ...) and with-bindings.
* | | | | | | | | | | Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that ↵Gravatar Maxime Dénès2017-05-31
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | are composed from uppercase letters
| | | | | | * | | | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
| | | | | | * | | | | Renaming interp_rawcontext_evars using a more "standard" name.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | | | * | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of a complex function doing both an incremental comparison and an effect on names (Notation_ops.compare_glob_constr). For the effect on names, it was actually already done at the time of turning glob_constr to notation_constr, so it could be skipped here. For the comparison, we rely on a new incremental variant of Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the artificial recursivity in mk_glob_constr_eq). Seizing the opportunity to get rid of catch-all clauses in pattern-matching (as advocated by Maxime). Also make indentation closer to the one of other functions.
| | | | | * | | | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
| | | | | | | | * [ide] Correct merging error.Gravatar Emilio Jesus Gallego Arias2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a mistake in the conflict resolution of merge 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and sorry for the problem.
* | | | | | | | | Merge PR#706: Add some test-suite generated files to .gitignoreGravatar Maxime Dénès2017-05-30
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ |/| | | | | | | |
| | | | | | | | * [gitlab] Artifact test suite logs on failure.Gravatar Gaëtan Gilbert2017-05-30
| |_|_|_|_|_|_|/ |/| | | | | | |
| * | | | | | | Add some test-suite generated files to .gitignoreGravatar Jason Gross2017-05-30
|/ / / / / / /
| | | | * / / Fix empty parentheses display in test-suiteGravatar Jason Gross2017-05-30
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was an extra trailing space in #680. Now things display as, e.g., ``` TEST bugs/opened/3754.v TEST bugs/opened/4803.v (-compat 8.4) ``` instead of ``` TEST bugs/opened/3754.v ( ) TEST bugs/opened/4803.v (-compat 8.4 ) ```
| | | * | | [readlink -f] doesn't work on OSXGravatar Gaëtan Gilbert2017-05-30
| |_|/ / / |/| | | | | | | | | | | | | | We only want an absolute path, no need to follow symlinks.
| | * | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
| | * | | Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | Includes fixes and suggestions from Théo.
| | * | | Few tests for e-variants of assert, set, remember.Gravatar Hugo Herbelin2017-05-30
| | | | |
| | * | | Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | evars. This is for consistency with the rest of the language. For instance, "eremember" and "epose" are supposed to refer to terms occurring in the goal, hence not leaving evars, hence in general pointless. Eventually, I guess that "e" should be a modifier (see e.g. the discussion at #3872), or the difference is removed.
| | * | | Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
| |/ / / |/| | | | | | | | | | | a goal with unresolved evars.
| * | | make sure that "ocamllibdep" properly recognizes Ocaml modules that are all ↵Gravatar Matej Košík2017-05-30
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | upper-case At the moment, when one tries to add an Ocaml module to Coq code-base which is composed just from upper-cases letters, the compilation fails with an error: File "......ml", line 1: Error: Error while linking ... Reference to undefined global `FOO' This commit removes the restriction.
* | | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ \ | | | | | | | | | | | | more uniform
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 05:07:04 +0000