| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-22 | romega: use N instead of nat for Tvar | Pierre Letouzey | |
| In a coming commit, we'll normalize terms by a Coq function that will compare Tvar's instead of blindly applying a trace, so let's speed-up these comparisons. | |||
| 2017-05-22 | romega: shorter trace (no more term lengths) | Pierre Letouzey | |
| 2017-05-22 | refl_omega: refactoring of normalize_equation | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: lots of dead code + a few refactored proofs | Pierre Letouzey | |
| 2017-05-22 | romega: if it bugs again, at least do it with a short and quick error | Pierre Letouzey | |
| 2017-05-22 | refl_omega: comment the lack of lifts when dealing with arrows | Pierre Letouzey | |
| 2017-05-22 | romega: discard constructor D_mono (shorter trace + fix a bug) | Pierre Letouzey | |
| For the bug, see new test test_romega10 in test-suite/success/ROmega0.v. | |||
| 2017-05-22 | refl_omega: more refactoring (e.g. IntSets instead of sorted lists) | Pierre Letouzey | |
| 2017-05-22 | refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp) | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: discard useless cosntructor P_NOP | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||]) | Pierre Letouzey | |
| 2017-05-22 | Compatibility fix while waiting for integration of Pierre Courtieu's PR #449. | Hugo Herbelin | |
| 2017-05-22 | Using type classes in the interpretation of "specialize" and "contradiction". | Hugo Herbelin | |
| We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153. | |||
| 2017-05-22 | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | |
| This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility. | |||
| 2017-05-20 | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin | |
| 2017-05-20 | Deprecate -nodoc. | Théo Zimmermann | |
| 2017-05-20 | [coqdoc] Add keywords in bug 2884. | Emilio Jesus Gallego Arias | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |