aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Fixes #7811 (uncaught Not_found in notation printer related to "match").Gravatar Hugo Herbelin2018-06-17
|
* Fix deprecation warning introduced by PR 664 mergeGravatar Matthieu Sozeau2018-06-14
|
* Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Gravatar Matthieu Sozeau2018-06-14
|\ | | | | | | to anomaly)
* \ Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ | | | | | | | | | in unification
* \ \ Merge PR #7105: Getting rid of some false "collision between bound variable ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ | | | | | | | | | | | | names" warnings
* | | | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | We move the last 3 types to more adequate places.
* | | | [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | | | | | We move the "flag types" to its use place, and mark some arguments with named parameters better.
* | | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | | | | | - move_location to proofs/logic. - intro_pattern_naming to Namegen.
* | | | [api] Misctypes removal: remove dummy alias.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | |
* | | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | |
| | * | Fixes #7780 (missing lift in expanding alias under a binder in unification).Gravatar Hugo Herbelin2018-06-12
| |/ / |/| |
* | | Merge PR #7679: Clean native compilation of primitive projectionsGravatar Maxime Dénès2018-06-05
|\ \ \
* \ \ \ Merge PR #7004: Make `simple apply` obey `Opaque` directive.Gravatar Pierre-Marie Pédrot2018-06-05
|\ \ \ \
* \ \ \ \ Merge PR #7077: Preserving canonical structure of return predicate in ↵Gravatar Maxime Dénès2018-06-05
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | vm_compute and native_compute (partial fix to #7068; also fixes #7076))
| | | * | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
* | | | | Merge PR #7099: Stronger invariants in unification signature.Gravatar Matthieu Sozeau2018-06-05
|\ \ \ \ \
| | | * | | Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
| | * | | Preserving "canonical" form of return predicate in native_compute.Gravatar Hugo Herbelin2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that the normalization of the context of the return predicate was not done by the native compilation but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval native_compute in fun x => match x in A y z return y = z with end.
| | * | | Preserving "canonical" form of return predicate in vm_compute.Gravatar Hugo Herbelin2018-06-04
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that the normalization of the context of the return predicate was not done by the vm but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval vm_compute in fun x => match x in A y z return y = z with end.
* | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ | | | | | | | | | | | | | | | pattern-matching names
* \ \ \ \ Merge PR #7189: Fix #5539: algebraic universe produced by cases.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \
| | | * | | Stronger invariants in unification signature.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use an option type instead of returning a pair with a boolean. Indeed, the boolean being true was always indicating that the returned value was unchanged. The previous API was somewhat error-prone, and I don't understand why it was designed this way in the first place.
* | | | | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | tactic unification.
* \ \ \ \ \ Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ 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
| | * | | | | | | Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Pierre-Marie Pédrot2018-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal.
| * | | | | | | | 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
|\ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 07:35:32 +0000