aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
Commit message (Collapse)AuthorAge
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
| | | | | any length with a [None] representation and ensure that this representation is canonical through the restricted interface.
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
| | | Adds a combinator List.map_right which chains effects from right to left.
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
|
* Useless instantiation function exported in Evd.Gravatar Pierre-Marie Pédrot2013-11-30
|
* Removing Evd.undefined_evars.Gravatar ppedrot2013-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless filter allocation in evar construction.Gravatar ppedrot2013-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless array-to-list and converse casts used inGravatar ppedrot2013-10-22
| | | | | | Evar{conv,solve} files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless evar code.Gravatar ppedrot2013-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing dubious use of evarmap manipulating functions in printingGravatar ppedrot2013-10-05
| | | | | | related code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
| | | | | | | | | | | | | | | | | | | state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless evar-related stuff.Gravatar ppedrot2013-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
| | | | | | | | | | | | casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing some evar_maps manipulation. In particular, using a [map] insteadGravatar ppedrot2013-09-05
| | | | | | of a [fold] in [nf_*] normalizing functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of Evd.Gravatar ppedrot2013-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partly replacing list-based access functions in Evd. This is stillGravatar ppedrot2013-09-03
| | | | | | | unsatisfactory as some functions implicitly require some ordering on the evars, but this is already better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
| | | | | | | | | | The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing now useless merging primitives from Evd.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16658 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleaning of Evd interface.Gravatar ppedrot2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a redundant function from Evd.Gravatar ppedrot2013-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
| | | | | | functor application. Rewritten the interface btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7
* Locating errors from consider_remaining_unif_problems if possibleGravatar herbelin2013-02-17
| | | | | | | (useful when consider_remaining_unif_problems not called via pretyping.ml, as e.g. from command.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envGravatar herbelin2013-01-29
| | | | | | for better uniformity of naming policy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of nameGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a comment: precondition on Evd.addGravatar aspiwack2012-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
| | | | | | | | | | | | known in advance to be instantiable by only a finite number of terms. When an evar with candidates remain unsolved after unification, the first candidate is taken as a heuristic. This is used in particular to reduce the number of pending conversion problems when trying to infer the return clause of a pattern-matching problem. As an example, this repairs test 2615.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r14585 (ill-typed restriction bug).Gravatar herbelin2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
| | | | | | | | | particular, new printer for evar_map which displays undefined evars + defined evars that were instantiated by these undefined evars and recursively, up to some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better procedure for checking presence of undefined evars.Gravatar aspiwack2011-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
| | | | | | | | | | "apply" unification. Assuming w_unify_0 is not eventually abandoned, it remains to merge unify_with_eta into unify_0 (what unify_with_eta does and that unify_0 does not do is to select of two instances of the same meta the one with less lambda's; it is unclear whether this is useful heuristic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
| | | | | | | | | | | | | evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
| | | | | | | - Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
| | | | | | | in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc improvements about evar_mapGravatar letouzey2010-12-15
| | | | | | | | | | | | - A Evd.defined_evars to keep only this part of the evar_map - One Evd.fold less in Typeclasses.mark_unresolvables - We check that only undefined evar_map could be set unresolvable - A duplicated function in himsg.ml TODO: some calls to Evd.fold(_undefined) would be faster if written as Map.map or Map.mapi. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
| | | | | | | | | | | | | evar_map into a map for defined evars and a map for undefined evars. Even before Spiwack's new proof engine, some Evd.fold were very costly, e.g. in check_evars or progress_evar_map. With the new proof engine, undefined evars traversals are apparently even more common (at least, it improves significantly the complexity of some calls to omega in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained by removal of evar_merge in clenv_fchain in commit 13007, arriving to figures comparable to the 8.3 ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 02:44:08 +0000