| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-04-28 | Fix incorrect syntax highlighting after the Goal command. | Guillaume Melquiond | |
| 2014-04-28 | Fixing coqdoc bug #3292 (unfortunate collision betweens the relative | Hugo Herbelin | |
| locations found when parsing expressions in comments and the absolute locations in the glob file). As now, the glob file does not parse comment, so I removed the test for location when parsing expressions in comments, which anyway are not linkable, precisely because not parsed by coqc. | |||
| 2014-04-28 | Fixing #3293 (eta-expansion at "match" printing time was failing | Hugo Herbelin | |
| because of let-in's interpreted as being part of the expansion). | |||
| 2014-04-28 | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin | |
| one_inductive_body so that when eta-expanding at "match" printing time we know if a let is part of the expected signature or part of the body. This is an easy fix for bugs like #3293. Another fix could be to enforce, as an invariant, or better syntactically, that "match"/"Case"'s have the body of their branches expanded. | |||
| 2014-04-27 | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot | |
| 2014-04-27 | Giving true proof-terms in inversion instead of metas. | Pierre-Marie Pédrot | |
| 2014-04-25 | coq_makefile: -I for the new stm/ dir | Enrico Tassi | |
| 2014-04-25 | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | Pierre-Marie Pédrot | |
| files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM. | |||
| 2014-04-25 | Removing Autoinstance once and for all. | Pierre-Marie Pédrot | |
| 2014-04-25 | Removing useless try-with clauses in Goal.enter variants. | Pierre-Marie Pédrot | |
| 2014-04-25 | Future: memory optimization when forcing a chained pure computation | Enrico Tassi | |
| Kudos to PMP for spotting that! | |||
| 2014-04-25 | Opaqueproofs: sink futures when interactive | Enrico Tassi | |
| 2014-04-25 | print futures in caml toplevel too | Enrico Tassi | |
| 2014-04-25 | Fix a second, trickier, typo in Termops.eta_reduce_head. | Arnaud Spiwack | |
| 2014-04-25 | Adding a debug printer for futures. | Pierre-Marie Pédrot | |
| 2014-04-25 | Fixing various backtrace recordings. | Pierre-Marie Pédrot | |
| 2014-04-25 | Fix a small typo in Termops.eta_reduce_head. | Arnaud Spiwack | |
| 2014-04-24 | Adding a [fold_map] operation on constrs. | Pierre-Marie Pédrot | |
| 2014-04-24 | Writing tclABSTRACT in the new monad. In particular the unsafe status is now | Pierre-Marie Pédrot | |
| preserved. | |||
| 2014-04-23 | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot | |
| any length with a [None] representation and ensure that this representation is canonical through the restricted interface. | |||
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | |
| 2014-04-23 | Import proof of decidability of negated formulas from Coquelicot. | Guillaume Melquiond | |
| 2014-04-22 | Remove some uses of excluded middle. | Guillaume Melquiond | |
| 2014-04-22 | Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from ↵ | Guillaume Melquiond | |
| Coquelicot. This change removes the need for excluded middle. It also greatly simplifies the proof (no need for geometric series, limits, constructive epsilon, and so on). | |||
| 2014-04-22 | Add regression tests for 3188 and 3265 | Jason Gross | |
| 2014-04-22 | Removing the compatibility layer from Leminv. Also removed an undocumented | Pierre-Marie Pédrot | |
| variant of the Derive Inversion command which took the current goal as the targeted inductive. It was unused in the contribs and it seemed rather bad from the STM point of view, as it generated a lemma inside a proof. | |||
| 2014-04-22 | Using the new monad tactic in Inv. | Pierre-Marie Pédrot | |
| 2014-04-22 | Removing tactic compatibility layer from Elim. | Pierre-Marie Pédrot | |
| 2014-04-22 | Small code cleaning in Tacticals. | Pierre-Marie Pédrot | |
| 2014-04-22 | Simplifying interface of elimination tactics. They used dummy clausenvs, and | Pierre-Marie Pédrot | |
| that should be changed anyway. | |||
| 2014-04-20 | Adding a test for bug #2923. | Pierre-Marie Pédrot | |
| 2014-04-20 | Adding a test for bug #3285. | Pierre-Marie Pédrot | |
| 2014-04-20 | Fixing bug #3285. | Pierre-Marie Pédrot | |
| 2014-04-20 | Adding a [map] primitive to the tactic monad. Hopefully this should be | Pierre-Marie Pédrot | |
| slightly more efficient in general. | |||
| 2014-04-16 | Fixing missing headers. | Hugo Herbelin | |
| 2014-04-14 | Closing bug #3260 | Julien Forest | |
| adding a new grammar entry for clauses | |||
| 2014-04-10 | Fix guard condition for nested cofixpoints in checker. | Maxime Dénès | |
| 2014-04-10 | Fix guard condition for nested cofixpoints. | Maxime Dénès | |
| There were actually two problems, one of them being clearly unsound. To make sure that this does not show up somewhere else in the code, it would be better to resort to an abstraction keeping in sync the environment and the De Bruijn index of the current cofixpoints, like guard_env does for fixpoints. | |||
| 2014-04-10 | better description of bug 3251 | Enrico Tassi | |
| 2014-04-10 | Have the feedback bus as a backend for dumping globs. | Carst Tankink | |
| 2014-04-10 | Dumpglob: factor out reference dumping. | Carst Tankink | |
| Factored out all functions that dump references to use one function "dump_ref" | |||
| 2014-04-10 | CoqIDE: options for syntax highlighting | Enrico Tassi | |
| 2014-04-10 | CoqIDE: removing a timer may raise an exception | Enrico Tassi | |
| 2014-04-10 | coqtop -batch refuses Back 1 but accepts Undo. | Pierre Boutillier | |
| 2014-04-10 | By resolution of the CoqWG, instantiate must not be used now that refine works | Pierre Boutillier | |
| 2014-04-10 | No more Coersion in Init. | Pierre Boutillier | |
| 2014-04-10 | Define [projT3] and [proj3_sig] | Jason Gross | |
| Also allow [projT1]/[projT2] to work for [sigT2]s and [proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions. This closes Bug 3044. This closes Pull Request #4. | |||
| 2014-04-10 | Test case for bug 3037 | Jason Gross | |
| Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9 | |||
| 2014-04-10 | Test case for 3164 | Jason Gross | |
| Closed in 69c4d0fd7b8325187e8da697a9c283594047d. I used [Timeout 2] to distinguish between stack overflow and immediate return. | |||
| 2014-04-10 | Test case for bug 3262 | Jason Gross | |
| Closed in f65fa9de8a4c9c12d933188a755b51508bd51921 I used [Timeout 2 Fail] to test the difference between immediate failure and stack overflow. Hopefully this is robust enough. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |