aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Optimizing the universes_of_constr_function.Gravatar Pierre-Marie Pédrot2016-02-03
| | | | | Instead of relying on a costly set union, we take advantage of the fact that instances are small compared to the set of universes.
* Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
| | | | variables and definitions in sections is unsupported.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
|
* Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
| | | | | | The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps.
* Univs: fix bug #4443.Gravatar Matthieu Sozeau2015-12-03
| | | | | Do not substitute rigid variables during minimization, keeping their equality constraints instead.
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
* Avoid recording spurious Set <= Top.i constraints which are alwaysGravatar Matthieu Sozeau2015-11-27
| | | | valid (when Top.i is global and hence > Set).
* Univs: fix type_of_global_in_context not returning instantiated universe ↵Gravatar Matthieu Sozeau2015-11-20
| | | | contexts.
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
| | | | involving Futures.
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
| | | | | Keep user-side information on the names used in instances of universe polymorphic references and use them for printing.
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
| | | | | | | | | | | | | | | | | | | | | Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large.
* lib_stack: API to reorder the libstackGravatar Enrico Tassi2015-10-28
| | | | | | | For discharging it is important that constants occur in the libstack in an order that respects the dependencies among them. This is impossible to achieve for private constants when they are exported globally without this (ugly IMO) api.
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
| | | | structure.
* Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Gravatar Pierre Letouzey2015-10-25
| | | | | | | As shown by the code snippets in these bug reports, I've been too hasty in considering these situations as anomalies in commit 466c4cb (at least the one at the last line of consistency_checks). So let's turn these anomalies back to regular user errors, as they were before this commit.
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
| | | | Add a flag to disallow minimization to set
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
| | | | | These options can be set to a string value, but also unset. Internal data is of type string option.
* Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
| | | | | | | context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time.
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
| | | | | | According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions.
* Univs: fix minimization to allow lowering a universe to Set, not Prop.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
| | | | No universe can be set lower than Prop anymore (or Set).
* Univs: minimization, adapt to graph invariants.Gravatar Matthieu Sozeau2015-10-02
| | | | | We are forced to declare universes that are global and appear in the local constraints as we start from an empty universe graph.
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
|
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
|
* Unexport Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-30
|
* Fix dumb typo.Gravatar Guillaume Melquiond2015-09-29
|
* Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
| | | | | | There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures.
* Prevent States.intern_state and System.extern_intern from looking up files ↵Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner.
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | | | | | | | | | | | | The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files.
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
| | | | | | | | | | This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq.
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
|
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
|
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
| | | | with Enrico.
* Nametab: print debug notice only in debug mode.Gravatar Maxime Dénès2015-09-20
|
* Add an if_verbose for "Fetching opaque proofs ..."Gravatar mlasson2015-09-03
| | | | | I do not think that this information is worth displaying without the verbose flag.
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
| | | | | | | | Indeed, the name of a bound variable was lost when unifying under a Prod in evarconv. The error message for "Unable to satisfy the following constraints" is still to be improved though.
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| | | | | | | | | | in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk?
* Native compiler: refactor code handling pre-computed values.Gravatar Maxime Dénès2015-07-10
| | | | Fixes #4139 (Not_found exception with Require in modules).
* Improve semantics of -native-compiler flag.Gravatar Maxime Dénès2015-07-09
| | | | | | | | | | Since Guillaume's, launching coqtop without -native-compiler and call native_compute would mean recompiling silently all dependencies, even if they had been precompiled (e.g. the stdlib). The new semantics is that -native-compiler disables separate compilation of the current library, but still tries to load precompiled dependencies. If loading fails when the flag is on, coqtop stays silent.
* Univs/minimization: Fix unused variable bug.Gravatar Matthieu Sozeau2015-07-07
|
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
| | | | | | | | | | | | | | | | | | | | | | | | When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w | case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
| | | | | | | | | | | | | | | 1) We now _assign_ the smallest possible arities to mutual inductive types and eventually add leq constraints on the user given arities. Remove useless limitation on instantiating algebraic universe variables with their least upper bound if they have upper constraints as well. 2) Do not remove non-recursive variables when computing minimal levels of inductives. 3) Avoid modifying user-given arities if not necessary to compute the minimal level of an inductive. 4) We correctly solve the recursive equations taking into account the user-declared level.
* Wrapped the declare_object function to pretty-print anomalies at loading time.Gravatar Thomas Sibut-Pinote2015-06-25
|
* On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | | Marshalled libraries are only loaded when needed and dropped thereafter. This might be costly for Require inside modules, but such a practice is discouraged anyway.
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | The first part only contains the summary of the library, while the second one contains the effective content of it.
* Fix bug #3446.Gravatar Matthieu Sozeau2015-06-11
| | | | Wrong handling of algebraic universes that have upper bounds.
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
| | | | | | Some asynchronous constraints between initial universes and the ones at the end of a proof were forgotten. Also add a message to print universes indicating if all the constraints are processed already or not.
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
| | | | | | | | | | | | | | Note that this does not prevent using native_compute, but it will force on-the-fly recompilation of dependencies whenever it is used. Precompilation is enabled for the standard library, assuming native compilation was enabled at configuration time. If native compilation was disabled at configuration time, native_compute falls back to vm_compute. Failure to precompile is a hard error, since it is now explicitly required by the user.
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| | | | | | Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.