| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-23 | Fixed 3233 (fresh does not work with a qualid). | Pierre Courtieu | |
| fresh now accepts a qualid, and behaves as if given the short name. Since fresh used to accept an id, supporting qualid is IMO not a new feature but just a fix. Hence the fix in v8.5. | |||
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-02-23 | Test for #3953 (subst in evar instances). | Hugo Herbelin | |
| 2015-02-23 | Fixing rewrite/subst when the subterm to rewrite is argument of an Evar. | Hugo Herbelin | |
| This was broken by the attempt to use the same algorithm for rewriting closed subterms than for rewriting subterms with evars: the algorithm to find subterms (w_unify_to_subterm) did not go through evars. But what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"? Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look in the instance? If we adopt the first approach, then, what to do when looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the instance? Is it normal that an evar behaves as a rigid constant when it cannot be unified with the pattern? | |||
| 2015-02-23 | Fixing occur-check which was too strong in unification.ml. | Hugo Herbelin | |
| 2015-02-23 | Fixing 934761875 about optimizing Import of several libraries at once ↵ | Hugo Herbelin | |
| (thanks to Enrico for noticing a bug). | |||
| 2015-02-23 | Fixing test #2830. | Pierre-Marie Pédrot | |
| 2015-02-23 | Fixing test for bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-21 | Moving test for bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-21 | Fixing bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-21 | Documenting the caveat of assumption printing in the mli. | Pierre-Marie Pédrot | |
| 2015-02-21 | Import (module): Do not force constraints if not ready (Close #4066) | Enrico Tassi | |
| 2015-02-21 | Future: human readable name for delegated (Close #4065) | Enrico Tassi | |
| 2015-02-21 | Test for bug #4078. | Pierre-Marie Pédrot | |
| 2015-02-21 | Tentative fix for bug #4078. | Pierre-Marie Pédrot | |
| 2015-02-21 | More 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-21 | Continuing experimentation on what part of the instance of an evar | Hugo 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-21 | Removing 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-21 | Better English for #4070 implicit arguments message (thanks to Jason for his ↵ | Hugo Herbelin | |
| help). | |||
| 2015-02-20 | An answer to #4070 (message for implicit arguments of inl not clear). | Hugo Herbelin | |
| 2015-02-20 | Fixing bug #4073. | Pierre-Marie Pédrot | |
| 2015-02-20 | Fixing error message when H already exists in tactic subexpression eqn:H. | Hugo Herbelin | |
| 2015-02-20 | A fix for #3993 (not fully applied term to destruct when eqn is given). | Hugo Herbelin | |
| 2015-02-19 | Adding a possible DEPRECATED flag to VERNAC EXTEND statements. | Pierre-Marie Pédrot | |
| 2015-02-19 | Record type for VERNAC EXTEND rules and a bit of documentation. | Pierre-Marie Pédrot | |
| 2015-02-19 | When 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-18 | Fix bug #3938 | Matthieu Sozeau | |
| 2015-02-18 | Fix bug #4046. | Matthieu Sozeau | |
| 2015-02-17 | Deprecated options issue a warning. | Pierre-Marie Pédrot | |
| 2015-02-17 | Remove 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-17 | Separate index for vernacular options. | Maxime Dénès | |
| 2015-02-17 | Remove documentation of non-existing Show Implicits command. | Maxime Dénès | |
| 2015-02-17 | Remove non-existing Tactic Definition command from index. | Maxime Dénès | |
| 2015-02-17 | Fix sentence that was cut in doc of Local Set. | Maxime Dénès | |
| 2015-02-17 | Fixing bug #4053. | Pierre-Marie Pédrot | |
| 2015-02-17 | Fixing bug #4023 again. | Pierre-Marie Pédrot | |
| 2015-02-17 | Tentative fix for bug #2855. | Pierre-Marie Pédrot | |
| 2015-02-17 | CoqIDE: read-only Qed sentence reflected in colors (Close: 4051) | Enrico Tassi | |
| 2015-02-16 | Remove some dead code and add test-suite file. | Matthieu Sozeau | |
| 2015-02-16 | Add test-suite file for #3960. | Matthieu Sozeau | |
| 2015-02-16 | Better comment for [type_of_global_unsafe]. | Matthieu Sozeau | |
| 2015-02-16 | Comment on the unsafe_ functions in Global. | Matthieu Sozeau | |
| 2015-02-16 | Test for bug #3922. | Pierre-Marie Pédrot | |
| 2015-02-16 | STM: when async_proofs_full is set process only tasks in the perspective | Enrico Tassi | |
| This change fixes performance problems in PIDE based user interfaces | |||
| 2015-02-16 | *Queue: API to wake up all threads | Enrico Tassi | |
| 2015-02-16 | Fix bug #3960: potential evar instance categorized as an unresolvable | Matthieu Sozeau | |
| goal in Instance. Also remove some dead code. | |||
| 2015-02-16 | Documenting "induction t in ctx" when ctx contains an hyp not mentioning t. | Hugo Herbelin | |
| 2015-02-16 | Fixing bug #4035 (support for dependent destruction within ltac code). | Hugo Herbelin | |
| 2015-02-16 | Test for #2946 (trunk bug with let's in unification). | Hugo Herbelin | |
| 2015-02-16 | Fixing test for bug #3944. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |