| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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. | |||
| 2014-06-23 | Fix for bug 1951, allowing at least fully-applied inductives types to be used | Matthieu Sozeau | |
| for building polymorphic instances of template polymorphic inductives. | |||
| 2014-06-23 | Fix test-suite script for subst working with let-ins, the following proof ↵ | Matthieu Sozeau | |
| was rightly failing. | |||
| 2014-06-23 | Changed syntax of explicit universes. | Matthieu Sozeau | |
| 2014-06-23 | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot | |
| 2014-06-23 | Removing opens to Clenvtac to track its use more easily. | Pierre-Marie Pédrot | |
| 2014-06-23 | Oops, I fixed the .ml's | Matthieu Sozeau | |
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence ↵ | Matthieu Sozeau | |
| of p, avoiding unwanted universe constraints in presence of universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113. | |||
| 2014-06-23 | Proper handling of the polymorphism flag for Context, fixing HoTT bug #98. | Matthieu Sozeau | |
| 2014-06-23 | The uses of the funext axiom forced levels to Set, relaxing its use doesn't. | Matthieu Sozeau | |
| 2014-06-23 | The test-suite file couldn't typecheck as it rightly introduces a universe ↵ | Matthieu Sozeau | |
| inconsistency. One needs to use a universe level lower than eq's parameter for this to be consistent. | |||
| 2014-06-23 | Fix test-suite script for HoTT coq bug #34 | Matthieu Sozeau | |
| 2014-06-22 | Less goal-entering. | Pierre-Marie Pédrot | |
| 2014-06-21 | Fixing grammar in doc of Opaque as proposed by Jason (#3389). | Hugo Herbelin | |
| 2014-06-21 | Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault). | Hugo Herbelin | |
| 2014-06-21 | Less ocaml warnings. | Hugo Herbelin | |
| 2014-06-21 | - Add an option to refresh only algebraic universes, for e_type_of. The goal | Matthieu Sozeau | |
| there is not the same as in Evd.define. - Fixed bugs #3330 and #3331. | |||
| 2014-06-21 | When discharging polymorphic definitions, we must take into account all | Matthieu Sozeau | |
| polymorphic variables of the section as they might incur universe constraints that were used to typecheck the body of the definition, even if the variable itself was not used. For "Monomorphic" variables, their constraints are already always pushed to the global context. This fixes bug # 3330. | |||
| 2014-06-21 | Reindex section variables for typeclass resolution if their type changed. | Matthieu Sozeau | |
| Fixes bug #3331. | |||
| 2014-06-20 | Fixed bug 3332. | Matthieu Sozeau | |
| 2014-06-20 | Allow more relaxed conversion between the types of the two terms of a rewrite | Matthieu Sozeau | |
| equation, fix uncaught exception in setoid_rewrite (bug #3336). | |||
| 2014-06-20 | Add fixed test-suite file for 3373. | Matthieu Sozeau | |
| 2014-06-20 | Fix computation of inductive level in monomorphism + indices-matter mode. | Matthieu Sozeau | |
| Fixes bug #3346. | |||
| 2014-06-20 | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau | |
| universe instance. | |||
| 2014-06-20 | Bug 27 closed now that universe contexts can be refined during the proof, | Matthieu Sozeau | |
| here instantiating a flexible level with Set. | |||
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau | |
| for helping fixing this). Now the issue is handled solely through refreshing of the terms assigned to evars during unification. If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention a template universe and in turn, ?X won't. Same goes when typechecking (nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh universes for the lists carriers. This also handles user-defined functions on template polymorphic inductives, which was fragile before. Pretyping and Evd are now uncluttered from template-specific code. | |||
| 2014-06-20 | Add an e_type_of to avoid losing universe constraints. | Matthieu Sozeau | |
| 2014-06-19 | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot | |
| 2014-06-19 | - Fix bug in unification, not only named metas are turned into evars (e.g. ↵ | Matthieu Sozeau | |
| in Ssreflect). - Fix is_applied_rewrite_relation to look for propositional relations. | |||
| 2014-06-19 | HoTT coq bug #62 fixed. | Matthieu Sozeau | |
| 2014-06-19 | Support dropping files over the coqide window. (Partial fix for bug #2765) | Guillaume Melquiond | |
| The fix is only partial, because dropping files only works over the menu bar, the icon bar, the status bar, and so on. Editable boxes, such as the script widget, catch dnd events, hence preventing this code from working for these drop targets. Some (labl)gtk expert should be able to sort it out. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |