aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.mli
Commit message (Collapse)AuthorAge
* Update evarutil.mliGravatar Matthieu Sozeau2018-06-05
| | | Actually all the new_ functions are in evarutil still
* Fix wrong deprecation msgGravatar Matthieu Sozeau2018-06-05
|
* [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
|
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
|
* Use evd_combX in Cases.Gravatar Gaëtan Gilbert2018-05-14
|
* Convert clear_hyps_in_evi to state passing style.Gravatar Gaëtan Gilbert2018-05-11
|
* Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
| | | | clear_hyps remain with no alternative
* [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 #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\
* \ Merge PR #6866: Slight improvement of messages related to direct and ↵Gravatar Pierre-Marie Pédrot2018-04-25
|\ \ | | | | | | | | | indirect uses of tactic `clear`.
| * | Improving error message for clear tactic (and indirect uses of it).Gravatar Hugo Herbelin2018-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Be more precise when trying to clear an hypothesis which occurs implicitly in a global constant. - Warns if destruct/induction cannot clear an hypothesis occurring implicitly in a global. In the first case, the change in situation Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a. is: - before: "a is used in conclusion" - after: "a is used implicitly in b in conclusion" In the second case: Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a. produces a warning: "Cannot remove a, it is used implicitly in b".
* | | Adding a flag to support different naming modes for evar hypotheses.Gravatar Hugo Herbelin2018-04-24
|/ / | | | | | | | | | | | | | | | | | | Four modes currently supported to deal with clashes: 1. Failing in case of clash 2. Renaming the most recent one 3. Renaming the previous hypothesis of same name if not a section variable 4. Renaming the previous hypothesis of same name even if a section variable The current mode is 3. Keeping it active by default
| * Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
|/ | | | Normalization sounds like it should be semantically noop.
* 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.
* Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
| | | | For instance, error in "Goal forall a f, f a = 0" is now located.
* Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
| | | | | | | We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
* Merge PR #6222: Share computation of unifiable evarsGravatar Maxime Dénès2017-12-22
|\
* | [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | | | We need to a partial restore. I think that we could design a better API, but further work on the toplevel state should improve it progressively.
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
* | [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | Note the problem with `create_evar_defs`.
| * Experimenting with a fine-grained cache for undefined evars in evinfos.Gravatar Pierre-Marie Pédrot2017-11-21
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| | | | This is a first step towards some of the solutions proposed in #6008.
* Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
| | | | | | | | | | | In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further.
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Adding intermediate entry point to create an evar in empty rel_context.Gravatar Hugo Herbelin2017-06-25
|/
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
* [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.
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
|
* 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
|
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Refine 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
|
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
|
* Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
| | | | This saves a quadratic allocation by replacing arrays with maps.