aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | | (Universes and Evd)
* Coq_omega: remove unused Goal.entersGravatar Gaëtan Gilbert2018-07-03
| | | | Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
* Remove unused function Coq_omega.timing.Gravatar Gaëtan Gilbert2018-07-03
|
* Taccoerce: remove various unused arguments.Gravatar Gaëtan Gilbert2018-07-03
|
* Pptactic: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
|
* Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\
* \ Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \ | | | | | | | | | points of Camlp5
| | * Implement uniform parameters in ComInductiveGravatar Jasper Hugunin2018-07-01
| |/ |/| | | | | Don't allow notations attached to uniform inductives
* | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | Z into three files
* | | Split the Ssrmatching module between code and grammar rules.Gravatar Pierre-Marie Pédrot2018-06-30
| | | | | | | | | | | | Fixes #7857.
| | * Port g_tactic to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | |
| | * Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| |/ |/| | | | | | | | | | | | | | | The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
| * Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
| |
* | Merge PR #7890: Inline a function from Quote used in setoid_ring.Gravatar Maxime Dénès2018-06-29
|\ \ | |/ |/|
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
* \ \ Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \ | | | | | | | | | | | | constants
| | * | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |/ / |/| |
| * | universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
| | | | | | | | | | | | | | | Apparently it was not useful. I don't remember what I was thinking when I added it.
* | | Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorGravatar Maxime Dénès2018-06-25
|\ \ \
* \ \ \ Merge PR #7236: [ssr] simpler semantics for delayed clearsGravatar Maxime Dénès2018-06-23
|\ \ \ \
* | | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
* | | | | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | | | | | | | | | | This is a first step towards the acceptance of mutual record types in the kernel.
| * | | | [ssr] implement {}/v as a short hand for {v}/v when v is an idGravatar Enrico Tassi2018-06-22
| | | | |
| * | | | [ssr] simplify delayed clearsGravatar Enrico Tassi2018-06-22
| | |/ / | |/| | | | | | | | | | | | | | - we always rename - we compile {clear}/view to /view{clear}
* | | | [ssr] matching: use eq_constr_nounivs in approximated matchingGravatar Enrico Tassi2018-06-22
| | | |
* | | | [ssr] set: merge universe constraints before type checking the termGravatar Enrico Tassi2018-06-22
|/ / /
| | * Further cleanup: do not export the closed_term Ltac entry.Gravatar Pierre-Marie Pédrot2018-06-21
| | | | | | | | | | | | | | | We only use it locally, so we simply register the ML tactic inside the module but we do not export the syntax.
| | * Inline a function from Quote used in setoid_ring.Gravatar Pierre-Marie Pédrot2018-06-21
| |/ |/| | | | | | | | | The code was wrong as it relies once again on term equality and fails on polymorphic constants. Quote is bound to disappear, so we write a correct version of this 10-line function in setoid_ring.
| * [ssr] rewrite: turn anomaly into regular errorGravatar Enrico Tassi2018-06-20
|/ | | | | | | | | I think the bug was introduces when apply_type was made safe. In the test joint to #7255 rewrite (setoid case) generates an ill-typed goal and apply_type raises a Pretype_error. It is unclear to me why the tactic monad does not turn the pretype_error into a UserError
* Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\
* \ Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Gravatar Pierre-Marie Pédrot2018-06-19
|\ \
| * | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| | | | | | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
| | * Remove reference name type.Gravatar Maxime Dénès2018-06-18
| |/ | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute.
* | Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/ | | | | | This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless.
* Workaround to handle non-value arguments in tactics.Gravatar Cyprien Mangin2018-06-14
| | | | | Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | We move the last 3 types to more adequate places.
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | This gets `Tactypes` closer to `tactics/`, however some legacy stuff blocks it in `proofs`. We consider that is satisfactory for now.
* [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: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
|
* [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
|
* Micromega clean-upGravatar Maxime Dénès2018-06-07
| | | | | | | | | We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
* 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.
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
* \ Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Pierre-Marie Pédrot2018-06-04
|\ \
* \ \ Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \ \
| | | * Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|/ |/| |
* | | Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \
| | | * Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
| | | |
* | | | [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 07:59:05 +0000