| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-05-02 | Update test-suite Makefile to handle coq-prog-args | Jason Gross | |
| 2014-05-01 | Allowing the "Declare Instance" command anywhere. This was artificially | Pierre-Marie Pédrot | |
| restricted to module types, although it was nothing more than a short hand for Axiom + Existing Instance. | |||
| 2014-05-01 | Fixing ml-doc. | Pierre-Marie Pédrot | |
| 2014-04-30 | Fix Qcanon after changes on injection. | Maxime Dénès | |
| 2014-04-30 | Document changes on injection. | Maxime Dénès | |
| 2014-04-30 | Trying to improve the error messages of injection. | Maxime Dénès | |
| Below are a few examples where the previous messages were misleading: Module InProp. Inductive tree : Prop := Leaf | Node : tree -> tree -> tree. Variables x y : tree. (* Wrong msg: "Nothing to do, it is an equality between convertible terms." *) (* These terms are not convertible *) Goal Node Leaf Leaf = Leaf -> False. Fail intros H; injection H. Abort. End InProp. Module InSet. Inductive tree : Set := Leaf | Node : tree -> tree -> tree. Variables x y : tree. (* Wrong msg: "Not a projectable equality but a discriminable one." *) (* This equality is both projectable and discriminable *) Goal Node x (Node Leaf Leaf) = Node Leaf Leaf -> False. intros H. Fail injection H. Abort. End InSet. | |||
| 2014-04-29 | Injection: do not fail when arguments have sort Prop. | Maxime Dénès | |
| This historic limitation of the injection tactic does not seem to have any precise justification. In fact, the only equalities that are not projectable is when the arguments of the constructor have sort Set or Type and the inductive type is in Prop (due to the restriction on pattern matching). The command "Unset Injection On Proofs" restores the old behavior. | |||
| 2014-04-29 | Native compiler: hide compiled files in a .coq-native subdirectory. | Maxime Dénès | |
| 2014-04-29 | Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately | Hugo Herbelin | |
| did not notice that kernel/values.ml had to be made consistent with kernel/cic.mli). | |||
| 2014-04-28 | Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for ↵ | Guillaume Melquiond | |
| bug #2964) | |||
| 2014-04-28 | Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964) | Guillaume Melquiond | |
| 2014-04-28 | Recognize Parameters as a command in coqdoc. (Fix for bug #3279) | Guillaume Melquiond | |
| 2014-04-28 | Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276) | Guillaume Melquiond | |
| 2014-04-28 | Remove unused lookup table. | Guillaume Melquiond | |
| 2014-04-28 | Fix broken commit 2bcb2cb. | Guillaume Melquiond | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |