| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-03-26 | Removing Tacmach compatibility layer in Inv. | Pierre-Marie Pédrot | |
| 2014-03-26 | Removing tactic compatibility layer from Inv. | Pierre-Marie Pédrot | |
| 2014-03-26 | STM: when an error occurs in a worker send back a bunch of states | Enrico Tassi | |
| In this way when the user fixes the script only a small part of the broken proof has to be recomputed on master. The density of states sent back decreases as they get far from the error. I.e. counting from the error, the worker sends back states at distance 0 1 2 3 5 7 10 14 19 26 35 47... | |||
| 2014-03-26 | CoqIDE: better error reporting for Qed on incomplete proof | Enrico Tassi | |
| 2014-03-26 | test for apply + TC resolution | Enrico Tassi | |
| 2014-03-26 | Adding an interface to Eqdecide and putting the grammar rules in a dedicated | Pierre-Marie Pédrot | |
| file. | |||
| 2014-03-26 | Moving some tactic code to the new engine. | Pierre-Marie Pédrot | |
| 2014-03-24 | Revert "Makefile: the initial build of grammar.cma is now directory-driven" | Pierre Letouzey | |
| This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022. This commit was wrong, since (at least) the highparsing part depends on the toplevel directory. I still didn't had time to fix that, so in the meantime let's revert it. | |||
| 2014-03-20 | Missing equalities in Names-like structures. | Pierre-Marie Pédrot | |
| 2014-03-20 | Slightly more efficient Array.smartmap & related. | Pierre-Marie Pédrot | |
| 2014-03-20 | Documenting the Print Strategy command. | Pierre-Marie Pédrot | |
| 2014-03-19 | Adding a Print Strategy vernacular command. It allows to check the | Pierre-Marie Pédrot | |
| transparent status of variables and constants. | |||
| 2014-03-19 | Using non-normalized goals in tactic interpretation. | Pierre-Marie Pédrot | |
| 2014-03-19 | Adding phantom types to discriminate normalized goals, and adding a way to | Pierre-Marie Pédrot | |
| observe non-normalized goals. | |||
| 2014-03-18 | Remove the -fno-defer-pop cflag | Jason Gross | |
| According to http://caml.inria.fr/mantis/view.php?id=6346, this flag causes ocamlc to fail on the latest version of xcode, because clang now errors on -fno-defer-pop. According to the same issue, -fno-defer-pop is required for computed gotos if you're using gcc 1.xx, but not gcc 3.4.0 nor 4.4.7 (nor presumably other reasonably modern versions of gcc). I haven't actually tested this, as I don't have a mac, but it's a relatively small change. Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org> | |||
| 2014-03-18 | Printing backtraces in coqchk while in debug mode. | Pierre-Marie Pédrot | |
| 2014-03-18 | Fixing checker with respect to new kernel name structure and hashmaps. | Pierre-Marie Pédrot | |
| Some wrong generic equalities and hashes were removed too. | |||
| 2014-03-18 | STM: make the slave start from the most recent known state | Enrico Tassi | |
| 2014-03-18 | STM: make -async-proofs on work from coqc too | Enrico Tassi | |
| 2014-03-17 | Evarconv: exact_ise_stack looks to stack head before bodies or branches | Pierre Boutillier | |
| the order of the inspection is a "random" choise but going back to the old behavior makes the compilation of ssreflect/rat.v 5 times faster ... | |||
| 2014-03-17 | Fix test-suite 2255.v | Pierre Boutillier | |
| 2014-03-16 | consider_remaining_unif_problems respects Conv_oracle | Pierre Boutillier | |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot | |
| no particular purpose. | |||
| 2014-03-13 | nanoPG: better copy/paste | Enrico Tassi | |
| 2014-03-13 | fix compilation with ocaml < 4 | Enrico Tassi | |
| 2014-03-13 | STM: perspective (tell the scheduler what the user sees) | Enrico Tassi | |
| 2014-03-13 | Stateid: export a Set module | Enrico Tassi | |
| 2014-03-13 | STM: move out a couple of submodules | Enrico Tassi | |
| These modules are not as reusable as one may want them to be, but moving them out simplifies a little STM. | |||
| 2014-03-12 | fake_ide: fix compilation | Enrico Tassi | |
| 2014-03-12 | Stm: smarter delegation policy | Enrico Tassi | |
| Stm used to delegate every proof when it was possible, but this may be a bad idea. Small proofs may take less time than the overhead delegation implies (marshalling, etc...). Now it delegates only proofs that take >= 1 second. By default a proof takes 1 second (that may be wrong). If the file was compiled before, it reuses the data stored in the .aux file and assumes the timings are still valid. After a proof is checked, Coq knows how long it takes for real, so it wont predict it wrong again (when the user goes up and down in the file for example). CoqIDE now sends to Coq, as part of the init message, the file name so that Coq can load the .aux file. | |||
| 2014-03-12 | CoqIDE: Errors page gets red if not empty | Enrico Tassi | |
| 2014-03-12 | CoqIDE: detachable message/error/jobs panes | Enrico Tassi | |
| 2014-03-11 | vi2vo: universes handling finally fixed | Enrico Tassi | |
| Universes that are computed in the vi2vo step are not part of the outermost module stocked in the vo file. They are part of the Library.seg_univ segment and are hence added to the safe env when the vo file is loaded. The seg_univ has been augmented. It is now: - an array of universe constraints, one for each constant whose opaque body was computed in the vi2vo phase. This is useful only to print the constants (and its associated constraints). - a union of all the constraints that come from proofs generated in the vi2vo phase. This is morally the missing bits in the toplevel module body stocked in the vo file, and is there to ease the loading of a .vo file (obtained from a .vi file). - a boolean, false if the file is incomplete (.vi) and true if it is complete (.vo obtained via vi2vo). | |||
| 2014-03-11 | Fix (3243): univ constraints of module subtyping were not propagated | Enrico Tassi | |
| Universe constraints coming from subtyping were not propagated to the outermost module and hence not stocked in the .vo file. Still, they were added to the interactive safe environment and hence checked for satisfiability. | |||
| 2014-03-10 | Useless Array.to_list in Typeops. | Pierre-Marie Pédrot | |
| 2014-03-10 | Evarconv unification respects Conv_oracle | Pierre Boutillier | |
| 2014-03-10 | MaybeFlexible semantic changes | Pierre Boutillier | |
| From Maybe reducible to Maybe to reduce (but for sure reducible) | |||
| 2014-03-10 | Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r. | Guillaume Melquiond | |
| 2014-03-08 | Using HMaps in global references. | Pierre-Marie Pédrot | |
| 2014-03-08 | Also use HMaps in KNmap. | Pierre-Marie Pédrot | |
| 2014-03-07 | Potentially unused computation in Goal. | Pierre-Marie Pédrot | |
| 2014-03-07 | Useless tactic bindings in Tacticals. | Pierre-Marie Pédrot | |
| 2014-03-07 | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot | |
| iter order, but it seems nobody was relying on it (contrarily to the string case). | |||
| 2014-03-07 | Tentative fix for a very strange pervasive equality in Auto. | Pierre-Marie Pédrot | |
| 2014-03-07 | Compiling coqc in "tools" target. | Pierre-Marie Pédrot | |
| 2014-03-07 | Fix lookup of native files when option -R is missing. | Guillaume Melquiond | |
| Testcase: mkdir a echo "Definition t := O." > a/a.v coqc -R a a a/a.v echo "Require Import a.a. Definition u := t." > b.v coqc -I . b.v rm -rf a b.* | |||
| 2014-03-07 | Fixing generic equality in Auto. | Pierre-Marie Pédrot | |
| 2014-03-06 | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot | |
| 2014-03-06 | make install-coqlight installs DLLCOQRUN and LIBCOQRUN | Pierre Boutillier | |
| 2014-03-06 | Lets coqtop use a slash | Virgile Prevosto | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |