aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | | | | | * | | | Using type classes in the interpretation of "specialize" and "contradiction".Gravatar Hugo Herbelin2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | * | | | Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
| |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * | | | | | | Added a test for #4765 (an example of printing abbreviation with binders).Gravatar Hugo Herbelin2017-05-20
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
| | | | | * | | | | | | Deprecate -nodoc.Gravatar Théo Zimmermann2017-05-20
| | | | | | | | | | | |
| | | | | | | | | | | * [coqdoc] Add keywords in bug 2884.Gravatar Emilio Jesus Gallego Arias2017-05-20
| | | | | | | | | | | |
| | * | | | | | | | | | Change wrong bullet message.Gravatar Théo Zimmermann2017-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Remove a space before colon. Remove the use of term mandatory (this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
| | | * | | | | | | | | Revised behavior on ill-formed identifiers.Gravatar Hugo Herbelin2017-05-20
| |_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Namely: Replacing (currently deactivated) warning on illegal ident by an error in strict mode and nothing in soft mode.
* | | | | | | | | | | Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | Mention ./configure in INSTALL.docGravatar Théo Zimmermann2017-05-20
| | | | |/ / / / / / / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | As prompted in https://coq.inria.fr/bugs/show_bug.cgi?id=2831
* | | | | | | | | | | Merge PR#654: Travis: do not cache opam logs (+prettier spacing)Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#643: [ide] Disable `print_ast` call.Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR#474: A fix for #5390 (a useful error on used introduction names was ↵Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | masked).
| | | | | | | * | | | | | [test-suite] Add tests for goal printing.Gravatar Emilio Jesus Gallego Arias2017-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 See also PR #640
* | | | | | | | | | | | | Merge PR#627: Obligations shrinking: shrink abstraction tooGravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.elGravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#649: Fix a typoGravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#651: Re-adding explicit dependency of misc universe test into ↵Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_stdlib.v.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * Exporting some functions of vars.ml as functions operating on EConstr.Gravatar Hugo Herbelin2017-05-19
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * In EConstr, defining some "cast" functions earlier.Gravatar Hugo Herbelin2017-05-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to use a cast in subst_of_rel_context_instance. Also added more cast functions for further use.
| | | | | | | | | | | | | | | | * Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
| | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | Travis: do not cache opam logs (+prettier spacing)Gravatar Gaetan Gilbert2017-05-19
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | Re-adding explicit dependency of misc universe test into all_stdlib.v.Gravatar Hugo Herbelin2017-05-19
| |/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | * | | | | Fixing an extra bug with pattern_of_constr.Gravatar Hugo Herbelin2017-05-19
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | | * | | Removing unused warnings.Gravatar Pierre-Marie Pédrot2017-05-19
| | | | | | | | | | | | | |
| | | | | | | | | | | * | | Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | | | | | | | | | | |\ \ \ | |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | |
| | * | | | | | | | | | | | Fix a typoGravatar Jason Gross2017-05-18
| |/ / / / / / / / / / / / |/| | | | | | | | | | | |
| | * | | | | | | | | | | Add .dir-locals.el to pluginsGravatar Jason Gross2017-05-18
| |/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542
| | | | | | | | | * | | Adding a trespasser warning to the Nametab API.Gravatar Pierre-Marie Pédrot2017-05-18
| | | | | | | | | | | |
| | | | | | | | | | * | [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | | | | | | [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Emilio Jesus Gallego Arias2017-05-18
| | | |_|_|_|_|_|_|/ / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * | | | | | [ide] Disable `print_ast` call.Gravatar Emilio Jesus Gallego Arias2017-05-18
| | | |_|/ / / / / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | | | | | A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-05-17
| | | |/ / / / / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ | |_|/ / / / / / / |/| | | | | | | | | | | | | | | | | tricks available to users
| | | | * | | | | Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We seized this opportunity to do a little refreshing of the section describing injection.
| | | | * | | | | Stopping injection not to work on discriminable atoms (see #4890).Gravatar Hugo Herbelin2017-05-17
| |_|_|/ / / / / |/| | | | | | |
* | | | | | | | Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \
| | | | * | | | | | [toplevel] Restore 8.6 goal printing behavior.Gravatar Emilio Jesus Gallego Arias2017-05-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When porting the toplevel to the STM, the logic for goal printing was simplified too much under optimistic assumptions. The idea was not to rely on the `vernac_classifier` which is an internal and complicated beast. However, it seems there are many cases to consider other than `is_query`, so at the risk of reimplementing the classifier we revert to the old approach of using the full classification. This gives maximum 8.6 compatibility, with the pitfall of having to call the classifier. Indeed, due to the dynamic nature of the "undo classifier", we cannot call it after `Stm.add`, as the document tree will be not the right one, making the classification of undo commands incorrect (actually raising an error "Cannot undo").
* | | | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#620: Reorganization of the layout for miscellaneous testsGravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|_|_|/ | |/| | | | | | | | |
* | | | | | | | | | | Merge PR#614: Improve TravisGravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | Travis: add -warn-error targets (standard and 4.04.1 ocaml)Gravatar Gaetan Gilbert2017-05-17
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupGravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | Travis: deduplicate package list for coqide+documentation targetsGravatar Gaetan Gilbert2017-05-17
| | | | | | | | | | | | |
| | * | | | | | | | | | | Travis: do not run the tests if building Coq failsGravatar Gaetan Gilbert2017-05-17
| |/ / / / / / / / / / / |/| | | | | | | | | | |
| | | * | | | | | | | | Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Gravatar Maxime Dénès2017-05-17
| | | |\ \ \ \ \ \ \ \ \
* | | | \ \ \ \ \ \ \ \ \ Merge PR#636: Miscellaneous typos, dead code, etc.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#639: Stop using auto with * in two proofs.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 08:18:45 +0000