aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-01-08Start credits for 8.5.Matthieu Sozeau
2015-01-08Small fix in whodidwhat 8.5.Pierre Courtieu
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated.
2015-01-08Fix some documentation typos.Guillaume Melquiond
2015-01-08Add a few words in whodidwhat.Maxime Dénès
2015-01-08Document native_compute.Maxime Dénès
2015-01-07Initiating who-did-what for 8.5Hugo Herbelin
2015-01-07Committing whodidwhat files.Hugo Herbelin
2015-01-07Reverting the tentative try to restore the use of second-orderHugo Herbelin
typed-based matching: it provokes a stack overflow in contrib ClassicalRealisability. To be investigated later on. (See 893a02f643858ba0b0172648e77af9ccb65f03df.)
2015-01-07Aligning printing of universe constraints.Hugo Herbelin
2015-01-07Hook when state arrives on master.Enrico Tassi
2015-01-06Fix checker's treatment of template polymorphicMatthieu Sozeau
inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ.
2015-01-06Safer version of the implementation of stores.Pierre-Marie Pédrot
2015-01-06remove unused iArrayEnrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-06Fix some documentation typos.Guillaume Melquiond
2015-01-06Fix setoid rewrite.Arnaud Spiwack
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].
2015-01-06Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵Guillaume Melquiond
#3802.)
2015-01-06updated include file for debuggingBruno Barras
2015-01-06improve efficiency of the reduction interpreter of coqtopBruno Barras
Conflicts: kernel/closure.ml kernel/closure.mli kernel/reduction.ml
2015-01-06improve efficiency of the reduction interpreter of the checkerBruno Barras
Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml
2015-01-06Fixing test for bug #2830.Pierre-Marie Pédrot
2015-01-06Rename ill-named "imports" field of safe_env into "required".Maxime Dénès
2015-01-06Propagating the relaxing of filtering started in 48509b6, fixed inHugo Herbelin
3cd718c, to the case of second_order_matching.
2015-01-06Fixing old filter bug in second_order_matching.Hugo Herbelin
2015-01-05Added more informative messages about bullets.Pierre Courtieu
Updated doc, but not tests-suite yet.
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
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.
2015-01-05In Show Universes, print universes before normalization.Matthieu Sozeau
2015-01-05Updating documentation about bullets.Pierre Courtieu
Error messages were outdated.
2015-01-05Removing GUtil dependency from ide/document.ml.Pierre-Marie Pédrot
We reimplement a quick-n-dirty Gtk-free signal handler.
2015-01-05Adding an option to deactivate the progress bar.Pierre-Marie Pédrot
2015-01-05Implementing a segment-viewer in CoqIDE.Pierre-Marie Pédrot
This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
2015-01-04STM: Make assert unneeded (Close 3898)Enrico Tassi
2015-01-04Adapting two files from test-suite to now forbidden Require's in modules.Hugo Herbelin
Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?).
2015-01-03Fixing 48509b61 which improved unification as expected but actuallyHugo Herbelin
not using the intended test. By fixing the intended test, the need for a delta-expansion resulting from this commit in PFsection6.v (line 1255) of ssreflect disappears.
2015-01-03Fixing #3896 (incorrect sigma given to printer).Hugo Herbelin
2015-01-03Tentatively trying to restore the use of second-order typed-basedHugo Herbelin
unification algorithm in consider_remaining_unif_problems. If it happens to be problematic, one can backtrack to the "optimization" from 3bd9cb26b which has a restriction on rels/vars.
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2015-01-01An optimization in the use of unification candidates so as to get theHugo Herbelin
following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
2014-12-30Document the new behavior of lazymatch.Guillaume Melquiond
2014-12-30Fixing #3892: Ensure that notation variables do not capture namesHugo Herbelin
hidden behind another notation.
2014-12-30Simplifying second_order_matching: no need to invert the linearHugo Herbelin
initial segment of the context of the evar.
2014-12-30Compatibility ocaml 3.12.Hugo Herbelin
2014-12-30more CHANGESEnrico Tassi
2014-12-30Minor fixes for the win32 installerEnrico Tassi
2014-12-29Fixing bug #3632 for good.Pierre-Marie Pédrot
2014-12-29Proof using: do not clear letins (unless they use a cleared var)Enrico Tassi
2014-12-28Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ↵Arnaud Spiwack
section variable. For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
2014-12-28Call nf_constraints also when compiling directly to voEnrico Tassi
After commit b46944e the system got way slower, hence the optimization is relevant also for non polymorphic constants. Putting it back now, but we shall find something in between: an optimization that does not clash with async proofs but that gives some performance improvement over no optimization at all.
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
As discussed on coqdev, clear is not perfect, Hints for trivial using cleared section vars are still used. But it is better than nothing I guess.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:03:07 +0000