| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-02 | Univs: test-suite file for #4301, subtyping of poly parameters | Matthieu Sozeau | |
| 2015-10-02 | Univs: uncovered bug in strengthening of opaque polymorphic definitions. | Matthieu Sozeau | |
| 2015-10-02 | Fix test-suite file for bug #3777 | Matthieu Sozeau | |
| 2015-10-02 | Fix test-suite file: failing earlier as expected. | Matthieu Sozeau | |
| 2015-10-02 | Fix test-suite file | Matthieu Sozeau | |
| 2015-10-02 | Univs: correcly compute the levels of records when they fall in Prop. | Matthieu Sozeau | |
| 2015-10-02 | Univs/program: handle side effects in obligations. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix Show Universes. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix handling of side effects/delayed proofs | Matthieu Sozeau | |
| - When there are side effects which might enrich the initial universes of a proof, keep the initial and refined universe contexts apart like for delayed proofs, ensuring universes are declared before they are used in the right order. - Fix undefined levels in proof statements so that they can't be lowered to Set by a subsequent, delayed proof. | |||
| 2015-10-02 | Univs: handle side-effects of futures correctly in kernel. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix environment handling in scheme building. | Matthieu Sozeau | |
| 2015-10-02 | discriminate: Do fresh_global in the right env in presence of side-effects. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fixed bug 2584, correct universe found for mutual inductive. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix Universe vernacular, fix bug #4287. | Matthieu Sozeau | |
| No universe can be set lower than Prop anymore (or Set). | |||
| 2015-10-02 | Univs: fix after rebase (from_ctx/from_env) | Matthieu Sozeau | |
| 2015-10-02 | Univs: fixed bug #4328. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | |
| 2015-10-02 | Univs (pretyping): allow parsing and decl of Top.n | Matthieu Sozeau | |
| This allows pretyping and detyping to be inverses regarding universes, and makes Function's detyping/pretyping manipulations bearable in presence of global universes that must be declared (otherwise an evd would need to be threaded there in many places as well). | |||
| 2015-10-02 | Univs (evd): deal with global universes and sideff | Matthieu Sozeau | |
| - Fix union of universe contexts to keep declarations - Fix side-effect handling to register new global universes in the graph. | |||
| 2015-10-02 | Univs: fix evar_map initialization in newring. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix evar_map leaks bugs in Function | Matthieu Sozeau | |
| The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors. | |||
| 2015-10-02 | Univs: fix an evar leak in congruence | Matthieu Sozeau | |
| 2015-10-02 | Univs: minimization, adapt to graph invariants. | Matthieu Sozeau | |
| We are forced to declare universes that are global and appear in the local constraints as we start from an empty universe graph. | |||
| 2015-10-02 | Univs (kernel) adapt to new invariants | Matthieu Sozeau | |
| Remove predicative flag and adapt to new invariant where every universe must be declared, ensuring it is >= Set, safe_repr is not necessary anymore. | |||
| 2015-10-02 | Univs: module constraints move to universe contexts as they might | Matthieu Sozeau | |
| declare new universes (e.g. with). | |||
| 2015-10-02 | Remove Print Universe directive. | Matthieu Sozeau | |
| 2015-10-02 | Univs: More info for developers. | Matthieu Sozeau | |
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau | |
| 2015-10-02 | Univs: force all universes to be >= Set. | Matthieu Sozeau | |
| 2015-10-02 | Univs: Fix part of bug #4161 | Matthieu Sozeau | |
| Rechecking applications built by evarconv's imitation. | |||
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau | |
| 2015-10-02 | Changed status of Info messages from notice to info. | Pierre Courtieu | |
| This fixes a bug in proofgeneral. PG will now diplay this message eagerly. Otherwise since they appear before the goal, they are considered outdated and not displayed. | |||
| 2015-10-02 | emacs output mode: Added <infomsg> tag to debug messages. | Pierre Courtieu | |
| So that they display in response buffer. | |||
| 2015-09-30 | Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013). | Hugo Herbelin | |
| Incidentally made writing style in CoqIDE chapter more homogeneous. | |||
| 2015-09-30 | Build the compatibility files. | Guillaume Melquiond | |
| 2015-09-30 | Add compatibility files (feature 4319) | Jason Gross | |
| 2015-09-30 | Unexport Loadpath.get_paths. | Guillaume Melquiond | |
| 2015-09-29 | Fix dumb typo. | Guillaume Melquiond | |
| 2015-09-29 | Make the interface of System.raw_extern_intern much saner. | Guillaume Melquiond | |
| 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. | |||
| 2015-09-29 | Prevent States.intern_state and System.extern_intern from looking up files ↵ | Guillaume Melquiond | |
| 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. | |||
| 2015-09-29 | Remove some uses of Loadpath.get_paths. | Guillaume Melquiond | |
| 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. | |||
| 2015-09-28 | Make -load-vernac-object respect the loadpath. | Guillaume Melquiond | |
| 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. | |||
| 2015-09-27 | Fixing loss of extra data in Evd. | Pierre-Marie Pédrot | |
| 2015-09-26 | Documenting how to support some special unicode characters in coqdoc | Hugo Herbelin | |
| (thanks to coq-club, Sep 2015). | |||
| 2015-09-26 | Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015. | Hugo Herbelin | |
| 2015-09-26 | Test for bug #4347. | Pierre-Marie Pédrot | |
| 2015-09-26 | Fixing bug #4347: Not_found Exception with some Records. | Pierre-Marie Pédrot | |
| A term was reduced in an improper environment. | |||
| 2015-09-25 | The -require option now accepts a logical path instead of a physical one. | Pierre-Marie Pédrot | |
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | |
| 2015-09-25 | The -compile option now accepts ".v" files and outputs a warning otherwise. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |