aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-05-08Fast-path equality of sorts in compare_constr*Matthieu Sozeau
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-05-08Fixing test-suite for bug #3043.Pierre-Marie Pédrot
2014-05-08Fixing output test-suite: since universe polymorphism, the Print commandPierre-Marie Pédrot
2014-05-08Code cleaning in Tacinterp: factorizing some uses of tclEVARS.Pierre-Marie Pédrot
2014-05-07Removing comment outdated since eta holds in conversion rule (thisHugo Herbelin
2014-05-06Adding test-suite for bug #3242.Pierre-Marie Pédrot
2014-05-06Add regression tests for univ. poly. and prim projJason Gross
2014-05-06Remove Lemmas from base_include, it's not linked in dev/printers anymoreMatthieu Sozeau
2014-05-06Cleanup before merge with the trunkMatthieu Sozeau
2014-05-06Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac...Matthieu Sozeau
2014-05-06Add missing case for primitive projection in fold_map.Matthieu Sozeau
2014-05-06Fix after merge.Matthieu Sozeau
2014-05-06Add incompatibilities paragraph in doc about universe polymorphism.Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Fix Field_tac to get fast reification again, with the fix on template univers...Matthieu Sozeau
2014-05-06Find a more efficient fix for dealing with template universes:Matthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06Print universes in module printingMatthieu Sozeau
2014-05-06Fix funind w.r.t. universesMatthieu Sozeau
2014-05-06Fix a pervasive equality use.Matthieu Sozeau
2014-05-06Avoid u+k <= v constraints, don't take the sup of an algebraic universe duringMatthieu Sozeau
2014-05-06- Add back some compatibility functions to avoid rewriting plugins.Matthieu Sozeau
2014-05-06Add doc on the new API for universe polymorphism and primitive projectionsMatthieu Sozeau
2014-05-06Fix derive plugin to properly treat universesMatthieu Sozeau
2014-05-06Keep track of universes on coercion applications even if they're not polymorp...Matthieu Sozeau
2014-05-06Comment in Funind.v test-suite fileMatthieu Sozeau
2014-05-06Proper calculation of constructor levels, forgetting the level of lets.Matthieu Sozeau
2014-05-06Refresh some universes in cases.ml as they might appear in the term.Matthieu Sozeau
2014-05-06Correct universe handling in program coercions (bug #2378).Matthieu Sozeau
2014-05-06Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.Matthieu Sozeau
2014-05-06Retype application of fix_proto to get the right universes in ProgramMatthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06Fix restrict_universe_context removing some universes that do appear in the t...Matthieu Sozeau
2014-05-06Fix declarations of monomorphic assumptionsMatthieu Sozeau
2014-05-06Allow 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
2014-05-06Fix program Fixpoint not taking care of universes.Matthieu Sozeau
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06Fix restrict_universe_context to not remove useful constraints.Matthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06Remove postponed constraints (unused)Matthieu Sozeau
2014-05-06Fixes after rebase. The use of pf_constr_of_global is problematic in presence...Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06Honor the Opaque flag for projections in simpl.Matthieu Sozeau
2014-05-06In case two constants/vars/rels are _not_ defined, force unification of unive...Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 08:55:00 +0000