| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-20 | Change wrong bullet message. | Théo Zimmermann | |
| Remove a space before colon. Remove the use of term mandatory (this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994). | |||
| 2017-05-20 | Revised behavior on ill-formed identifiers. | Hugo Herbelin | |
| Namely: Replacing (currently deactivated) warning on illegal ident by an error in strict mode and nothing in soft mode. | |||
| 2017-05-20 | Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890). | Maxime Dénès | |
| 2017-05-20 | Mention ./configure in INSTALL.doc | Théo Zimmermann | |
| As prompted in https://coq.inria.fr/bugs/show_bug.cgi?id=2831 | |||
| 2017-05-20 | Merge PR#654: Travis: do not cache opam logs (+prettier spacing) | Maxime Dénès | |
| 2017-05-20 | Merge PR#653: Bug #5535, test for Show with -emacs | Maxime Dénès | |
| 2017-05-20 | Merge PR#643: [ide] Disable `print_ast` call. | Maxime Dénès | |
| 2017-05-20 | Merge PR#474: A fix for #5390 (a useful error on used introduction names was ↵ | Maxime Dénès | |
| masked). | |||
| 2017-05-20 | [test-suite] Add tests for goal printing. | Emilio Jesus Gallego Arias | |
| - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 See also PR #640 | |||
| 2017-05-20 | Merge PR#627: Obligations shrinking: shrink abstraction too | Maxime Dénès | |
| 2017-05-20 | Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520) | Maxime Dénès | |
| 2017-05-20 | Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.el | Maxime Dénès | |
| 2017-05-20 | Merge PR#649: Fix a typo | Maxime Dénès | |
| 2017-05-20 | Merge PR#651: Re-adding explicit dependency of misc universe test into ↵ | Maxime Dénès | |
| all_stdlib.v. | |||
| 2017-05-20 | Merge PR#641: Fix bug #5486, don't reverse ids in tuples | Maxime Dénès | |
| 2017-05-20 | Merge PR#640: [toplevel] Restore 8.6 goal printing behavior. | Maxime Dénès | |
| 2017-05-19 | Exporting some functions of vars.ml as functions operating on EConstr. | Hugo Herbelin | |
| 2017-05-19 | In EConstr, defining some "cast" functions earlier. | Hugo Herbelin | |
| This allows to use a cast in subst_of_rel_context_instance. Also added more cast functions for further use. | |||
| 2017-05-19 | Moving "sym" on "eq" type to lib/util.ml. | Hugo Herbelin | |
| 2017-05-19 | Travis: do not cache opam logs (+prettier spacing) | Gaetan Gilbert | |
| 2017-05-19 | add test for Show with -emacs, bug 5535 | Paul Steckler | |
| 2017-05-19 | Adding new tactic notation scopes. | Pierre-Marie Pédrot | |
| 2017-05-19 | Extending the Coq API in Ltac2. | Pierre-Marie Pédrot | |
| 2017-05-19 | Removing dead code in Ltac2, and cleaning up a bit. | Pierre-Marie Pédrot | |
| 2017-05-19 | Introducing tactic notations in Ltac2. | Pierre-Marie Pédrot | |
| 2017-05-19 | Allow raw terms to contain references to absolute definitions. | Pierre-Marie Pédrot | |
| 2017-05-19 | Stdlib functions now return Ltac2 exceptions. | Pierre-Marie Pédrot | |
| 2017-05-19 | Proper handling of exception definition in Ltac2. | Pierre-Marie Pédrot | |
| We actually implemented a full-fledged open type system, so that exceptions are a special case of it. | |||
| 2017-05-19 | Merging GTacTuple and GTacCst nodes. | Pierre-Marie Pédrot | |
| 2017-05-19 | Towards a proper printing of Ltac2 data structures. | Pierre-Marie Pédrot | |
| 2017-05-19 | Allow the embedding of Ltac2 terms in constrs via the ltac2:(...) syntax. | Pierre-Marie Pédrot | |
| 2017-05-19 | Fixing a precedence issue in type parameters. | Pierre-Marie Pédrot | |
| 2017-05-19 | Proper handling of record types. | Pierre-Marie Pédrot | |
| We add the standard ML facilities for records, that is, projections, mutable fields and primitive to set them. | |||
| 2017-05-19 | Allowing to include Coq terms in Ltac2 using the constr:(...) syntax. | Pierre-Marie Pédrot | |
| 2017-05-19 | Embedding generic arguments in Ltac2 AST. | Pierre-Marie Pédrot | |
| 2017-05-19 | Introduction of the Ltac2 plugin. | Pierre-Marie Pédrot | |
| For now, it is only a simple mini-ML whose effects are the proofview monad. There is no facility to manipulate terms nor any hardwired tactic. Pattern-matching is restricted to superficial constructors, the language is lacking a lot of user-friendly interfaces, the grammar is crappy, and much more. | |||
| 2017-05-19 | Re-adding explicit dependency of misc universe test into all_stdlib.v. | Hugo Herbelin | |
| Was working when calling test-suite from main Makefile but not when calling directly from the test-suite Makefile. The dependency was mistakenly dropped in 98a927aef. | |||
| 2017-05-19 | Fixing an extra bug with pattern_of_constr. | Hugo Herbelin | |
| Ensure in type constr_pattern that those preexisting existential variables of the goal which do not contribute as pattern variables are expanded: constr_pattern is not observed up to evar expansion (like EConstr does), so we need to pre-normalize defined evars in patterns to that matching against an EConstr works. | |||
| 2017-05-19 | Removing unused warnings. | Pierre-Marie Pédrot | |
| 2017-05-19 | Merge branch 'master' into ltac2-hooks | Pierre-Marie Pédrot | |
| 2017-05-18 | Fix a typo | Jason Gross | |
| 2017-05-18 | Add .dir-locals.el to plugins | Jason Gross | |
| As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542 | |||
| 2017-05-18 | Adding a trespasser warning to the Nametab API. | Pierre-Marie Pédrot | |
| 2017-05-18 | [stm] Tweak debug options. | Emilio Jesus Gallego Arias | |
| We allow for a dynamic setting of the STM debug flag, and we print some more information about the result of `process_transaction`. We also fix a printing bug due to mixing `Printf` and `Format`, which are not compatible. | |||
| 2017-05-18 | [toplevel] [stm] Avoid edit_at in batch mode (bug #5520) | Emilio Jesus Gallego Arias | |
| In non-interactive mode, `edit_at` seems to do very weird things, for instance will try to recompute all the previous states which seems weird. We better avoid that to approximate 8.6 behavior while we investigate more. | |||
| 2017-05-18 | [ide] Disable `print_ast` call. | Emilio Jesus Gallego Arias | |
| So far this part of the system has shown little utility other than having developers put time to fix it every time they change something in the system. I have never seen this functionality used in the wild, and a large part of the vernac was marked TODO. Given that we have automatic methods to provide this functionality these days (PPX), we remove Texmacspp. | |||
| 2017-05-17 | A fix for #5390 (a useful error on used introduction names was masked). | Hugo Herbelin | |
| With the "apply in" introduction pattern, and the backtrack possibly done in "apply" over the components of conjunctions (descend_in_conjunctions), the reasons for failing might have different sources. We give priority to the detection of used names over other (unification) errors so that an error there is not masked in the backtracking made by descend_in_conjunctions. Of course, the question of what best unification error to give in the presence of backtracking is still open. | |||
| 2017-05-17 | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵ | Maxime Dénès | |
| tricks available to users | |||
| 2017-05-17 | Documenting relaxing of constraints on injection. | Hugo Herbelin | |
| We seized this opportunity to do a little refreshing of the section describing injection. | |||
| 2017-05-17 | Stopping injection not to work on discriminable atoms (see #4890). | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |