| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau | |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | |
| problem with hashconsing at the same time. This fixes bug# 3302. | |||
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot | |
| tactics. | |||
| 2014-05-08 | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | |
| (made push command with wrong local ref; leaving control to Matthieu on new revert) This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a. | |||
| 2014-05-08 | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | |
| 2014-05-08 | Typo reference manual | Hugo Herbelin | |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | |
| which compute an abstraction of the goal over a term or a pattern. | |||
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin | |
| works in the presence of local definitions referring to x and dependent in other hyps or concl. | |||
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | |
| 2014-05-08 | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin | |
| Also removing trailing spaces. | |||
| 2014-05-08 | Cleanup code in pretyping/evarutil | Matthieu Sozeau | |
| 2014-05-08 | Fix performance problem with unification in presence of universes (bug ↵ | Matthieu Sozeau | |
| #3302) by considering Type i a ground term even when "i" is a flexible universe variable, using the infer_conv function to do the unification of universes. | |||
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ↵ | Matthieu Sozeau | |
| evar_map in tactics, avoiding useless and potentially costly merge's of constraints. - Implement revert and generalize using the new tactics (not bound to syntax though, as they are not backwards-compatible yet). | |||
| 2014-05-08 | Avoid allocations in type_of_inductive | Matthieu Sozeau | |
| 2014-05-08 | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau | |
| 2014-05-08 | Adapt the checker to polymorphic universes and projections (untested). | Matthieu Sozeau | |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | |
| 2014-05-08 | Fixing test-suite for bug #3043. | Pierre-Marie Pédrot | |
| 2014-05-08 | Fixing output test-suite: since universe polymorphism, the Print command | Pierre-Marie Pédrot | |
| shows the polymorphism status of the term. | |||
| 2014-05-08 | Code cleaning in Tacinterp: factorizing some uses of tclEVARS. | Pierre-Marie Pédrot | |
| 2014-05-07 | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin | |
| answers #3299). | |||
| 2014-05-06 | Adding test-suite for bug #3242. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |