| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-22 | romega: add a tactic named unsafe_romega (for debugging, or bold users) | Pierre Letouzey | |
| In this variant, the proof term produced by romega isn't verified at the tactic run-time (no vm_compute). In theory, [unsafe_romega] should behave exactly as [romega], but faster. Now, if there's a bug in romega, we'll be notified only at the following Qed. This could be interesting for debugging purpose : you could inspect the produced buggish term via a Show Proof. | |||
| 2017-05-22 | romega: no more normalization trace, replaced by some Coq-side computation | Pierre Letouzey | |
| This is a major change : - Generated proofs are quite shorter, since only the resolution trace remains. - No time penalty mesured (it even tends to be slightly faster this way). - Less infrastructure in ReflOmegaCore and refl_omega. - Warning: the normalization functions in ML and in Coq should be kept in sync, as well as the variable order. - Btw: get rid of ML constructor Oufo | |||
| 2017-05-22 | romega/const_omega : a few improvements (less try with, no gen equality) | Pierre Letouzey | |
| 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-20 | Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890). | Maxime Dénès | |
| 2017-05-20 | Merge PR#654: Travis: do not cache opam logs (+prettier spacing) | 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 | 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#640: [toplevel] Restore 8.6 goal printing behavior. | Maxime Dénès | |
| 2017-05-19 | Travis: do not cache opam logs (+prettier spacing) | Gaetan Gilbert | |
| 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-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 | [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 | |
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | |
| 2017-05-17 | Merge PR#607: Make congruence reuse discriminate instead of rolling its own. | Maxime Dénès | |
| 2017-05-17 | [toplevel] Restore 8.6 goal printing behavior. | Emilio Jesus Gallego Arias | |
| 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"). | |||
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-17 | Merge PR#620: Reorganization of the layout for miscellaneous tests | Maxime Dénès | |
| 2017-05-17 | Merge PR#614: Improve Travis | Maxime Dénès | |
| 2017-05-17 | Travis: add -warn-error targets (standard and 4.04.1 ocaml) | Gaetan Gilbert | |
| 2017-05-17 | Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanup | Maxime Dénès | |
| 2017-05-17 | Travis: deduplicate package list for coqide+documentation targets | Gaetan Gilbert | |
| 2017-05-17 | Travis: do not run the tests if building Coq fails | Gaetan Gilbert | |
| 2017-05-17 | Merge PR#635: Fixing #5522 (anomaly with free vars of pat) | Maxime Dénès | |
| 2017-05-17 | Merge PR#636: Miscellaneous typos, dead code, etc. | Maxime Dénès | |
| 2017-05-17 | Merge PR#639: Stop using auto with * in two proofs. | Maxime Dénès | |
| 2017-05-16 | Stop using auto with * in two proofs. | Théo Zimmermann | |
| auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db. | |||
| 2017-05-16 | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. | Hugo Herbelin | |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |