aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
* Merge PR#627: Obligations shrinking: shrink abstraction tooGravatar Maxime Dénès2017-05-20
|\
* \ Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| | |
* | | Uniformity of style for selecting plural or not; spacing for comma.Gravatar Hugo Herbelin2017-05-13
| | |
| | * Obligations shrinking: shrink abstraction tooGravatar Matthieu Sozeau2017-05-11
| |/ |/|
| * Adapted to EConstr.Gravatar Pierre Courtieu2017-05-05
| |
| * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
| | | | | | | | | | | | | | | | | | | | | | We want to print variables in vertical boxes as much as possible. The criterion to distinguish "variable" from "hypothesis" is not obvious. We chose this one but may change it in the future: X:T is a variable if T is not of type Prop AND T is "simple" which means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall Ti:Type, but not Ti:nat).
* | Fix two new unused opens.Gravatar Maxime Dénès2017-05-02
|/
* Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\
* | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| |
* | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
|\ \ | | | | | | | | | let-ins
| | * Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
| | |
| | * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | |
| | * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
| | * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |/ |/|
* | Merge PR#583: [toplevel] More work on error handling.Gravatar Maxime Dénès2017-04-27
|\ \
| * | [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a partial backtrack on 63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we disregarded exception and tried to print error messages just by listening to feedback. However, feedback error messages are not always emitted due to https://coq.inria.fr/bugs/show_bug.cgi?id=5479 Thus meanwhile it is safer to go back to printing the information present in exceptions until we tweak the STM. This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many other glitches not reported, such errors in nested proofs.
* | | Removing tactic compatibility layer in Command.Gravatar Pierre-Marie Pédrot2017-04-24
|/ /
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
* \ \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \ \
* | | | [toplevel] [emacs] Don't quote errors in emacs mode.Gravatar Emilio Jesus Gallego Arias2017-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. We also update the warnings quoter to use a warning tag instead of a non-printable char. This fixes ProofGeneral for trunk users. c.f. https://github.com/ProofGeneral/PG/issues/175
| * | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
|/ / /
| * | [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.
* | | [toplevel] Fix #5475Gravatar Emilio Jesus Gallego Arias2017-04-18
|/ / | | | | | | | | This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e, `Notice`-level messages should not be wrapped in `<infomsg>` tags.
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
| |
* | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \
| * | [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | Mostly documentation and making a couple of local flags, local.
| * | [vernac] vernacentries.mli cleanupGravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | This header file had accumulated quite a bit of cruft over the years, we clean it up while we are at it. No functional change as all the removed variables/methods were noops long time ago.
| * | [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled.
* | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ \ | | | | | | | | | | | | record fields.
* \ \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ \ | |_|/ / |/| | |
| | | * Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
| | | * Fixing several wrong computations of implicit arguments by positionGravatar Hugo Herbelin2017-04-09
| | | | | | | | | | | | | | | | in the presence of let-ins.
| | | * Minor cosmetic commit.Gravatar Hugo Herbelin2017-04-09
| | | |
| | | * Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
| |_|/ |/| | | | | | | | | | | There were actually no syntax for it, and I'm still unsure what good syntax to give to it, even more that it would be useful to have one.
| * | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \
* | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| | | | | | | | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* | | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ↵Gravatar Maxime Dénès2017-04-07
|\ \ \ | | | | | | | | | | | | printer.
* \ \ \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \
| | * | | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
* | | | Merge PR#502: [pp] Add anomaly header to error messages.Gravatar Maxime Dénès2017-04-04
|\ \ \ \
| | | * \ Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| | | |\ \ | |_|_|/ / |/| | | |
* | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-03
| | | | |
* | | | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \ \ \ \
| | | | * | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
| | | | * | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For now we only normalize sorts, and we leave instances for the next commit.
* | | | | | Merge PR#511: [stm] Remove some obsolete vernacs/classification.Gravatar Maxime Dénès2017-03-30
|\ \ \ \ \ \
| | | | | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| | | | | | |
| * | | | | | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | |_|_|/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away.
* / | | | | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
|/ / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:41:08 +0000