| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | |
| into a specific new cleaned file find_subterm.ml. This makes things clearer but also solves some dependencies problem between Evd, Termops and Pretype_errors. | |||
| 2014-06-28 | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin | |
| not a variable, in the future objective to factorize code between "generalize dependent" and "set", "destruct", etc. | |||
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | |
| proof engine. Moved it to unification.ml. | |||
| 2014-06-28 | Typo in stm error message. | Hugo Herbelin | |
| 2014-06-28 | Updating CHANGES w.r.t. opacity in type inference + layout of file. | Hugo Herbelin | |
| 2014-06-28 | Small short optimization of instantiation in Evd. | Hugo Herbelin | |
| 2014-06-28 | More open in base_include | Hugo Herbelin | |
| 2014-06-27 | Fast path in Canonical structure detection. We do not always compute the normal | Pierre-Marie Pédrot | |
| form of a potential canonical argument anymore, and we check that it may be part of a canonical structure first. | |||
| 2014-06-27 | Add an init_setoid check in rewrite to avoid trying to get undefined references. | Matthieu Sozeau | |
| Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded. | |||
| 2014-06-26 | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond | |
| 2014-06-26 | Avoid scanning .coq-native directories when building the library index. | Guillaume Melquiond | |
| 2014-06-26 | Fix documentation. | Guillaume Melquiond | |
| 2014-06-26 | Remove some theories that have been deprecated for 10 years. | Guillaume Melquiond | |
| 2014-06-26 | Export the right modules in Setoid, avoiding anomalies in generalized rewriting. | Matthieu Sozeau | |
| 2014-06-26 | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin | |
| incompatibilities, at least until the check of compilation of contribs succeeds more often. Incidentally adapted some proofs in Reals which were not agnostic relatively to whether the option is on or off. | |||
| 2014-06-26 | Invalid bug report. | Matthieu Sozeau | |
| 2014-06-26 | Fix bug # 3325 using canonical structure declarations where needed. | Matthieu Sozeau | |
| 2014-06-26 | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau | |
| is has non-local effects. For now it is not disabled by default, but we'll try to disable it once the test-suite and contribs are stabilized. | |||
| 2014-06-26 | Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into ↵ | Matthieu Sozeau | |
| JasonGross-tc | |||
| 2014-06-26 | Fixed bug with new semantics of change. | Matthieu Sozeau | |
| 2014-06-26 | Duplicate | Matthieu Sozeau | |
| 2014-06-26 | This has been fixed. | Matthieu Sozeau | |
| 2014-06-26 | Properly refresh the local hintdb database in case an external tactic changed | Matthieu Sozeau | |
| the hypotheses in eauto. | |||
| 2014-06-26 | Fix test-suite file, adding the proper Fail. | Matthieu Sozeau | |
| 2014-06-26 | Bug #3329 is closed. | Matthieu Sozeau | |
| 2014-06-26 | 3392 is now closed thanks to E. Tassi. | Matthieu Sozeau | |
| 2014-06-26 | Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into ↵ | Matthieu Sozeau | |
| JasonGross-more-test-suite Conflicts: test-suite/bugs/closed/3300.v test-suite/bugs/closed/3373.v | |||
| 2014-06-26 | Fix test-suite files. | Matthieu Sozeau | |
| 2014-06-26 | Bug #3301 is closed, the projection cannot be defined anymore. | Matthieu Sozeau | |
| 2014-06-26 | Fix test-suite file for opened bug #1596 | Matthieu Sozeau | |
| 2014-06-26 | Fix test-suite file for bug # 3036, the unification has _never_ succeeded, | Matthieu Sozeau | |
| as this would result in an ill-scoped substitution. | |||
| 2014-06-26 | Change interface of refresh universes to get a pbty argument instead of | Matthieu Sozeau | |
| the computed direction argument. In case pbty is conv, no refreshing is done as the evar body must be convertible with the given term, however refreshing of template application evar arguments can still happen. (Re)-Closing bug #2966. | |||
| 2014-06-26 | Add an Unset Standard... | Matthieu Sozeau | |
| 2014-06-25 | Putting implicit arguments of Clenv.res_pf right. | Pierre-Marie Pédrot | |
| 2014-06-25 | Incorrect folding of evars in let_tac_gen made remember fail to store | Matthieu Sozeau | |
| correct constraints (bug found in CFGV). | |||
| 2014-06-25 | In rewrite, wrong computation of the sort of the term to be rewritten in | Matthieu Sozeau | |
| generated an uncaught Not_found. This raises an anomaly now and the sort is properly computed now (fixes a bug in CoLoR). | |||
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi | |
| lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/ | |||
| 2014-06-25 | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi | |
| User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively. | |||
| 2014-06-25 | In exact check, use e_type_of to ensure that universe constraints necessary | Matthieu Sozeau | |
| to typecheck the term are not forgotten. (relieves tactic implementors from calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers. | |||
| 2014-06-25 | Use the right transparent state when comparing _types_ of metas. | Matthieu Sozeau | |
| 2014-06-25 | Fix type_of_inductive_knowing_conclusion, relying on an actually broken ↵ | Matthieu Sozeau | |
| univ_depends. Also add a missing constraint when generating a fresh universe for a template polymorphic inductive in that case. | |||
| 2014-06-25 | Use full transparent state when checking well-typedness of a second order ↵ | Matthieu Sozeau | |
| matching infered predicate, instead of the arguments ts which might be empty (e.g. in unification). Fixes failure in success/unification.v | |||
| 2014-06-24 | Fix computation of Type argument for Program's fix_proto. | Matthieu Sozeau | |
| 2014-06-24 | Fix program cases and inversion tactic to correctly record universe constraints. | Matthieu Sozeau | |
| Fixes FingerTree contrib. | |||
| 2014-06-24 | Force the final universe context of a proof only in poly || now case. | Matthieu Sozeau | |
| 2014-06-24 | Update some bugs about typeclass resolution | Jason Gross | |
| 2014-06-24 | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot | |
| exhibits the "useless goal" behaviour: there is code out there depending on the fact that goals cannot be solved by side effects. | |||
| 2014-06-24 | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot | |
| 2014-06-23 | Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344) | Enrico Tassi | |
| Every time you use abstract a kitten dies, please stop. | |||
| 2014-06-23 | Add some compatibility notes on the changes to [change] and unification in ↵ | Matthieu Sozeau | |
| general. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |