| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-05-06 | Add regression tests for univ. poly. and prim proj | Jason Gross | |
| These regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently passes. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one. | |||
| 2014-05-06 | Remove Lemmas from base_include, it's not linked in dev/printers anymore | Matthieu Sozeau | |
| 2014-05-06 | Cleanup before merge with the trunk | Matthieu Sozeau | |
| 2014-05-06 | Use new tactic combinators in tclABSTRACT, to avoid blowup when using ↵ | Matthieu Sozeau | |
| V82.tactic (tclEVARS _). Again, performance is back to normal. Remove reintroduced try .. with _ -> in raw_enter's. | |||
| 2014-05-06 | Add missing case for primitive projection in fold_map. | Matthieu Sozeau | |
| 2014-05-06 | Fix after merge. | Matthieu Sozeau | |
| 2014-05-06 | Add incompatibilities paragraph in doc about universe polymorphism. | Matthieu Sozeau | |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | |
| in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. - Fix a HUGE performance problem in the processing of constraints, which was remerging all the previous constraints with the ambient global universes at each new constraint addition. Performance is now back to (or better than) normal. | |||
| 2014-05-06 | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau | |
| Fix restriction of universe contexts to not forget about potentially useful constraints. | |||
| 2014-05-06 | Fix Field_tac to get fast reification again, with the fix on template ↵ | Matthieu Sozeau | |
| universe polymorphic constructors. | |||
| 2014-05-06 | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau | |
| eagerly solve l <= k constraints as k := l when k is a fresh variable coming from a template type. This has the effect of fixing the variable at the first instantiation of the parameters of template polymorphic inductive and avoiding to generate useless <= constraints that need to be minimized afterwards. | |||
| 2014-05-06 | Try a new way of handling template universe levels | Matthieu Sozeau | |
| 2014-05-06 | Print universes in module printing | Matthieu Sozeau | |
| 2014-05-06 | Fix funind w.r.t. universes | Matthieu Sozeau | |
| 2014-05-06 | Fix a pervasive equality use. | Matthieu Sozeau | |
| 2014-05-06 | Avoid u+k <= v constraints, don't take the sup of an algebraic universe during | Matthieu Sozeau | |
| minimization. | |||
| 2014-05-06 | - Add back some compatibility functions to avoid rewriting plugins. | Matthieu Sozeau | |
| - Fix in canonical structure inferce, we have to check that the heads are convertible and keep universe information around. | |||
| 2014-05-06 | Add doc on the new API for universe polymorphism and primitive projections | Matthieu Sozeau | |
| 2014-05-06 | Fix derive plugin to properly treat universes | Matthieu Sozeau | |
| 2014-05-06 | Keep track of universes on coercion applications even if they're not ↵ | Matthieu Sozeau | |
| polymorphic (fixes bug #3043). | |||
| 2014-05-06 | Comment in Funind.v test-suite file | Matthieu Sozeau | |
| 2014-05-06 | Proper calculation of constructor levels, forgetting the level of lets. | Matthieu Sozeau | |
| 2014-05-06 | Refresh some universes in cases.ml as they might appear in the term. | Matthieu Sozeau | |
| 2014-05-06 | Correct universe handling in program coercions (bug #2378). | Matthieu Sozeau | |
| 2014-05-06 | Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible. | Matthieu Sozeau | |
| 2014-05-06 | Retype application of fix_proto to get the right universes in Program | Matthieu Sozeau | |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau | |
| - Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints. (Needs to be enforced in the kernel as well, but that's the main entry point). - Fix a test-suite script and remove a regression comment, it's just as before now. | |||
| 2014-05-06 | Fix restrict_universe_context removing some universes that do appear in the ↵ | Matthieu Sozeau | |
| term. | |||
| 2014-05-06 | Fix declarations of monomorphic assumptions | Matthieu Sozeau | |
| 2014-05-06 | Allow records whose sort is defined by a constant. | Matthieu Sozeau | |
| 2014-05-06 | - Fix RecTutorial, and mutual induction schemes getting the wrong names. | Matthieu Sozeau | |
| Now the universe inconsistency appears at [exact t] instead of the Defined :) | |||
| 2014-05-06 | Fix program Fixpoint not taking care of universes. | Matthieu Sozeau | |
| 2014-05-06 | - Fixes for canonical structure resolution (check that the initial term ↵ | Matthieu Sozeau | |
| indeed unifies with the projected term, keeping track of universes). - Fix the [unify] tactic to fail properly. - Fix unification to disallow lowering a global Type(i) universe to Prop or Set. | |||
| 2014-05-06 | Fix restrict_universe_context to not remove useful constraints. | Matthieu Sozeau | |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | |
| - Fix passing of universe contexts through definitions/proofs, abstract is ok now, even in presence of polymorphism - Correctly mark unresolvable the evars made by the Simple abstraction. | |||
| 2014-05-06 | Remove postponed constraints (unused) | Matthieu Sozeau | |
| 2014-05-06 | Fixes after rebase. The use of pf_constr_of_global is problematic in ↵ | Matthieu Sozeau | |
| presence of side-effects... | |||
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | |
| - Remove Universe Polymorphism flags everywhere. - Properly infer, discharge template arities and fix substitution inside them (kernel code to check for correctness). - Fix tactics that were supposing universe polymorphic constants/inductives to be parametric on that status. Required to make interp_constr* return the whole evar universe context now. - Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing, sadly losing most of its benefits. Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting all serialization code. Conflicts: kernel/univ.ml tactics/tactics.ml theories/Logic/EqdepFacts.v | |||
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | |
| 2014-05-06 | Fix issue #88: restrict_universe_context was wrongly forgetting about ↵ | Matthieu Sozeau | |
| constraints, and keeping spurious equalities. simplify_universe_context is correct, although it might keep unused universes around (it's the responsibility of the tactics to not produce unused universes then). Add printer for future universe contexts for debugging. | |||
| 2014-05-06 | Honor the Opaque flag for projections in simpl. | Matthieu Sozeau | |
| 2014-05-06 | In case two constants/vars/rels are _not_ defined, force unification of ↵ | Matthieu Sozeau | |
| universes (better semantics for axioms, opaque constants). Conflicts: pretyping/evarconv.ml | |||
| 2014-05-06 | Fix context forgetting universes (temporary, the fix is not exactly right). | Matthieu Sozeau | |
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot | |
| A quick and dirty approach to private inductive types Types for which computable functions are provided, but pattern-matching is disallowed. This kind of type can be used to simulate simple forms of higher inductive types, with convertibility for applications of the inductive principle to 0-constructors Conflicts: intf/vernacexpr.mli kernel/declarations.ml kernel/declarations.mli kernel/entries.mli kernel/indtypes.ml library/declare.ml parsing/g_vernac.ml4 plugins/funind/glob_term_to_relation.ml pretyping/indrec.ml pretyping/tacred.mli printing/ppvernac.ml toplevel/vernacentries.ml Conflicts: kernel/declarations.mli kernel/declareops.ml kernel/indtypes.ml kernel/modops.ml | |||
| 2014-05-06 | - Fix abstract forgetting about new constraints. | Matthieu Sozeau | |
| 2014-05-06 | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau | |
| - Avoid generation of dummy universes for unsafe_global* - Handle side effects better for polymorphic definitions. Conflicts: kernel/term_typing.ml tactics/tactics.ml | |||
| 2014-05-06 | Cleanup in constr, correct classification of polymorphic defs. | Matthieu Sozeau | |
| 2014-05-06 | - Fix index-list to show computational relations for rewriting files. | Matthieu Sozeau | |
| - Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower. Conflicts: kernel/constr.ml kernel/univ.ml proofs/proof_global.ml | |||
| 2014-05-06 | Fix printing of projections with implicits. | Matthieu Sozeau | |
| 2014-05-06 | Fix inversion of notations for projections. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |