aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-21Moving test for bug #3071.Pierre-Marie Pédrot
2015-02-21Fixing bug #3071.Pierre-Marie Pédrot
2015-02-21Documenting the caveat of assumption printing in the mli.Pierre-Marie Pédrot
2015-02-21Import (module): Do not force constraints if not ready (Close #4066)Enrico Tassi
2015-02-21Future: human readable name for delegated (Close #4065)Enrico Tassi
2015-02-21Test for bug #4078.Pierre-Marie Pédrot
2015-02-21Tentative fix for bug #4078.Pierre-Marie Pédrot
2015-02-21More resilient implementation of Print Assumptions.Pierre-Marie Pédrot
Instead of registering all the transitive dependencies of a term in one go, we rather recursively build the graph of direct dependencies of this term. This is finer-grained and offers a better API. The traversal now uses the standard term fold operation, and also registers inductives and constructors encountered in the traversal.
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
to display by default (see bc8a5357889 - 17 Oct 2014): - not printing instances for let-in anymore even when expanded (since they are canonical up to conversion) - still printing x:=x in [x:=x;x':=x] when x is directly an instance of another var, but not in [x:=x;x':=S x] This can be discussed, but if ever this is to be changed, it should not be printed in [x:=x;x:=?n] with ?n implicitly depending on x (otherwise said, variables which are not displayed in instances of internal evars should not contribute to the decision of writing x:=x in the instance).
2015-02-21Removing need for ensure_evar_independent by passing a force flag to ↵Hugo Herbelin
is_constrainable_in to do the job of ensuring that ?p does not belong to the ti while solving ?p[...]:=?n[t1..tn].
2015-02-21Better English for #4070 implicit arguments message (thanks to Jason for his ↵Hugo Herbelin
help).
2015-02-21Removed tests for #3900 and #3944 as open bugs.Hugo Herbelin
2015-02-20An answer to #4070 (message for implicit arguments of inl not clear).Hugo Herbelin
2015-02-20Fixing bug #4073.Pierre-Marie Pédrot
2015-02-20Fixing error message when H already exists in tactic subexpression eqn:H.Hugo Herbelin
2015-02-20A fix for #3993 (not fully applied term to destruct when eqn is given).Hugo Herbelin
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-19Record type for VERNAC EXTEND rules and a bit of documentation.Pierre-Marie Pédrot
2015-02-19When looking for restrictions in ?n=?p problems, keep the type of let-bindings.Hugo Herbelin
Bindings of the form [let x:T := M] are unfolded into [(M:T)], so that occur-check is done in [T] as well as in [M] (except when [M] is a variable, where it is hopefully not necessary). This is a way to fix #4062 (evars with type depending on themselves). The fix modifies the alias map (make_alias_map) but it should behave the same at all places using alias maps other than has_constrainable_free_vars.
2015-02-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-18Fix bug #3938Matthieu Sozeau
2015-02-18Fix bug #4046.Matthieu Sozeau
2015-02-17Deprecated options issue a warning.Pierre-Marie Pédrot
2015-02-17Remove Whelp commands.Maxime Dénès
Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-17Remove documentation of non-existing Show Implicits command.Maxime Dénès
2015-02-17Remove non-existing Tactic Definition command from index.Maxime Dénès
2015-02-17Fix sentence that was cut in doc of Local Set.Maxime Dénès
2015-02-17Fixing bug #4053.Pierre-Marie Pédrot
2015-02-17Fixing bug #4023 again.Pierre-Marie Pédrot
2015-02-17Tentative fix for bug #2855.Pierre-Marie Pédrot
2015-02-17CoqIDE: read-only Qed sentence reflected in colors (Close: 4051)Enrico Tassi
2015-02-16Remove some dead code and add test-suite file.Matthieu Sozeau
2015-02-16Add test-suite file for #3960.Matthieu Sozeau
2015-02-16Better comment for [type_of_global_unsafe].Matthieu Sozeau
2015-02-16Comment on the unsafe_ functions in Global.Matthieu Sozeau
2015-02-16Test for bug #3922.Pierre-Marie Pédrot
2015-02-16STM: when async_proofs_full is set process only tasks in the perspectiveEnrico Tassi
This change fixes performance problems in PIDE based user interfaces
2015-02-16*Queue: API to wake up all threadsEnrico Tassi
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
goal in Instance. Also remove some dead code.
2015-02-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise.
2015-02-16Using home-made ocamllibdep rather than coqdep_boot.Hugo Herbelin
2015-02-16New short stand-alone ocamllibdep to build .mllib dependencies files.Hugo Herbelin
2015-02-16Restricting the need for coqdep_boot to mllib.d files (since ocamlHugo Herbelin
3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d is the only feature that coqdep_boot was still required for).
2015-02-16Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Hugo Herbelin
2015-02-16Fixing bug #4035 (support for dependent destruction within ltac code).Hugo Herbelin
2015-02-16Test for #2946 (trunk bug with let's in unification).Hugo Herbelin
2015-02-16Fixing test for bug #3944.Pierre-Marie Pédrot
2015-02-16Test for bug #3944.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 00:01:32 +0000