aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
|
* Test for #3953 (subst in evar instances).Gravatar Hugo Herbelin2015-02-23
|
* Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Gravatar Hugo Herbelin2015-02-23
| | | | | | | | | | | | 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?
* Fixing occur-check which was too strong in unification.ml.Gravatar Hugo Herbelin2015-02-23
|
* Fixing 934761875 about optimizing Import of several libraries at once ↵Gravatar Hugo Herbelin2015-02-23
| | | | (thanks to Enrico for noticing a bug).
* Fixing test #2830.Gravatar Pierre-Marie Pédrot2015-02-23
|
* Fixing test for bug #3071.Gravatar Pierre-Marie Pédrot2015-02-23
|
* Moving test for bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
|
* Fixing bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
|
* Documenting the caveat of assumption printing in the mli.Gravatar Pierre-Marie Pédrot2015-02-21
|
* Import (module): Do not force constraints if not ready (Close #4066)Gravatar Enrico Tassi2015-02-21
|
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
|
* Test for bug #4078.Gravatar Pierre-Marie Pédrot2015-02-21
|
* Tentative fix for bug #4078.Gravatar Pierre-Marie Pédrot2015-02-21
|
* More resilient implementation of Print Assumptions.Gravatar Pierre-Marie Pédrot2015-02-21
| | | | | | | | | 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.
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
| | | | | | | | | | | | | 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).
* Removing need for ensure_evar_independent by passing a force flag to ↵Gravatar Hugo Herbelin2015-02-21
| | | | is_constrainable_in to do the job of ensuring that ?p does not belong to the ti while solving ?p[...]:=?n[t1..tn].
* Better English for #4070 implicit arguments message (thanks to Jason for his ↵Gravatar Hugo Herbelin2015-02-21
| | | | help).
* An answer to #4070 (message for implicit arguments of inl not clear).Gravatar Hugo Herbelin2015-02-20
|
* Fixing bug #4073.Gravatar Pierre-Marie Pédrot2015-02-20
|
* Fixing error message when H already exists in tactic subexpression eqn:H.Gravatar Hugo Herbelin2015-02-20
|
* A fix for #3993 (not fully applied term to destruct when eqn is given).Gravatar Hugo Herbelin2015-02-20
|
* Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
|
* Record type for VERNAC EXTEND rules and a bit of documentation.Gravatar Pierre-Marie Pédrot2015-02-19
|
* When looking for restrictions in ?n=?p problems, keep the type of let-bindings.Gravatar Hugo Herbelin2015-02-19
| | | | | | | | | | | | 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.
* Fix bug #3938Gravatar Matthieu Sozeau2015-02-18
|
* Fix bug #4046.Gravatar Matthieu Sozeau2015-02-18
|
* Deprecated options issue a warning.Gravatar Pierre-Marie Pédrot2015-02-17
|
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
| | | | | | 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.
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
|
* Remove documentation of non-existing Show Implicits command.Gravatar Maxime Dénès2015-02-17
|
* Remove non-existing Tactic Definition command from index.Gravatar Maxime Dénès2015-02-17
|
* Fix sentence that was cut in doc of Local Set.Gravatar Maxime Dénès2015-02-17
|
* Fixing bug #4053.Gravatar Pierre-Marie Pédrot2015-02-17
|
* Fixing bug #4023 again.Gravatar Pierre-Marie Pédrot2015-02-17
|
* Tentative fix for bug #2855.Gravatar Pierre-Marie Pédrot2015-02-17
|
* CoqIDE: read-only Qed sentence reflected in colors (Close: 4051)Gravatar Enrico Tassi2015-02-17
|
* Remove some dead code and add test-suite file.Gravatar Matthieu Sozeau2015-02-16
|
* Add test-suite file for #3960.Gravatar Matthieu Sozeau2015-02-16
|
* Better comment for [type_of_global_unsafe].Gravatar Matthieu Sozeau2015-02-16
|
* Comment on the unsafe_ functions in Global.Gravatar Matthieu Sozeau2015-02-16
|
* Test for bug #3922.Gravatar Pierre-Marie Pédrot2015-02-16
|
* STM: when async_proofs_full is set process only tasks in the perspectiveGravatar Enrico Tassi2015-02-16
| | | | This change fixes performance problems in PIDE based user interfaces
* *Queue: API to wake up all threadsGravatar Enrico Tassi2015-02-16
|
* Fix bug #3960: potential evar instance categorized as an unresolvableGravatar Matthieu Sozeau2015-02-16
| | | | goal in Instance. Also remove some dead code.
* Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Gravatar Hugo Herbelin2015-02-16
|
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
|
* Test for #2946 (trunk bug with let's in unification).Gravatar Hugo Herbelin2015-02-16
|
* Fixing test for bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
|
* Test for bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 22:04:08 +0000