Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | More code sharing between tactic notation and genarg interpretation. | Pierre-Marie Pédrot | 2015-12-13 |
| | |||
* | Removing dead unsafe code in Genarg. | Pierre-Marie Pédrot | 2015-12-12 |
| | |||
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-11 |
|\ | |||
| * | Document removal of Set Virtual Machine and -vm in CHANGES. | Maxime Dénès | 2015-12-11 |
| | | |||
| * | Remove Set Virtual Machine from doc, since the command itself has been removed. | Maxime Dénès | 2015-12-11 |
| | | |||
| * | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès | 2015-12-11 |
| | | |||
| * | Fixing a pat%constr bug. Thanks to Enrico for reporting. | Hugo Herbelin | 2015-12-10 |
| | | |||
| * | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | 2015-12-10 |
| | | | | | | | | Marking it as experimental. | ||
| * | Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing | Hugo Herbelin | 2015-12-10 |
| | | | | | | | | "open Unix" from lib/system.ml. | ||
| * | Silently ignore requests to _not_ clear something when that something cannot ↵ | Guillaume Melquiond | 2015-12-10 |
| | | | | | | | | | | | | be cleared. This should fix the contrib failures on tactics like "destruct (0)". | ||
| * | Refman, ch. 4: A few fixes. | Hugo Herbelin | 2015-12-10 |
| | | |||
| * | ENH: redundant examples were removed | Matej Kosik | 2015-12-10 |
| | | |||
| * | FIX: wrong reference to a figure | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP: putting examples inside "figure" environment | Matej Kosik | 2015-12-10 |
| | | |||
| * | ENH: The definition of the "_ ; _" operation on local context was added. | Matej Kosik | 2015-12-10 |
| | | |||
| * | TYPOGRAPHY: adjustments | Matej Kosik | 2015-12-10 |
| | | |||
| * | PROPOSITION: the side-condition was made more specific. | Matej Kosik | 2015-12-10 |
| | | |||
| * | PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]' | Matej Kosik | 2015-12-10 |
| | | |||
| * | PROPOSITION: Added an explicit definition of the notation for enriching the ↵ | Matej Kosik | 2015-12-10 |
| | | | | | | | | global environment (we use throughout the document) | ||
| * | PROPOSITION: Added "if" and "then" words missing in the original sentence. | Matej Kosik | 2015-12-10 |
| | | |||
| * | PROPOSITION: Example was simplified | Matej Kosik | 2015-12-10 |
| | | |||
| * | DONE | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | TYPOGRAPHY | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: to do | Matej Kosik | 2015-12-10 |
| | | |||
| * | GRAMMAR: added punctuation | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP PROPOSITION: rephrasing the original idea in a simpler way | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP PROPOSITION: existing example was removed because it is not urgently ↵ | Matej Kosik | 2015-12-10 |
| | | | | | | | | needed | ||
| * | ENH: existing example was changed so that it is now linked to the results ↵ | Matej Kosik | 2015-12-10 |
| | | | | | | | | shown in the previous example | ||
| * | ENH: an existing example was further expanded. | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP: Existing example was removed. | Matej Kosik | 2015-12-10 |
| | | | | | | | | | | | | | | We have expanded the example above. For consistency reasons, it would make sense to do the same also for this example. However, due to the size of the terms, it is hard to typeset it nicely. I propose to remove it. | ||
| * | ENH: existing example was expanded | Matej Kosik | 2015-12-10 |
| | | |||
| * | ENH: define the meaning of 'p' | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive ↵ | Matej Kosik | 2015-12-10 |
| | | | | | | | | definition'? Doesn't make more sense to refer to it as 'inductive type'? | ||
| * | CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive ↵ | Matej Kosik | 2015-12-10 |
| | | | | | | | | definition. | ||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP: removing a superfluous index | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | GRAMMAR | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: note | Matej Kosik | 2015-12-10 |
| | | |||
| * | TYPOGRAPHY | Matej Kosik | 2015-12-10 |
| | | |||
| * | CLEANUP: originally, we talked about "B" as an "arity" | Matej Kosik | 2015-12-10 |
| | | |||
| * | COMMENT: question | Matej Kosik | 2015-12-10 |
| | | |||
| * | ENH: a forward reference to a place where the concept of "allowed ↵ | Matej Kosik | 2015-12-10 |
| | | | | | | | | elimination sorts" is actually used |