aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
| | | | | | | | | | 8a8caba3). - Adding cLexer.current_file to the lexer state, i.e. making it a component of the type "coq_parsable" of lexer state (it was forgotten in b8ae2de5 and 8a8caba3). - Inlining save_translator/restore_translator which have now lost most of their substance.
* Adding debugging printer for Genarg.ArgT.t.Gravatar Hugo Herbelin2016-10-08
|
* A fix to dev/include.Gravatar Hugo Herbelin2016-08-17
|
* Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
* | Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).Gravatar Hugo Herbelin2016-07-19
| |
* | FIX: "dev/doc/changes.txt"Gravatar Matej Kosik2016-07-05
| |
| * Add a renaming of Tacexpr.TacDynamicGravatar Jason Gross2016-07-04
|/
* Mention recent renaming of files in dev/doc/changes.txt.Gravatar Maxime Dénès2016-07-03
|
* rename toplevel/cerror.ml into explainErr.ml (too close to the new ↵Gravatar Pierre Letouzey2016-07-03
| | | | lib/cErrors.ml)
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
|
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* [doc] Update changes for feedback.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | I've included some other changes that didn't happen in this PR.
* [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | | This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished.
* remove an old workaround for OCaml 3.11 + MacOS natdynlinkGravatar Pierre Letouzey2016-06-24
|
* Makefile: compat5* moved in grammar/, less -I given to camlp4oGravatar Pierre Letouzey2016-06-21
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\
* | Documenting API changes in dev/doc/changes.txt.Gravatar Pierre-Marie Pédrot2016-06-09
| |
* | Merge PR #197.Gravatar Pierre-Marie Pédrot2016-06-09
|\ \
* | | Adding profiling developer information in dev/doc/profiling.txt.Gravatar Pierre-Marie Pédrot2016-06-08
| | |
| * | Add an explicit replacement rule for Refine moduleGravatar Jason Gross2016-06-08
|/ /
* | Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment.
* | proofs/proofs.mllib: no more proof_errors !Gravatar Pierre Letouzey2016-06-08
| |
| * Add license text to the windows installationGravatar Enrico Tassi2016-06-03
| |
* | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\|
* | Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\ \
| * | Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy)
| * | Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | | | | | | | | | | Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility.
| | * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
| | | | | | | | | | | | This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| * Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| | | | | | | | | | | | | | Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible.
* | Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | A note concerning the "Drop" command.Gravatar Matej Kosik2016-05-03
| |
* | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug.Gravatar Matej Kosik2016-05-03
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\|
* | Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
| | | | | | | | | | | | | | This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all.
| * Use -win32 and -win64 suffixes for installer name on Windows.Gravatar Maxime Dénès2016-04-07
| |
* | Merge remote-tracking branch 'origin/pr/78' into trunk:Gravatar Maxime Dénès2016-04-04
|\ \ | | | | | | | | | | | | An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output.
* | | Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
| | |
* | | Moving Tacenv to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| | |
* | | Moving Tactic_debug to Hightactic.Gravatar Pierre-Marie Pédrot2016-03-20
| | |
* | | Documenting changes.Gravatar Pierre-Marie Pédrot2016-03-20
| | |
* | | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
| | |
* | | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
| | | | | | | | | | | | | | | Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.