aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* | [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.
| * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |
* | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ | | | | | | | | | more uniform
* \ \ Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \ \
| | * | Relying on computation done in Envars to discover the installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | This allows to share the test for possible relocalisation done in envars.ml.
| | * | Generalizing to docdir and datadir the test for a relocated installation.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also standardizing the choice of the default datadir (I don't see why we should add by default both /usr/local/share/coq and /usr/share/coq when we know that the installation is in only one of them). Open question: test for possible relocation of the installed coq should be done on raw dirname of the executable or on the standardization of this name wrt symbolic links?
| | * | Exporting the suffixes needed to build coqlib, docdir, etc.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given.
| | * | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | This goes towards an approach where a local layout can be seen as an installed layout.
| | * | Configuration: always giving a value to configdir and datadir.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
| | * | Dead code (xdg_config_dirs).Gravatar Hugo Herbelin2017-05-29
| | | |
| * | | Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| |/ / | | | | | | | | | | | | | | | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* / / [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ / | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ \ | | | | | | | | | resolution trace
* \ \ Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\ \ \
* \ \ \ Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \
* | | | | | [location] Renaming "CAst.ast" to "CAst.t"Gravatar Matej Košík2017-05-24
| | | | | |
* | | | | | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \ \ \
| | * | | | | coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | ocamlfind: coqtop -config prints ocamlfind as found by ./configureGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it.
| | * | | | | print_config: print COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile
| | * | | | | Put the list of Coq sources subdirectories in one placeGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | and avoid duplication
| | * | | | | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | CoqProject_file: document in API deprecated featuresGravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | CoqProject_file: API and code cleanup (tuples -> records)Gravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
| |/ / / / / | | | | | | | | | | | | | | | | | | The .mli only acknowledges the current API. I'm not guilty your honor!
| | | | * / Bigint.euclid: clarify which sign convention is usedGravatar Pierre Letouzey2017-05-23
| | |_|/ / | |/| | |
| | | * | Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
| | | | |
| | * | | [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | We allow for a dynamic setting of the STM debug flag, and we print some more information about the result of `process_transaction`. We also fix a printing bug due to mixing `Printf` and `Format`, which are not compatible.
| * | | Documenting Option.List.find.Gravatar Hugo Herbelin2017-05-05
| | | |
| * | | Cosmetic: unifying style within option.ml.Gravatar Hugo Herbelin2017-05-05
| | | |
| * | | Upgrading some local function as a general-purpose combinator Option.List.map.Gravatar Hugo Herbelin2017-05-05
| |/ /
| * | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
| | |
* | | [location] Cleanup.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | We remove some unnecessary functions introduced before in the patch series + unused functions.
* | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes.
* | | [location] Document changes.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | |
* | | [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it.
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | Now it is a private field, locations are optional.
* | | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
| | |
* | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
* | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location.
* | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created.
* | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| | | | | | | | | | | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* | [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | Mostly documentation and making a couple of local flags, local.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:12:15 +0000