aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | Merge PR#623: Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \
| * | | | | | | | Overlays.Gravatar Maxime Dénès2017-06-06
| | | | | | | | |
| * | | | | | | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* | | | | | | | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | short econstr-cleaning of record.ml
* \ \ \ \ \ \ \ \ Merge PR#728: A few typos.Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#600: Some factorizations of ltac interpretation functions between ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ssreflect and coq code
* \ \ \ \ \ \ \ \ \ \ Merge PR#638: Fix bug #5360: anomalies in typeclass resolution outputGravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#723: [travis] [fiat] Test also fiat-core.Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ 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
| | | | | | | | | | | | | | | | * | Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
| | | | | | | | | * | | | | | | | A few typos.Gravatar Hugo Herbelin2017-06-04
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | 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
| |_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | Add an overlay for coq-dpdgraph for 8.7Gravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | Make coq-dpdgraph allow-failGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | Add coq-dpdgraph CIGravatar Jason Gross2017-06-02
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |
| | | | | | * | | | | | | | | Use Names.Constant.printGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#discussion_r119963405
| | | | | | * | | | | | | | | 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | | | | 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#705: Fix bug #5019 (looping zify on dependent types)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] [fiat] Test also fiat-core.Gravatar Emilio Jesus Gallego Arias2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
| | | | | * | | | | | | | | | | | | | | | [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
| | | | | | | | | |_|/ / / / / / / / / / | | | | | | | | |/| | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | mention 'make world' without 'byte' in CHANGES + 2 minor suggestionsGravatar Pierre Letouzey2017-06-01
| | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | drop vo.itarget files and compute the corresponding the corresponding values ↵Gravatar Matej Kosik2017-06-01
| | |/ / / / / / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | automatically instead
| | | | | | | | | | | | | | | | | * | test-suite/coq-makefile: we do not build byte file by default anymoreGravatar Pierre Letouzey2017-06-01
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | * \ \ \ Merge PR#631: Fix bug #5255Gravatar 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
| | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 14:43:21 +0000