aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2017-12-11Merge PR #6338: Remove up-to-conversion term matchingMaxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
2017-12-09Remove up-to-conversion matching functions.Pierre-Marie Pédrot
They were not used anymore since the previous patches.
2017-12-06Getting rid of the Update constructor in Reductionops.Pierre-Marie Pédrot
This was dead code, probably due to the fact it was once shared with the kernel stack type.
2017-12-06Getting rid of the Shift constructor in Reductionops.Pierre-Marie Pédrot
It was actually not used. The only place generating one was easily writable without it.
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607].
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Maxime Dénès
#3125)
2017-11-30Remove unused boolean from cl_context field of Typeclasses.typeclassGaëtan Gilbert
2017-11-28Adding a variant get_truncation_family_of of get_sort_family_of.Hugo Herbelin
This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type.
2017-11-28Moving non-recursive function sort_family_of out of the retype block of ↵Hugo Herbelin
recursive functions.
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
There don't really bring anything, we also correct some minor nits with the printing function.
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
Also nicer error when the constraints are impossible.
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
Before sometimes there were lists and strings.
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Maxime Dénès
constructs.
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
2017-11-22[api] A few more minor deprecation notices.Emilio Jesus Gallego Arias
Note the problem with `create_evar_defs`.
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Maxime Dénès
unbound rel
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaëtan Gilbert
When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case.
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6117: Fix printing anomaly in convMaxime Dénès
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-08Fixing missing separator in an error message.Hugo Herbelin
The message is the "Conversion test raised an anomaly" one.
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
We do up to `Term` which is the main bulk of the changes.
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
This will allow to merge back `Names` with `API.Names`
2017-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin
We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
This is a first step towards some of the solutions proposed in #6008.
2017-11-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵Maxime Dénès
variables).
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵Maxime Dénès
alphabet
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
This fixes also #5731, #6035, #5364.
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
To this extent we factor out the relevant bits to a new file, ltac_pretype.
2017-10-17unification: fix BZ#5692, recognize prim projs as CS projectionsMatthieu Sozeau
2017-10-17Properly handling projection parameters in canonical structures.Pierre-Marie Pédrot
2017-10-17Handling primitive projections in canonical structures.Pierre-Marie Pédrot
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ↵Maxime Dénès
?INTERNAL#42 style is ugly
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-09-28Remove trivial TODO comment (constants can't be template poly now).Gaëtan Gilbert
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Maxime Dénès
let-ins and non-recursively uniform parameters
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Maxime Dénès
4e70791).
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 02:17:47 +0000