| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-30 | Reordering Termops w.r.t. Evd and Namegen in engine folder. | Pierre-Marie Pédrot | |
| 2016-10-30 | Fix spurious OCaml Warning 56 in TACTIC EXTEND macros. | Pierre-Marie Pédrot | |
| 2016-10-29 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-29 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-29 | Removing dead code. | Hugo Herbelin | |
| 2016-10-29 | Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c). | Hugo Herbelin | |
| (May it fell in the case mentioned in the inner comment of Exninfo.info?) | |||
| 2016-10-29 | Documenting changes in typeclasses | Matthieu Sozeau | |
| 2016-10-29 | Fixing #5164 (regression in locating error in argument of "refine"). | Hugo Herbelin | |
| Reporting location was not expecting a term passed to an ML tactic to be interpreted by the ML tactic itself. Made an empirical fix to report about the as-precise-as-possible location available. | |||
| 2016-10-28 | Merge remote-tracking branch 'github/pr/321' into v8.6 | Maxime Dénès | |
| Was PR#321: Handling of section variables in hints | |||
| 2016-10-28 | Merge remote-tracking branch 'github/pr/319' into v8.6 | Maxime Dénès | |
| Was PR#319: More error tagging, try to fix bug 5135 | |||
| 2016-10-28 | Merge commit 'fccbd64' into v8.6 | Maxime Dénès | |
| Was PR#187: Add a META file to support ocamlfind linking. | |||
| 2016-10-28 | [build] Add a target to install the META file. | Emilio Jesus Gallego Arias | |
| 2016-10-28 | [build] META file to enable plugin linking with ocamlfind. | Emilio Jesus Gallego Arias | |
| This allows building SerAPI and jsCoq using ocamlbuild. | |||
| 2016-10-28 | Merge remote-tracking branch 'github/pr/337' into v8.6 | Maxime Dénès | |
| Was PR#337: Fix arguments | |||
| 2016-10-27 | Fixing #5161 (case of a notation with unability to detect a recursive binder). | Hugo Herbelin | |
| Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations. | |||
| 2016-10-27 | COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ↵ | Matej Kosik | |
| generates garbage. So the comment is kept but it is not passed over to ocamldoc. | |||
| 2016-10-27 | Add missing dot to impargs error message. | Maxime Dénès | |
| 2016-10-27 | Proper fix for #3753 (anomaly with implicit arguments and renamings) | Maxime Dénès | |
| Instead of circumventing the problem on the caller's side, as was done in Arguments, we simply avoid failing as there was no real reason for this anomaly to be triggered. If the list of renamings is shorter than the one of implicits, we simply interpret the remaining arguments as not renamed. | |||
| 2016-10-27 | Complete overhaul of the Arguments vernacular. | Maxime Dénès | |
| The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs. | |||
| 2016-10-26 | Using msg_info for info_auto and info_eauto (PR #324). | Hugo Herbelin | |
| 2016-10-26 | STM: make ~valid state id non optional from APIs | Enrico Tassi | |
| It used to be Stateid.initial by default. That is indeed a valid state id but very likely not the very best one (that would be the tip of the document). | |||
| 2016-10-26 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-26 | COMMENT: Namegen.next_ident_away | Matej Kosik | |
| 2016-10-26 | COMMENT: Declarations.constant_def | Matej Kosik | |
| 2016-10-26 | COMMENT: Names.Cmap and Names.Cmap_env | Matej Kosik | |
| 2016-10-26 | COMMENT: Proofview.entry | Matej Kosik | |
| 2016-10-26 | COMMENT: Constr.kind_of_term | Matej Kosik | |
| 2016-10-25 | Merge remote-tracking branch 'github/pr/338' into v8.5 | Maxime Dénès | |
| Was PR#338: Remove warning now that info_auto is fixed. | |||
| 2016-10-25 | Remove warning now that info_auto is fixed. | Théo Zimmermann | |
| Removes a warning dating from 8.5 signaling that info_auto and info_trivial are broken and advising to use Info 1 auto instead. Now, these tactics are fixed and thus they can be used again. They do not do exactly the same thing as Info 1 auto and may be more useful for the learner. | |||
| 2016-10-25 | Remove v62 from the refman. | Théo Zimmermann | |
| 2016-10-25 | Remove v62 from the codebase. | Théo Zimmermann | |
| 2016-10-25 | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | |
| This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses. | |||
| 2016-10-25 | Merge commit 'a799600' into v8.6 | Maxime Dénès | |
| Was PR#334: Fix bug 5031 : should not be an anomaly | |||
| 2016-10-25 | That Function is unable to create a Fixpoint equation is a user problem, | Yves Bertot | |
| not an anomaly | |||
| 2016-10-25 | Update CHANGES. | Maxime Dénès | |
| 2016-10-25 | Bump version number to 8.5pl3. | Maxime Dénès | |
| 2016-10-25 | Merge remote-tracking branch 'github/pr/333' into v8.5 | Maxime Dénès | |
| Was PR#233: Fix a bug in error printing of unif constraints | |||
| 2016-10-25 | Merge remote-tracking branch 'github/pr/329' into v8.5 | Maxime Dénès | |
| Was PR#329: Fix #5127 Memory corruption with the VM | |||
| 2016-10-24 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-24 | Adding a test for #4398 (interpretation scopes for "match goal"). | Hugo Herbelin | |
| 2016-10-24 | Rename lia.cache into .lia.cache in the test-suite Makefile. | Maxime Dénès | |
| 2016-10-24 | Merge commit '81bdc22' into v8.6 | Maxime Dénès | |
| Was PR#301: Update .gitignore with new names for psatz caches. | |||
| 2016-10-24 | Merge remote-tracking branch 'github/pr/326' into v8.5 | Maxime Dénès | |
| Was PR#326: Extend documentation of auto | |||
| 2016-10-24 | Test file for #5127: Memory corruption with the VM | Maxime Dénès | |
| 2016-10-24 | Fix #5127 Memory corruption with the VM | Maxime Dénès | |
| The bytecode interpreter ensures that the stack space available at some points is above a static threshold. However, arbitrary large stack space can be needed between two check points, leading to segmentation faults in some cases. We track the use of stack space at compilation time and add an instruction to ensure greater stack capacity when required. This is inspired from OCaml's PR#339 and PR#7168. Patch written with Benjamin Grégoire. | |||
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Hugo Herbelin | |
| + a few improvements on 5f1dd4c40 (lexing of { and }). | |||
| 2016-10-24 | Remove v62 from stdlib. | Théo Zimmermann | |
| This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore. | |||
| 2016-10-24 | ssrmatching: fix interpretation of rpattern | Enrico Tassi | |
| 2016-10-24 | Fixing a location bug with "?" and "$". | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |