aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Collapse)AuthorAge
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \
| | * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| | * Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | |\ | | |/ | |/|
| | * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| | |
| * | Type@{_} should not produce a flexible algebraic universe.Gravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | Otherwise [(fun x => x) (Type : Type@{_})] becomes [(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})] breaking the invariant that terms do not contain algebraic universes (at the lambda abstraction).
| * | Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| |/ | | | | | | The addition to the test suite showcases the usage.
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| |
| * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| |
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | Now it is a private field, locations are optional.
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge PR#543: Sanitize instance interpretationGravatar Maxime Dénès2017-04-11
|\
* \ Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \
| * \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\ \
| | | * Factor interp_instance out of Pretyping.pretype_globalGravatar Gaetan Gilbert2017-04-06
| | | |
| | | * Avoid strange shadowing of Pretyping.interp_universe_level_nameGravatar Gaetan Gilbert2017-04-06
| | |/ | |/|
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| |
* | | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | | | | For now we only normalize sorts, and we leave instances for the next commit.
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
| | * Make the computation of frozen evars lazy in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | A lot of tactic calls actually use the open_constr_no_classes_flags option which does not require checking anything about frozen evars. Computing it upfront is useless in this case.
| | * Fast path in computation of frozen evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | Most of the time, undefined evars are not modified by the considered function, which leads to the costly recomputation of a trivial partition of evars. We simply take advantage of physical equality to discriminate when this is useless and special-case it in the type of frozen evars.
| | * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| |/ | | | | | | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | We make mli files look to what they were looking before the move to EConstr by opening this module.
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| |
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
| |
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Nativenorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 10:33:06 +0000