aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
Commit message (Collapse)AuthorAge
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| | | | | | | | | | | | | | | | | | | The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
* Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\
* \ Merge PR #946: Functional pretyping interfaceGravatar Maxime Dénès2017-08-29
|\ \
* | | A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
| | * Adapting code to renaming Option.fold_map -> Option.fold_left_map.Gravatar Hugo Herbelin2017-08-29
| | |
| | * Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| |/ |/| | | | | (from module List).
* | Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \
| | * Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
| |/ |/|
* | Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Maxime Dénès2017-08-01
|\ \
* | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | |
| * | Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2017-07-26
|/ / | | | | | | This fixes bug 5650: evar (x : Prop) should not be slow.
* | [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
* | Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \
* | | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
| | |
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | |
| | * Preparing to hints supporting discharge.Gravatar Hugo Herbelin2017-06-27
| |/ |/| | | | | | | I.e., do not set local flag to false when in a section since compatibility tells discharge of hints is not supported.
* | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \
* \ \ Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \
| | * | plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
* | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \ \
* \ \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
| | | | * | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
| | | * | | Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | | | |
| | | * | | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | |/ /
* | | / / Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| |_|/ / |/| | |
| | | * [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file.
* | | | Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \ \ \ | |_|_|/ |/| | |
| | | * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`.
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | |
| * | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/ /
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/ | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* 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#600: Some factorizations of ltac interpretation functions between ↵Gravatar Maxime Dénès2017-06-06
|\ | | | | | | ssreflect and coq code
* \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \
* \ \ 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
| | | * | 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#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \
* \ \ \ \ Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \ \ \
| | | | * | [printing] Remove duplicated printing function.Gravatar Emilio Jesus Gallego Arias2017-06-01
| |_|_|/ / |/| | | | | | | | | | | | | | It seems there were 4 copies of the same function in the code base.
| | | * | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar.
| | | | * Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure.
| | | | * Splitting interp_open_constr into two variants, with or without type classes.Gravatar Hugo Herbelin2017-05-31
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | This simplifies the API as before, inference of instances of type classes was iff a type constraint was given. We then export these both versions of interp_open_constr.
| * | / 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.
* | | 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).
* | | Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | evars. This is for consistency with the rest of the language. For instance, "eremember" and "epose" are supposed to refer to terms occurring in the goal, hence not leaving evars, hence in general pointless. Eventually, I guess that "e" should be a modifier (see e.g. the discussion at #3872), or the difference is removed.
* | | Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
|/ / | | | | | | a goal with unresolved evars.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 14:11:29 +0000