aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
| | | | observe non-normalized goals.
* Remove the -fno-defer-pop cflagGravatar Jason Gross2014-03-18
| | | | | | | | | | | | 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>
* Printing backtraces in coqchk while in debug mode.Gravatar Pierre-Marie Pédrot2014-03-18
|
* Fixing checker with respect to new kernel name structure and hashmaps.Gravatar Pierre-Marie Pédrot2014-03-18
| | | | Some wrong generic equalities and hashes were removed too.
* STM: make the slave start from the most recent known stateGravatar Enrico Tassi2014-03-18
|
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
|
* Evarconv: exact_ise_stack looks to stack head before bodies or branchesGravatar Pierre Boutillier2014-03-17
| | | | | 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 ...
* Fix test-suite 2255.vGravatar Pierre Boutillier2014-03-17
|
* consider_remaining_unif_problems respects Conv_oracleGravatar Pierre Boutillier2014-03-16
|
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
| | | | no particular purpose.
* nanoPG: better copy/pasteGravatar Enrico Tassi2014-03-13
|
* fix compilation with ocaml < 4Gravatar Enrico Tassi2014-03-13
|
* STM: perspective (tell the scheduler what the user sees)Gravatar Enrico Tassi2014-03-13
|
* Stateid: export a Set moduleGravatar Enrico Tassi2014-03-13
|
* STM: move out a couple of submodulesGravatar Enrico Tassi2014-03-13
| | | | | These modules are not as reusable as one may want them to be, but moving them out simplifies a little STM.
* fake_ide: fix compilationGravatar Enrico Tassi2014-03-12
|
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
| | | | | | | | | | | | | | | | | | | | 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.
* CoqIDE: Errors page gets red if not emptyGravatar Enrico Tassi2014-03-12
|
* CoqIDE: detachable message/error/jobs panesGravatar Enrico Tassi2014-03-12
|
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
| | | | | | | | | | | | | | | | | | 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).
* Fix (3243): univ constraints of module subtyping were not propagatedGravatar Enrico Tassi2014-03-11
| | | | | | | 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.
* Useless Array.to_list in Typeops.Gravatar Pierre-Marie Pédrot2014-03-10
|
* Evarconv unification respects Conv_oracleGravatar Pierre Boutillier2014-03-10
|
* MaybeFlexible semantic changesGravatar Pierre Boutillier2014-03-10
| | | | From Maybe reducible to Maybe to reduce (but for sure reducible)
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
|
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
|
* Also use HMaps in KNmap.Gravatar Pierre-Marie Pédrot2014-03-08
|
* Potentially unused computation in Goal.Gravatar Pierre-Marie Pédrot2014-03-07
|
* Useless tactic bindings in Tacticals.Gravatar Pierre-Marie Pédrot2014-03-07
|
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
| | | | iter order, but it seems nobody was relying on it (contrarily to the string case).
* Tentative fix for a very strange pervasive equality in Auto.Gravatar Pierre-Marie Pédrot2014-03-07
|
* Compiling coqc in "tools" target.Gravatar Pierre-Marie Pédrot2014-03-07
|
* Fix lookup of native files when option -R is missing.Gravatar Guillaume Melquiond2014-03-07
| | | | | | | | | | 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.*
* Fixing generic equality in Auto.Gravatar Pierre-Marie Pédrot2014-03-07
|
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
|
* make install-coqlight installs DLLCOQRUN and LIBCOQRUNGravatar Pierre Boutillier2014-03-06
|
* Lets coqtop use a slashGravatar Virgile Prevosto2014-03-06
|
* Uses slashes for install and config directoriesGravatar Virgile Prevosto2014-03-06
|
* remove trailing '\r' from file names returned by coqtopGravatar Virgile Prevosto2014-03-06
|
* Fix typo in comment.Gravatar Maxime Dénès2014-03-05
|
* Fixing interpretation of tactics in terms. It was forgetting part of theGravatar Pierre-Marie Pédrot2014-03-06
| | | | environment.
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Canary testing absence of generic equality for KerNamesGravatar Pierre-Marie Pédrot2014-03-05
|
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
| | | | (hopefully), and forbids generic equality. Still, it allows generic hash.
* Fixing compilation on OCaml 4.01.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Fixing previous commit. Forgot to include some code.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
| | | | | | | | | | | the provided type to come with a hashing function. The internal representation is changed, such that values are first compared w.r.t. to their hash. This effectively saves a lot of comparisons which may be far more expensive than O(1), as in the string case, hence resulting in an overall speedup. CAVEAT: everything is not implemented yet, and order-sensitive functions now do not respect the provided order anymore.
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
| | | | The removed code isn't used locally and isn't exported in the signature
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 22:54:37 +0000