| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-05 | Removing redundant versions of generalize. | Hugo Herbelin | |
| 2015-12-05 | Moving three related small half-general half-ad-hoc utility functions | Hugo Herbelin | |
| next to each other, waiting for possible integration into a more uniform API. | |||
| 2015-12-04 | Getting rid of dynamic hacks in Setoid_newring. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the last use of tacticIn in setoid_ring. | Pierre-Marie Pédrot | |
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-19 | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau | |
| constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore. | |||
| 2015-11-18 | Fix a bug preventing the generation of graphs when doing multiple | Matthieu Sozeau | |
| pattern-matching on function calls. | |||
| 2015-11-07 | Preventing an unwanted warning 5 "this function application is partial" | Hugo Herbelin | |
| which e.g. OCaml 4.02.1 displays. | |||
| 2015-11-07 | Merge remote-tracking branch 'origin/v8.5' into upstream-trunk | Hugo Herbelin | |
| - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml | |||
| 2015-11-06 | Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan | Hugo Herbelin | |
| for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise. | |||
| 2015-10-29 | Monotonizing Tactics.change_arg. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing some goal unsafeness in inductive schemes. | Pierre-Marie Pédrot | |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-28 | Univs: local names handling. | Matthieu Sozeau | |
| Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. | |||
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi | |
| 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. | |||
| 2015-10-28 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau | |
| 2015-10-28 | Do not pause globing in funind. (Fix bug #4382) | Guillaume Melquiond | |
| Since the functions of this plugin exit by raising exceptions, globing was never restarted. This prevented coqdoc from generating a proper output whenever some feature of this plugin was used. There does not seem to be any parsing of dynamic expressions, so pausing globing does not make much sense in the first place. | |||
| 2015-10-20 | Proofview.Goal.sigma returns an indexed evarmap. | Pierre-Marie Pédrot | |
| 2015-10-20 | Indexing Proofview.goals with a stage. | Pierre-Marie Pédrot | |
| This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level. | |||
| 2015-10-20 | Boxing the Goal.enter primitive into a record type. | Pierre-Marie Pédrot | |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-19 | Type delayed_open_constr is now monotonic. | Pierre-Marie Pédrot | |
| 2015-10-19 | Function debug mode more formatted. | Pierre Courtieu | |
| 2015-10-19 | Partly fixes #3225. Removed some old experimental stuff in funind. | Pierre Courtieu | |
| 2015-10-18 | Constraining refine to monotonic functions. | Pierre-Marie Pédrot | |
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-14 | Exporting the original unprocessed hint in the hint running function. | Pierre-Marie Pédrot | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-08 | f_equal fix continued: do a refresh_universes as before. | Matthieu Sozeau | |
| 2015-10-07 | Fix bug #4069: f_equal regression. | Matthieu Sozeau | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: fix after rebase (from_ctx/from_env) | Matthieu Sozeau | |
| 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-09-27 | Removing uselessly duplicated function in Evd. | Pierre-Marie Pédrot | |
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau | |
| ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. | |||
| 2015-09-08 | Opacifying the proof_terminator type. | Pierre-Marie Pédrot | |
| 2015-09-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-03 | Improve directives for Haskell extraction of nat. | Maxime Dénès | |
| 2015-09-03 | Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v | Nickolai Zeldovich | |
| The previous extraction of [Z.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Z.modulo], with the same check for modulo-by-zero. | |||
| 2015-09-03 | Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v | Nickolai Zeldovich | |
| The previous extraction of [Nat.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Nat.modulo], with the same check for modulo-by-zero. | |||
| 2015-07-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-22 | Extraction: fix primitive projection extraction. | Matthieu Sozeau | |
| Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly. | |||
| 2015-06-22 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-06-22 | Add efficient extraction of [nat], [Z], and [string] to Haskell | Nickolai Zeldovich | |
| This mirrors the existing extraction libraries for OCaml. One wart: the extraction for [string] requires that the Haskell code imports Data.Bits and Data.Char. Coq has no way to add extra import statements to the extracted code. So we have to rely on the user to somehow import these libraries (e.g., using the -pgmF ghc option). See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189 Message to github robot: this commit closes #65 | |||
| 2015-06-06 | micromega : fix silly timeout | Frédéric Besson | |
| 2015-05-26 | micromega : options to limit proof search | Frédéric Besson | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |