aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR#724: Move README.ci to markdownGravatar Maxime Dénès2017-06-05
|\
* \ Merge PR#726: [stm] Solve bug 5577 "STM branch name is incorrect with Time"Gravatar Maxime Dénès2017-06-05
|\ \
* \ \ Merge PR#722: [printing] Remove duplicated printing function.Gravatar Maxime Dénès2017-06-05
|\ \ \
* \ \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Gravatar Maxime Dénès2017-06-05
|\ \ \ \ | | | | | | | | | | | | | | | a flag suspectingly renamed in a clearer way
* \ \ \ \ Merge PR#526: solving implicit resolution in FunctionGravatar Maxime Dénès2017-06-04
|\ \ \ \ \
| | | | * | [stm] Solve bug 5577 "STM branch name is incorrect with Time"Gravatar Emilio Jesus Gallego Arias2017-06-03
| |_|_|/ / |/| | | |
* | | | | Merge PR#720: Reformat Makefile.ciGravatar Maxime Dénès2017-06-02
|\ \ \ \ \
| | | | | * Move README.ci to markdownGravatar Théo Zimmermann2017-06-02
| |_|_|_|/ |/| | | | | | | | | The file was already (mostly) following Markdown syntax so we just take advantage of this by moving to a .md extension.
* | | | | 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
| | | | | | | | | | |
| | | | | | | | * | | solving implicit resolution in FunctionGravatar Julien Forest2017-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"
| | | | | | | | | | * [printing] Remove duplicated printing function.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It seems there were 4 copies of the same function in the code base.
* | | | | | | | | | | 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
| | | | | | | | | | | * Adding overlay for math-comp.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | |
| | | | | | | | | | | * Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A priori considered to be a good programming style.
| | | | | | | | | | | * Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar.
| | | | | | * | | | | 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
| |_|_|_|_|_|_|/ |/| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-25 21:41:34 +0000