| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-25 | Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming ↵ | Arnaud Spiwack | |
| guardedness. | |||
| 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-24 | Add corresponding field in `VernacInductive`. | Arnaud Spiwack | |
| Makes sure not to generate inductive schemes of assumed positive types. | |||
| 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 | |
| 2015-05-15 | Merge v8.5 into trunk | Hugo Herbelin | |
| Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot | |
| Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. | |||
| 2015-05-11 | Rationalizing a bit the interface of Hints. | Pierre-Marie Pédrot | |
| 2015-05-05 | Fix bug #4212, congruence forgetting about some universe constraints. | Matthieu Sozeau | |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-28 | maintenance micromega plugin | Frédéric Besson | |
| - add a nra tactic (similar to nia) for non-linear real arithmetic tactic - fix a long-standing bug in the reification code - port to the new proof-engine | |||
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond | |
| 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. | |||
| 2015-04-23 | Using tclZEROMSG instead of tclZERO in several places. | Pierre-Marie Pédrot | |
| 2015-04-22 | Declarative mode: remaining goals are "given up" when closing blocks. | Arnaud Spiwack | |
| Restores the intended behaviour from v8.3 and earlier. | |||
| 2015-04-15 | Remove dirty debug printing from funind. | Maxime Dénès | |
| 2015-04-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-14 | Function now supports puniveres | jforest | |
| 2015-04-14 | better debug in recdef | jforest | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |