| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-18 | Code factorization in LMap. | Pierre-Marie Pédrot | |
| 2014-06-17 | Dummy commit to test the new setup of coq-commits mailinglist (bis) | Pierre Letouzey | |
| 2014-06-17 | Dummy commit to test the new setup of coq-commits mailinglist | Pierre Letouzey | |
| 2014-06-17 | Fix a destArity that does not exactly match isArity in presence of let-ins. | Matthieu Sozeau | |
| 2014-06-17 | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau | |
| 2014-06-17 | Not a bug, keep for backwards compatibility | Matthieu Sozeau | |
| 2014-06-17 | Bug closed, now in polymorphic mode, Variables A B : Type give different ↵ | Matthieu Sozeau | |
| levels to A and B. | |||
| 2014-06-17 | Explicit universes allow to write liftings explicitely. Implicit lifting ↵ | Matthieu Sozeau | |
| would change the theory non-trivially. | |||
| 2014-06-17 | Not considering test-suite file #89 as a bug anymore. | Matthieu Sozeau | |
| 2014-06-17 | Continue fix on argument scopes of primitive projections. | Matthieu Sozeau | |
| 2014-06-17 | Fix HoTT bug #84, binding scopes to projections. | Matthieu Sozeau | |
| 2014-06-17 | HoTT coq bug #82 already fixed. | Matthieu Sozeau | |
| 2014-06-17 | Adapt coercion code to work with projections as target classes. | Matthieu Sozeau | |
| 2014-06-17 | Tentative optimization not to nf_evar too often in the compatibility | Pierre-Marie Pédrot | |
| layer. To this intent, we add a cache evar_map in goals that is the latest known one where the goal is nf-evarized. If the current one and the cache coincide, we leave the goal as-is. | |||
| 2014-06-17 | Fixing #3292 (locations of notations shifted by 1 in glob files in trunk). | Hugo Herbelin | |
| Thanks to David M. Cooke on coq-bugs for pointing out one part of the problem. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |