aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\
* | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \
| | * Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| | | | | | | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| |/ |/| | | | | | | | | Close #7562. [api] move hint_info ast to tactics.
| * [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
|/ | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
* Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\
| * Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | | | | | | | | | We now have only two notions of environments in the kernel: env and safe_env.
* | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/ | | | We address the easy ones, but they should probably be all removed.
* Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Gravatar Pierre-Marie Pédrot2018-05-24
|\ | | | | | | in CArray
| * Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| |
| * Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| |
| * Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
| |
| * Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| |
* | [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
| | | | | | | | | | | | There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more.
* | [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
|/ | | | | | | `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed.
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
* \ Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \
| | * Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
| | |
| | * Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| | |
| | * Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
| | | | | | | | | | | | This API is a bit strange, I expect it will change at some point.
| | * Stop using Universes.subst(_opt)_univs_constrGravatar Gaëtan Gilbert2018-05-17
| | | | | | | | | | | | | | | | | | | | | Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from?
| | * Make set minimization option internal to UniversesGravatar Gaëtan Gilbert2018-05-17
| |/ |/|
* | Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \
* \ \ Merge PR #7213: Do not compute constr matching context if not used.Gravatar Matthieu Sozeau2018-05-15
|\ \ \
| | * | Use evd_combX in Cases.Gravatar Gaëtan Gilbert2018-05-14
| | | |
| | * | Typing implementation doesn't use evdref.Gravatar Gaëtan Gilbert2018-05-14
| | | |
| | * | Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
| | | |
| | * | Typing: define functional alternatives to e_* functionsGravatar Gaëtan Gilbert2018-05-14
| | | |
| | * | set_solve_evars doesn't use an evar_map refGravatar Gaëtan Gilbert2018-05-11
| | | |
| | * | Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
| | | |
| | * | Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
| |/ / |/| | | | | | | | clear_hyps remain with no alternative
| | * [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | We move syntax for universes from `Misctypes` to `Glob_term`. There is basically no reason that this type is there instead of the proper file, as witnessed by the diff. Unfortunately the change is not compatible due to moving a type to a higher level in the hierarchy, but we expect few problems. This change plus the related PR (#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns.
* | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* | Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Pierre-Marie Pédrot2018-05-04
|\ \
* | | [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
* | | Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
* | | Merge PR #7358: Fix #7356: missing lift when interpreting default instances ↵Gravatar Enrico Tassi2018-04-27
|\ \ \ | | | | | | | | | | | | of evars
| * | | Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Gravatar Hugo Herbelin2018-04-26
| | | |
| | * | [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
| |/ / | | | | | | | | | | | | | | | `hint_info_expr`, `hint_info_gen` do conceptually belong to the typeclasses modules and should be able to be used without a dependency on the concrete vernacular syntax.
* / / Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This removes the Flags.univ_print in the kernel, making it possible to put the univ printing flag ownership back in Detyping. The lazyness is because getting an explanation may be costly and we may discard it without printing. See benches - with lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console - without lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console Notably without lazy mathcomp odd_order is +1.26% with some lines showing significant changes, eg PFsection11 line 874 goes from 11.76s to 13.23s (+12%). (with lazy the same development has -1% overall and the same line goes from 11.76s to 11.23s (-4%) which may be within noise range)
* | [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
* | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| | | | | | | | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* | Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵Gravatar Pierre-Marie Pédrot2018-04-13
|\ \ | | | | | | | | | contains evars
* \ \ Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\ \ \
| | | * Do not compute constr matching context if not used.Gravatar Pierre-Marie Pédrot2018-04-10
| |_|/ |/| | | | | | | | This mitigates bug #6860.
* | | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Gravatar Pierre-Marie Pédrot2018-04-01
|\ \ \
| | | * [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants.
| * | Supporting fix/cofix in Ltac pattern-matching (wish #7092).Gravatar Hugo Herbelin2018-03-28
| | | | | | | | | | | | | | | This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern.
| * | Patterns: Accepting patterns in PFix and PCofix and not only constr.Gravatar Hugo Herbelin2018-03-28
| | |