aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| * windows build scripts made more accurate in detecting failuresGravatar Enrico Tassi2015-08-17
| |
| * Remove duplicate code.Gravatar Guillaume Melquiond2015-08-17
| |
| * Remove generatable documentation files from repository. (Fix bug #4315)Gravatar Guillaume Melquiond2015-08-17
| |
* | Using the new preference mechanism for colors in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-16
| | | | | | | | | | A lot of legacy code has been removed in the process in favour of signal-based interactions.
* | Taking advantage of the new type of preferences.Gravatar Pierre-Marie Pédrot2015-08-16
| | | | | | | | | | | | | | | | | | We use uniform functions instead of code duplication. Likewise, we disentangle the hook mechanisms by using callbacks connected to preferences instead. Only the easy hook bits were removed. The most awing one, the editor refreshing hook, is still alive.
* | Turning CoqIDE preferences into new style.Gravatar Pierre-Marie Pédrot2015-08-16
| | | | | | | | | | Some old style references remain because all type converters are not implemented yet.
* | Simplifying CoqIDE preferences mechanism.Gravatar Pierre-Marie Pédrot2015-08-16
| | | | | | | | | | | | | | We use a class-based system instead of the old record-based system. This allows for more uniformity and the possibility to define complex interactions with preferences based on GTK signals. This will allow to simplify some architectural choices.
| * Revert the four previous commits and update the description of Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
| | | | | | | | | | Correcting the code w.r.t. to the API was not the right solution. Instead, the API comment had to be corrected.
| * More invariants in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
| | | | | | | | | | | | We ensure statically by typing that the tags used by the rich printer are integers. Furthermore, we also expose through typing that tags are irrelevants in the returned XML.
| * More parametric type for generalized XML.Gravatar Pierre-Marie Pédrot2015-08-15
| |
| * Statically ensure that we omit null annotations in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
| |
| * Fixing richpp behaviour w.r.t. its specification.Gravatar Pierre-Marie Pédrot2015-08-15
| | | | | | | | | | Contrarily to what was described in the API, nodes without annotations were not ignored by the printer but left there instead.
| * report the full module path when reporting errors in coqdepGravatar Gregory Malecha2015-08-13
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * Test file for #4254: Mutual inductives with parameters on Type raises anomaly.Gravatar Maxime Dénès2015-08-03
| |
| * Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
| | | | | | | | of syntax in test file ltac.v.
| * Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
| |
| * Fixing pop_rel_context.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | This is necessary for the patch for #4221 (817308ab5) to work.
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
| * Hconsing continuedGravatar Hugo Herbelin2015-08-02
| |
| * Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
| |
| * Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
| |
| * Documenting in passing.Gravatar Hugo Herbelin2015-08-02
| |
| * Hopefully clearer printing of stack when debugging evarconv unification.Gravatar Hugo Herbelin2015-08-02
| |
| * Failing when reaching end of file with unterminated comment whenGravatar Hugo Herbelin2015-08-02
| | | | | | | | parsing Make (project) file.
| * Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
| | | | | | | | of arguments of eta_constructor.
| * Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
| | | | | | | | naming of arguments of eta.
| * Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
| |
| * Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
| |
| * Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
| |
| * Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
| |
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same.
| * Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | in 8.4 with the schemes of the subcomponent of an inductive added to the environment or discharged as let-ins over the main scheme. As of today, decidable-equality schemes are built when calling vernacular command (Inductive with option Set Dedicable Equality Schemes, or Scheme Equality), so there is no need to discharge the sub-schemes as let-ins. But if ever the schemes are built from within an opaque proof and one would not like the schemes and a fortiori the subschemes to appear in the env, the new addition of a parameter internal_flag to "find_scheme" allows this possibility (then to be set to KernelSilent).
| * Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | Auto_ind_decl over the internal lemmas. The schemes are built in the main process and the internal lemmas are actually already also in the environment.
| * Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | capturing bound names unexpectingly). We moved renaming to after finding bindings, i.e. in pretyping "fun x y => x + y" in an ltac environment where y is ltac-bound to x, we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1" (which later on is displayed into "fun y y0 => y + y0"). We renounced to renaming in "match" patterns, which was anyway not working well, as e.g. in let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0). which was producing forall z : nat, match z with 0 => z | S y => y end = 0 because the names in default branches are treated specifically. It would be easy to support renaming in match again, by putting the ltac env in the Cases.pattern_matching_problem state and to rename the names in "typs" (from build_branch), just before returning them at the end of the function (and similarly in abstract_predicate for the names occurring in the return predicate). However, we rename binders in fix which were not interpreted. There are some difficulties with evar because we want them defined in the interpreted env (see comment to ltac_interp_name_env). fix ltac name
| * Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v.
| * Documenting change of behavior of apply when the lemma is a tuple andGravatar Hugo Herbelin2015-08-02
| | | | | | | | applying a component of the tuple.
| * For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | command line. Documenting only the former for simplicity and uniformity with predating option -with-geoproof.
| * Fix typos in the Extraction part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
| | | | | | | | In particular, fix the name of all the user contributions.
| * Fix typos in the Micromega part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
| |
| * Improve the table of content of the reference manual.Gravatar Guillaume Melquiond2015-07-31
| | | | | | | | | | Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts.
| * Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
| |
| * Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
| | | | | | | | | | | | The hash function exported by the interface ought to respect the equality. Therefore, we only use the syntactic hash for the hashconsing module while using the canonical hash in the API.
| * STM: make multiple, admitted, nested proofs work (fix #4314)Gravatar Enrico Tassi2015-07-30
| |
| * STM: emit a warning when a QED/Admitted proof contains a nested lemmaGravatar Enrico Tassi2015-07-30
| |
| * STM: fix backtrack in presence of nested, immediate, proofsGravatar Enrico Tassi2015-07-30
| |
| * STM: remove assertion not being true for nested, immediate, proofs (#4313)Gravatar Enrico Tassi2015-07-30
| |
| * Test file for bug #4289 (buggy hash-consing of kernel name pairsGravatar Hugo Herbelin2015-07-30
| | | | | | | | | | | | breaking backtracking in the presence of functors). In "interactive" rather than "bugs" because of the use of Back.
| * Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
| | | | | | | | | | | | | | | | | | | | | | compatible with a unique bound module name counter which is not synchronous with the backtracking). We changed hash-consing of kernel name pairs to a purely memory management issue, not trying to exploit logical properties such as "syntactically equal user names have syntactically same canonical names" (which is true in a given logical session, but not in memory, at least because of residual values after backtracking).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 02:30:57 +0000