aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Now closed.Gravatar Matthieu Sozeau2015-11-11
|
* Ensure that conversion is called on terms of the same type inGravatar Matthieu Sozeau2015-11-11
| | | | unification (not necessarily preserved due to the fo approximation rule).
* Fix bug #3998: when using typeclass resolution for conversion, allowGravatar Matthieu Sozeau2015-11-11
| | | | only one disjoint component of the typeclasses instances to resolve.
* Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
|
* Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
|
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
| | | | their type annotation.
* Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
| | | | | | | We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time.
* Dead code from the commit having introduced primitive projections (a4043608).Gravatar Hugo Herbelin2015-11-10
|
* Typo.Gravatar Hugo Herbelin2015-11-10
|
* Fixing a bug in reporting ill-formed constructor.Gravatar Hugo Herbelin2015-11-10
| | | | | | | | | | | | | | For instance, Inductive a (x:=1) := C : a -> True. was wrongly reporting Error: The type of constructor C is not valid; its conclusion must be "a" applied to its parameter. Also "simplifying" explain_ind_err.
* Test for bug #4404.Gravatar Pierre-Marie Pédrot2015-11-10
|
* Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Gravatar Pierre-Marie Pédrot2015-11-10
|
* Pushing the backtrace in conversion anomalies.Gravatar Pierre-Marie Pédrot2015-11-09
|
* Fixing output test Existentials.v after eec77191b.Gravatar Hugo Herbelin2015-11-07
|
* Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Gravatar Hugo Herbelin2015-11-07
| | | | | | | | | | | | | | | | | | | | | For pose/set/clearbody, I think it is clear that we want to preserve the name and this commit do it. For revert, I first did not preserve the name, then considered in 2ba2ca96be88 that it was better to preserve it. For intro, like for revert actually, I did not preserve the name, based on the idea that the type was changing (*). For instance if we have ?f:nat->nat, do we really want to keep the name f in ?f:nat after an intro. For revert, I changed my mind based on the idea that if we had a better control of the name if we keep the name that if the system invents a new one based on the type. I think this is more reasonable than (*), so this commit preserves the name for intro. For generalize, it is still not done because of generalize being in the old proof engine.
* Tests for syntax "Show id" and [id]:tac (shelved or not).Gravatar Hugo Herbelin2015-11-07
|
* Fixing documention of Add Printing Coercion.Gravatar Hugo Herbelin2015-11-07
|
* Fixed #4407.Gravatar Pierre Courtieu2015-11-06
| | | | | | | Like coqc: detect if the current directory was set by options, if not: add it with empty logical path. TODO: check if coq_makefile is still correct wrt to this modification, I think yes, actually it should end being more correct.
* Fixing #4406 coqdep: No recursive search of ml (-I).Gravatar Pierre Courtieu2015-11-06
|
* Fixing complexity file f_equal.v.Gravatar Hugo Herbelin2015-11-06
|
* More on how to compile doc.Gravatar Hugo Herbelin2015-11-06
|
* Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
| | | | | | | for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise.
* Add test-suite file for #4273.Gravatar Matthieu Sozeau2015-11-05
|
* Fix bug #4273Gravatar Matthieu Sozeau2015-11-05
| | | | | | Syntactic analysis of dependencies when atomizing arguments in destruct was not dealing properly with primitive projections hiding their parameters.
* Update version numbers and magic numbers for 8.5beta3 release.Gravatar Maxime Dénès2015-11-05
|
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
| | | | proofs.
* Univs: missing checks in evarsolve with candidates and missing aGravatar Matthieu Sozeau2015-11-04
| | | | whd_evar in refresh_universes.
* Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
|
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
| | | | inconsistent).
* Univs: compatibility with 8.4.Gravatar Matthieu Sozeau2015-11-04
| | | | | When refreshing a type variable, always use a rigid universe to force the most general universe constraint, as in 8.4.
* Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
| | | | is buggy in general.
* Test file for #4397.Gravatar Maxime Dénès2015-11-04
|
* Update compatibility file for some of bug #4392Gravatar Jason Gross2015-11-03
| | | | | | | | | | | | | Now doing ```coq Tactic Notation "left" "~" := left. Tactic Notation "left" "*" := left. ``` will no longer break the `left` tactic in Coq 8.4. List obtained via ``` grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g' ```
* Fix bug #4397: refreshing types in abstract_generalize.Gravatar Matthieu Sozeau2015-11-02
|
* Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
|
* Refresh rigid universes as well, and in 8.4 compatibility mode,Gravatar Matthieu Sozeau2015-11-02
| | | | make them rigid to disallow minimization.
* Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Gravatar Maxime Dénès2015-11-02
|
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
|
* Made that the syntax [id]:tac also applies to the shelve, which is after all ↵Gravatar Hugo Herbelin2015-11-02
| | | | its main interest!
* STM: fix undo into a branch containing side effectsGravatar Enrico Tassi2015-11-02
| | | | The "master" label used to be reset to the wrong id
* STM: never reopen a branch containing side effectsGravatar Enrico Tassi2015-11-02
|
* Command.declare_definition: grab the fix_exn early (follows 77cf18e)Gravatar Enrico Tassi2015-10-30
| | | | | | | | | When a future is fully forced (joined), the fix_exn is dropped, since joined futures are values (hence they cannot raise exceptions). When a future for a transparent definition enters the environment it is joined. If one needs to pick its fix_exn, he should do it before that.
* Manually expand red_tactic so that notations do not break reduction tactics. ↵Gravatar Guillaume Melquiond2015-10-30
| | | | (Fix bug #3654)
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
| | | | involving Futures.
* Fix typo.Gravatar Guillaume Melquiond2015-10-30
|
* Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
| | | | universes are declared correctly in the enclosing proofs evar_map's.
* Collect subproof universes in handle_side_effects.Gravatar Matthieu Sozeau2015-10-29
|
* Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Gravatar Guillaume Melquiond2015-10-29
| | | | | Without this expansion, camlp4 fails to properly factor a user notation starting with either "trivial" or "auto".
* Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)Gravatar Guillaume Melquiond2015-10-29
| | | | | It is too bad that OCaml does not warn when catching an exception over a closure rather than inside it.
* Fixing another instance of bug #3267 in eauto, this time in theGravatar Hugo Herbelin2015-10-29
| | | | | | presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 16:30:05 +0000