aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Update test for #3363 now that Require is forbidden inside modules.Gravatar Maxime Dénès2015-01-12
|
* Fix a few typos.Gravatar Maxime Dénès2015-01-12
|
* Fixing name of evars in output test Notation.v.Gravatar Hugo Herbelin2015-01-12
|
* Not "Setting ?n=?p order to ?p:=?n to see if it solves someGravatar Hugo Herbelin2015-01-12
| | | | | | | incompatibilities wrt 8.4.", as it creates other problems (in Ergo and Compcert). This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.
* Fixing typo in previous commit.Gravatar Hugo Herbelin2015-01-12
|
* Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep.Gravatar Hugo Herbelin2015-01-11
|
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
|
* some credits for STMGravatar Enrico Tassi2015-01-11
|
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
|
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | After this commit, module_type_body is a particular case of module_type. For a [module_type_body], the implementation field [mod_expr] is supposed to be always [Abstract]. This is verified by coqchk, even if this isn't so crucial, since [mod_expr] is never read in the case of a module type. Concretely, this amounts to the following rewrite on field names for module_type_body: - typ_expr --> mod_type - typ_expr_alg --> mod_type_alg - typ_* --> mod_* and adding two new fields to mtb: - mod_expr (always containing Abstract) - mod_retroknowledge (always containing []) This refactoring should be completely transparent for the user. Pros: code sharing, for instance subst_modtype = subst_module. Cons: a runtime invariant (mod_expr = Abstract) which isn't enforced by typing. I tried a polymorphic typing of mod_expr, to share field names while not having mtb = mb, but the OCaml typechecker isn't clever enough with polymorphic mutual fixpoints, and reject code sharing (e.g. between subst_modtype and subst_module). In the future (with ocaml>=4), some GADT could maybe help here, but for now the current solution seems good enough.
* Extraction: discard unnecessary code inside modules without signaturesGravatar Pierre Letouzey2015-01-11
| | | | | | | In the case of an inner module without explicit signature, (and not used later in a functor application), we now extract only the needed items (used later or asked by the user), instead of blindly extracting all fields as earlier.
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
| | | | | | Since type variables are local to the definition, we simply rename them in case of unicode chars. We also get rid of any ' to avoid Ocaml illegal 'a' type var (clash with char litteral).
* Extraction : some more support functions for a future "Extraction Compute"Gravatar Pierre Letouzey2015-01-11
|
* Extraction: minor tweaks to ease ongoing experiments about LambdaGravatar Pierre Letouzey2015-01-11
| | | | | | - Common.get_native_char instead of just a pp function of this char - Enrich the record projection table
* Adding more sharing in Map.udpate and Map.modify.Gravatar Pierre-Marie Pédrot2015-01-10
|
* CHANGES: mention "Optimize (Heap|Proof)"Gravatar Enrico Tassi2015-01-10
|
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
|
* Continuing 785f82ee1 on reverting not only f5d7b2b1e but alsoGravatar Hugo Herbelin2015-01-08
| | | | | | fd98174afe6 about fixing hypothesis alpha-conversion strategy for This completion of the reverting fixes #3905.
* Fixing compilation of penultimate commit d08532d.Gravatar Hugo Herbelin2015-01-08
|
* Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ↵Gravatar Hugo Herbelin2015-01-08
| | | | 8.4.
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
|
* Update + English in CHANGESGravatar Hugo Herbelin2015-01-08
|
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
|
* Small fix in whodidwhat 8.5.Gravatar Pierre Courtieu2015-01-08
|
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
| | | | | Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated.
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-08
|
* Add a few words in whodidwhat.Gravatar Maxime Dénès2015-01-08
|
* Document native_compute.Gravatar Maxime Dénès2015-01-08
|
* Initiating who-did-what for 8.5Gravatar Hugo Herbelin2015-01-07
|
* Committing whodidwhat files.Gravatar Hugo Herbelin2015-01-07
|
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
| | | | | | typed-based matching: it provokes a stack overflow in contrib ClassicalRealisability. To be investigated later on. (See 893a02f643858ba0b0172648e77af9ccb65f03df.)
* Aligning printing of universe constraints.Gravatar Hugo Herbelin2015-01-07
|
* Hook when state arrives on master.Gravatar Enrico Tassi2015-01-07
|
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
| | | | | inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ.
* Safer version of the implementation of stores.Gravatar Pierre-Marie Pédrot2015-01-06
|
* remove unused iArrayGravatar Enrico Tassi2015-01-06
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
|
* Fix setoid rewrite.Gravatar Arnaud Spiwack2015-01-06
| | | Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false].
* Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵Gravatar Guillaume Melquiond2015-01-06
| | | | #3802.)
* updated include file for debuggingGravatar Bruno Barras2015-01-06
|
* improve efficiency of the reduction interpreter of coqtopGravatar Bruno Barras2015-01-06
| | | | | | | Conflicts: kernel/closure.ml kernel/closure.mli kernel/reduction.ml
* improve efficiency of the reduction interpreter of the checkerGravatar Bruno Barras2015-01-06
| | | | | | | Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml
* Fixing test for bug #2830.Gravatar Pierre-Marie Pédrot2015-01-06
|
* Rename ill-named "imports" field of safe_env into "required".Gravatar Maxime Dénès2015-01-06
|
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06
| | | | 3cd718c, to the case of second_order_matching.
* Fixing old filter bug in second_order_matching.Gravatar Hugo Herbelin2015-01-06
|
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
| | | | Updated doc, but not tests-suite yet.
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
| | | | | | Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:33:45 +0000