aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/command.ml
Commit message (Collapse)AuthorAge
...
* | | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| * | | 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.
| | | * More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We want to avoid capture in "Inductive I {A} := C : forall A, I". But in "Record I {A} := { C : forall A, A }.", non recursivity ensures that no clash will occur. This fixes previous commit, with which it could possibly be merged.
| | | * Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| | |/ | |/| | | | | | | | | | | | | For instance, the following was failing to use the implicitness of n: Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
* / | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/ / | | | | | | | | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
| * Command.ml cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [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.
* | [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ | | | | | | | | | | | We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\
| * \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
| |\ \ | | | | | | | | | | | | let-ins
| | | * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |/ | |/|
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| | |
* | | [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] 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] 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.
| * | Removing tactic compatibility layer in Command.Gravatar Pierre-Marie Pédrot2017-04-24
|/ /
* | [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.
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
| |
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ | | | | | | | | | record fields.
| | * 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
| | |
* | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \ \ | | |/ | |/|
| * | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\ \
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| | |
* | | | 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 branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| | | |
| * | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
| * | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | RawLocal -> CLocal
| * | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | This is a bit long, but it is to keep a symmetry with constr_expr.
| * | | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ / /
| | * Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |/ |/| | | | | | | | | | | | | | | | | | | | | Deprecating abstract_constr_expr in favor of mkCLambdaN, prod_constr_expr in favor of mkCProdN. Note: They did not do exactly the same, the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type, what I think is the correct thing to do. So, there is also a "fix" of semantic here.
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/ | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
* [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
| | | | It was always set to `greedy:true`.
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 17:25:14 +0000