From f41af657b779c7593b0c659a51afd11978b4163a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 6 Sep 2024 21:59:55 -0700 Subject: [PATCH] ulib: move hints to separate directory This makes git summaries much more readable --- .../{.cache => .hints}/FStar.Algebra.CommMonoid.Equiv.fst.hints | 0 .../FStar.Algebra.CommMonoid.Fold.Nested.fst.hints | 0 .../FStar.Algebra.CommMonoid.Fold.Nested.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.Fold.fst.hints | 0 .../{.cache => .hints}/FStar.Algebra.CommMonoid.Fold.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.fst.hints | 0 ulib/{.cache => .hints}/FStar.Algebra.Monoid.fst.hints | 0 ulib/{.cache => .hints}/FStar.All.fst.hints | 0 ulib/{.cache => .hints}/FStar.Array.fst.hints | 0 ulib/{.cache => .hints}/FStar.Array.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Axiomatic.Array.fst.hints | 0 ulib/{.cache => .hints}/FStar.BV.fst.hints | 0 ulib/{.cache => .hints}/FStar.BV.fsti.hints | 0 ulib/{.cache => .hints}/FStar.BaseTypes.fsti.hints | 0 ulib/{.cache => .hints}/FStar.BigOps.fst.hints | 0 ulib/{.cache => .hints}/FStar.BigOps.fsti.hints | 0 ulib/{.cache => .hints}/FStar.BitVector.fst.hints | 0 ulib/{.cache => .hints}/FStar.Buffer.Quantifiers.fst.hints | 0 ulib/{.cache => .hints}/FStar.Buffer.fst.hints | 0 ulib/{.cache => .hints}/FStar.BufferNG.fst.hints | 0 ulib/{.cache => .hints}/FStar.Bytes.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Calc.fst.hints | 0 ulib/{.cache => .hints}/FStar.Calc.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Cardinality.Cantor.fst.hints | 0 ulib/{.cache => .hints}/FStar.Cardinality.Cantor.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Cardinality.Universes.fst.hints | 0 ulib/{.cache => .hints}/FStar.Cardinality.Universes.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Char.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Class.Add.fst.hints | 0 ulib/{.cache => .hints}/FStar.Class.Embeddable.fst.hints | 0 ulib/{.cache => .hints}/FStar.Class.Embeddable.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Class.Eq.Raw.fst.hints | 0 ulib/{.cache => .hints}/FStar.Class.Eq.fst.hints | 0 ulib/{.cache => .hints}/FStar.Class.Printable.fst.hints | 0 ulib/{.cache => .hints}/FStar.Class.TotalOrder.Raw.fst.hints | 0 ulib/{.cache => .hints}/FStar.Classical.Sugar.fst.hints | 0 ulib/{.cache => .hints}/FStar.Classical.Sugar.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Classical.fst.hints | 0 ulib/{.cache => .hints}/FStar.Classical.fsti.hints | 0 ulib/{.cache => .hints}/FStar.ConstantTime.Integers.fst.hints | 0 ulib/{.cache => .hints}/FStar.ConstantTime.Integers.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Constructive.fst.hints | 0 ulib/{.cache => .hints}/FStar.Crypto.fst.hints | 0 ulib/{.cache => .hints}/FStar.Date.fsti.hints | 0 ulib/{.cache => .hints}/FStar.DependentMap.fst.hints | 0 ulib/{.cache => .hints}/FStar.DependentMap.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Dyn.fst.hints | 0 ulib/{.cache => .hints}/FStar.Dyn.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Endianness.fst.hints | 0 ulib/{.cache => .hints}/FStar.Endianness.fsti.hints | 0 ulib/{.cache => .hints}/FStar.ErasedLogic.fst.hints | 0 ulib/{.cache => .hints}/FStar.Error.fst.hints | 0 ulib/{.cache => .hints}/FStar.Exn.fst.hints | 0 ulib/{.cache => .hints}/FStar.Fin.fst.hints | 0 ulib/{.cache => .hints}/FStar.Fin.fsti.hints | 0 ulib/{.cache => .hints}/FStar.FiniteMap.Ambient.fst.hints | 0 ulib/{.cache => .hints}/FStar.FiniteMap.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.FiniteMap.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.FiniteSet.Ambient.fst.hints | 0 ulib/{.cache => .hints}/FStar.FiniteSet.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.FiniteSet.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Float.fsti.hints | 0 .../{.cache => .hints}/FStar.FunctionalExtensionality.fst.hints | 0 .../FStar.FunctionalExtensionality.fsti.hints | 0 ulib/{.cache => .hints}/FStar.FunctionalQueue.fst.hints | 0 ulib/{.cache => .hints}/FStar.FunctionalQueue.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Functions.fst.hints | 0 ulib/{.cache => .hints}/FStar.Functions.fsti.hints | 0 ulib/{.cache => .hints}/FStar.GSet.fst.hints | 0 ulib/{.cache => .hints}/FStar.GSet.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Ghost.Pull.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Ghost.fst.hints | 0 ulib/{.cache => .hints}/FStar.Ghost.fsti.hints | 0 ulib/{.cache => .hints}/FStar.GhostSet.fst.hints | 0 ulib/{.cache => .hints}/FStar.GhostSet.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Heap.fst.hints | 0 ulib/{.cache => .hints}/FStar.HyperStack.All.fst.hints | 0 ulib/{.cache => .hints}/FStar.HyperStack.IO.fst.hints | 0 ulib/{.cache => .hints}/FStar.HyperStack.ST.fst.hints | 0 ulib/{.cache => .hints}/FStar.HyperStack.ST.fsti.hints | 0 ulib/{.cache => .hints}/FStar.HyperStack.fst.hints | 0 ulib/{.cache => .hints}/FStar.IFC.fst.hints | 0 ulib/{.cache => .hints}/FStar.IFC.fsti.hints | 0 ulib/{.cache => .hints}/FStar.IO.fst.hints | 0 ulib/{.cache => .hints}/FStar.ImmutableArray.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.ImmutableArray.fsti.hints | 0 ulib/{.cache => .hints}/FStar.IndefiniteDescription.fst.hints | 0 ulib/{.cache => .hints}/FStar.IndefiniteDescription.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Int.Cast.Full.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int.Cast.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Int128.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int128.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Int16.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int16.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Int32.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int32.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Int64.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int64.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Int8.fst.hints | 0 ulib/{.cache => .hints}/FStar.Int8.fsti.hints | 0 ulib/{.cache => .hints}/FStar.IntegerIntervals.fst.hints | 0 ulib/{.cache => .hints}/FStar.Integers.fst.hints | 0 ulib/{.cache => .hints}/FStar.InteractiveHelpers.Base.fst.hints | 0 .../FStar.InteractiveHelpers.Effectful.fst.hints | 0 .../FStar.InteractiveHelpers.ExploreTerm.fst.hints | 0 .../FStar.InteractiveHelpers.Output.fst.hints | 0 .../FStar.InteractiveHelpers.PostProcess.fst.hints | 0 .../FStar.InteractiveHelpers.Propositions.fst.hints | 0 ulib/{.cache => .hints}/FStar.InteractiveHelpers.fst.hints | 0 ulib/{.cache => .hints}/FStar.Issue.fsti.hints | 0 ulib/{.cache => .hints}/FStar.LexicographicOrdering.fst.hints | 0 ulib/{.cache => .hints}/FStar.LexicographicOrdering.fsti.hints | 0 ulib/{.cache => .hints}/FStar.List.Pure.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.List.Pure.Properties.fst.hints | 0 ulib/{.cache => .hints}/FStar.List.Pure.fst.hints | 0 ulib/{.cache => .hints}/FStar.List.Tot.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.List.Tot.Properties.fst.hints | 0 ulib/{.cache => .hints}/FStar.List.Tot.fst.hints | 0 ulib/{.cache => .hints}/FStar.List.fst.hints | 0 ulib/{.cache => .hints}/FStar.MRef.fst.hints | 0 ulib/{.cache => .hints}/FStar.MRef.fsti.hints | 0 ulib/{.cache => .hints}/FStar.MST.fst.hints | 0 ulib/{.cache => .hints}/FStar.MSTTotal.fst.hints | 0 ulib/{.cache => .hints}/FStar.Map.fst.hints | 0 ulib/{.cache => .hints}/FStar.Map.fsti.hints | 0 ulib/{.cache => .hints}/FStar.MarkovsPrinciple.fst.hints | 0 ulib/{.cache => .hints}/FStar.Math.Euclid.fst.hints | 0 ulib/{.cache => .hints}/FStar.Math.Euclid.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Math.Fermat.fst.hints | 0 ulib/{.cache => .hints}/FStar.Math.Fermat.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Math.Lemmas.fst.hints | 0 ulib/{.cache => .hints}/FStar.Math.Lemmas.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Math.Lib.fst.hints | 0 ulib/{.cache => .hints}/FStar.Matrix.fst.hints | 0 ulib/{.cache => .hints}/FStar.Matrix.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Matrix2.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Modifies.fst.hints | 0 ulib/{.cache => .hints}/FStar.Modifies.fsti.hints | 0 ulib/{.cache => .hints}/FStar.ModifiesGen.fst.hints | 0 ulib/{.cache => .hints}/FStar.ModifiesGen.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.DependentMap.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.DependentMap.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Heap.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Heap.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.HyperHeap.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.HyperHeap.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.HyperStack.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.HyperStack.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Map.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Pure.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Seq.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Witnessed.fst.hints | 0 ulib/{.cache => .hints}/FStar.Monotonic.Witnessed.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Mul.fst.hints | 0 ulib/{.cache => .hints}/FStar.NMST.fst.hints | 0 ulib/{.cache => .hints}/FStar.NMSTTotal.fst.hints | 0 ulib/{.cache => .hints}/FStar.Option.fst.hints | 0 ulib/{.cache => .hints}/FStar.OrdMap.fst.hints | 0 ulib/{.cache => .hints}/FStar.OrdMap.fsti.hints | 0 ulib/{.cache => .hints}/FStar.OrdMapProps.fst.hints | 0 ulib/{.cache => .hints}/FStar.OrdSet.fst.hints | 0 ulib/{.cache => .hints}/FStar.OrdSet.fsti.hints | 0 ulib/{.cache => .hints}/FStar.OrdSetProps.fst.hints | 0 ulib/{.cache => .hints}/FStar.Order.fst.hints | 0 ulib/{.cache => .hints}/FStar.PCM.fst.hints | 0 ulib/{.cache => .hints}/FStar.Parse.fst.hints | 0 ulib/{.cache => .hints}/FStar.PartialMap.fst.hints | 0 ulib/{.cache => .hints}/FStar.PartialMap.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pervasives.Native.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pervasives.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pervasives.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Derived1.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Derived1.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Derived2.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Derived2.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Derived3.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.Derived3.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pointer.fst.hints | 0 ulib/{.cache => .hints}/FStar.PredicateExtensionality.fst.hints | 0 ulib/{.cache => .hints}/FStar.Preorder.fst.hints | 0 ulib/{.cache => .hints}/FStar.Printf.fst.hints | 0 .../FStar.PropositionalExtensionality.fst.hints | 0 ulib/{.cache => .hints}/FStar.PtrdiffT.fst.hints | 0 ulib/{.cache => .hints}/FStar.PtrdiffT.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Pure.BreakVC.fst.hints | 0 ulib/{.cache => .hints}/FStar.Pure.BreakVC.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Range.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Real.Old.fst.hints | 0 ulib/{.cache => .hints}/FStar.Real.Old.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Real.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Ref.fst.hints | 0 .../{.cache => .hints}/FStar.RefinementExtensionality.fst.hints | 0 .../FStar.RefinementExtensionality.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.Const.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.Formula.fst.hints | 0 .../{.cache => .hints}/FStar.Reflection.TermEq.Simple.fst.hints | 0 .../FStar.Reflection.TermEq.Simple.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.TermEq.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.TermEq.fsti.hints | 0 .../FStar.Reflection.Typing.Builtins.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.Typing.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.Typing.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V1.Builtins.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V1.Compare.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V1.Data.fsti.hints | 0 .../FStar.Reflection.V1.Derived.Lemmas.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V1.Derived.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V1.Formula.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V1.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Arith.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Builtins.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Compare.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Compare.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Data.fsti.hints | 0 .../FStar.Reflection.V2.Derived.Lemmas.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Derived.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.Formula.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.V2.fst.hints | 0 ulib/{.cache => .hints}/FStar.Reflection.fst.hints | 0 .../FStar.ReflexiveTransitiveClosure.fst.hints | 0 .../FStar.ReflexiveTransitiveClosure.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Relational.Comp.fst.hints | 0 ulib/{.cache => .hints}/FStar.Relational.Relational.fst.hints | 0 ulib/{.cache => .hints}/FStar.ST.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sealed.Inhabited.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sealed.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Equiv.fst.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Equiv.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Permutation.fst.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Permutation.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Properties.fst.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Properties.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Seq.Sorted.fst.hints | 0 ulib/{.cache => .hints}/FStar.Seq.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Ambient.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Permutation.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Permutation.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Seq.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Seq.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.Util.fst.hints | 0 ulib/{.cache => .hints}/FStar.Sequence.fst.hints | 0 ulib/{.cache => .hints}/FStar.Set.fst.hints | 0 ulib/{.cache => .hints}/FStar.Set.fsti.hints | 0 ulib/{.cache => .hints}/FStar.SizeT.fst.hints | 0 ulib/{.cache => .hints}/FStar.SizeT.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Squash.fst.hints | 0 ulib/{.cache => .hints}/FStar.Squash.fsti.hints | 0 ulib/{.cache => .hints}/FStar.SquashProperties.fst.hints | 0 ulib/{.cache => .hints}/FStar.String.fsti.hints | 0 ulib/{.cache => .hints}/FStar.StrongExcludedMiddle.fst.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Errors.Msg.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Pprint.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Reflection.Types.fsti.hints | 0 .../FStar.Stubs.Reflection.V1.Builtins.fsti.hints | 0 .../FStar.Stubs.Reflection.V1.Data.fsti.hints | 0 .../FStar.Stubs.Reflection.V2.Builtins.fsti.hints | 0 .../FStar.Stubs.Reflection.V2.Data.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Syntax.Syntax.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Tactics.Common.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Tactics.Result.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.Tactics.Types.fsti.hints | 0 .../FStar.Stubs.Tactics.V1.Builtins.fsti.hints | 0 .../FStar.Stubs.Tactics.V2.Builtins.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Stubs.TypeChecker.Core.fsti.hints | 0 ulib/{.cache => .hints}/FStar.TSet.fst.hints | 0 ulib/{.cache => .hints}/FStar.TSet.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Arith.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.BV.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.BreakVC.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.BreakVC.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Builtins.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Canon.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.CanonCommMonoid.fst.hints | 0 .../FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.hints | 0 .../FStar.Tactics.CanonCommMonoidSimple.fst.hints | 0 .../FStar.Tactics.CanonCommSemiring.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.CanonCommSwaps.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.CanonMonoid.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.CheckLN.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.CheckLN.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Common.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Common.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Derived.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Effect.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Effect.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Logic.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.MApply.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.MApply.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.MkProjectors.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.MkProjectors.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.NamedView.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.NamedView.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Parametricity.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Parametricity.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.PatternMatching.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Print.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Result.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Result.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.SMT.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Simplifier.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.SyntaxHelpers.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.TypeRepr.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.TypeRepr.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Typeclasses.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Typeclasses.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Types.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Unseal.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Util.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.V1.Derived.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.V1.Logic.fst.hints | 0 .../{.cache => .hints}/FStar.Tactics.V1.SyntaxHelpers.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.V1.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.V2.Derived.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.V2.Logic.fst.hints | 0 .../FStar.Tactics.V2.SyntaxCoercions.fst.hints | 0 .../{.cache => .hints}/FStar.Tactics.V2.SyntaxHelpers.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.V2.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.Visit.fst.hints | 0 ulib/{.cache => .hints}/FStar.Tactics.fst.hints | 0 ulib/{.cache => .hints}/FStar.TaggedUnion.fst.hints | 0 ulib/{.cache => .hints}/FStar.TaggedUnion.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Tcp.fsti.hints | 0 ulib/{.cache => .hints}/FStar.TwoLevelHeap.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt.fsti.hints | 0 ulib/{.cache => .hints}/FStar.UInt128.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt128.fsti.hints | 0 ulib/{.cache => .hints}/FStar.UInt16.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt16.fsti.hints | 0 ulib/{.cache => .hints}/FStar.UInt32.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt32.fsti.hints | 0 ulib/{.cache => .hints}/FStar.UInt64.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt64.fsti.hints | 0 ulib/{.cache => .hints}/FStar.UInt8.fst.hints | 0 ulib/{.cache => .hints}/FStar.UInt8.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Udp.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Universe.PCM.fst.hints | 0 ulib/{.cache => .hints}/FStar.Universe.fst.hints | 0 ulib/{.cache => .hints}/FStar.Universe.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Util.fst.hints | 0 ulib/{.cache => .hints}/FStar.VConfig.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Vector.Base.fst.hints | 0 ulib/{.cache => .hints}/FStar.Vector.Base.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Vector.Properties.fst.hints | 0 ulib/{.cache => .hints}/FStar.Vector.fst.hints | 0 ulib/{.cache => .hints}/FStar.WellFounded.Util.fst.hints | 0 ulib/{.cache => .hints}/FStar.WellFounded.Util.fsti.hints | 0 ulib/{.cache => .hints}/FStar.WellFounded.fst.hints | 0 ulib/{.cache => .hints}/FStar.WellFoundedRelation.fst.hints | 0 ulib/{.cache => .hints}/FStar.WellFoundedRelation.fsti.hints | 0 ulib/{.cache => .hints}/FStar.Witnessed.Core.fst.hints | 0 ulib/{.cache => .hints}/FStar.Witnessed.Core.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.Buffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.BufferCompat.fst.hints | 0 ulib/{.cache => .hints}/LowStar.BufferOps.fst.hints | 0 ulib/{.cache => .hints}/LowStar.BufferView.Down.fst.hints | 0 ulib/{.cache => .hints}/LowStar.BufferView.Down.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.BufferView.Up.fst.hints | 0 ulib/{.cache => .hints}/LowStar.BufferView.Up.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.BufferView.fst.hints | 0 ulib/{.cache => .hints}/LowStar.BufferView.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.Comment.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Comment.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.ConstBuffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.ConstBuffer.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.Endianness.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Failure.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.Ignore.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.ImmutableBuffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Lens.Buffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Lens.Tuple2.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Lens.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Literal.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.Modifies.fst.hints | 0 ulib/{.cache => .hints}/LowStar.ModifiesPat.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Monotonic.Buffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Monotonic.Buffer.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.PrefixFreezableBuffer.fst.hints | 0 .../{.cache => .hints}/LowStar.PrefixFreezableBuffer.fsti.hints | 0 ulib/{.cache => .hints}/LowStar.Printf.fst.hints | 0 ulib/{.cache => .hints}/LowStar.RVector.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Regional.Instances.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Regional.fst.hints | 0 ulib/{.cache => .hints}/LowStar.ToFStarBuffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.UninitializedBuffer.fst.hints | 0 ulib/{.cache => .hints}/LowStar.Vector.fst.hints | 0 ulib/{.cache => .hints}/prims.fst.hints | 0 ulib/Makefile.verify | 2 +- 396 files changed, 1 insertion(+), 1 deletion(-) rename ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.Equiv.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.Fold.Nested.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.Fold.Nested.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.Fold.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.Fold.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Algebra.CommMonoid.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Algebra.Monoid.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.All.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Array.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Array.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Axiomatic.Array.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.BV.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.BV.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.BaseTypes.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.BigOps.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.BigOps.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.BitVector.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Buffer.Quantifiers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Buffer.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.BufferNG.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Bytes.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Calc.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Calc.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Cardinality.Cantor.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Cardinality.Cantor.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Cardinality.Universes.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Cardinality.Universes.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Char.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.Add.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.Embeddable.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.Embeddable.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.Eq.Raw.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.Eq.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.Printable.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Class.TotalOrder.Raw.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Classical.Sugar.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Classical.Sugar.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Classical.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Classical.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.ConstantTime.Integers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.ConstantTime.Integers.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Constructive.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Crypto.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Date.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.DependentMap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.DependentMap.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Dyn.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Dyn.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Endianness.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Endianness.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.ErasedLogic.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Error.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Exn.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Fin.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Fin.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.FiniteMap.Ambient.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.FiniteMap.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.FiniteMap.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.FiniteSet.Ambient.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.FiniteSet.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.FiniteSet.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Float.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.FunctionalExtensionality.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.FunctionalExtensionality.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.FunctionalQueue.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.FunctionalQueue.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Functions.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Functions.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.GSet.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.GSet.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Ghost.Pull.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Ghost.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Ghost.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.GhostSet.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.GhostSet.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Heap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.HyperStack.All.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.HyperStack.IO.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.HyperStack.ST.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.HyperStack.ST.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.HyperStack.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.IFC.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.IFC.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.IO.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.ImmutableArray.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.ImmutableArray.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.IndefiniteDescription.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.IndefiniteDescription.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Int.Cast.Full.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int.Cast.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Int128.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int128.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Int16.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int16.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Int32.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int32.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Int64.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int64.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Int8.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Int8.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.IntegerIntervals.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Integers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.Effectful.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.ExploreTerm.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.Output.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.PostProcess.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.Propositions.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.InteractiveHelpers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Issue.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.LexicographicOrdering.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.LexicographicOrdering.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.List.Pure.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.List.Pure.Properties.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.List.Pure.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.List.Tot.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.List.Tot.Properties.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.List.Tot.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.List.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.MRef.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.MRef.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.MST.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.MSTTotal.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Map.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Map.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.MarkovsPrinciple.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Euclid.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Euclid.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Fermat.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Fermat.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Lemmas.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Lemmas.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Math.Lib.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Matrix.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Matrix.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Matrix2.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Modifies.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Modifies.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.ModifiesGen.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.ModifiesGen.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.DependentMap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.DependentMap.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Heap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Heap.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.HyperHeap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.HyperHeap.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.HyperStack.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.HyperStack.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Map.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Pure.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Seq.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Witnessed.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Monotonic.Witnessed.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Mul.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.NMST.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.NMSTTotal.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Option.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.OrdMap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.OrdMap.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.OrdMapProps.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.OrdSet.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.OrdSet.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.OrdSetProps.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Order.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PCM.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Parse.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PartialMap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PartialMap.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pervasives.Native.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pervasives.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pervasives.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Derived1.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Derived1.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Derived2.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Derived2.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Derived3.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.Derived3.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pointer.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PredicateExtensionality.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Preorder.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Printf.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PropositionalExtensionality.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PtrdiffT.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.PtrdiffT.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Pure.BreakVC.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Pure.BreakVC.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Range.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Real.Old.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Real.Old.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Real.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Ref.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.RefinementExtensionality.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.RefinementExtensionality.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.Const.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.Formula.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.TermEq.Simple.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.TermEq.Simple.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.TermEq.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.TermEq.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.Typing.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.Typing.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.Typing.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.Compare.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.Data.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.Derived.Lemmas.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.Derived.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.Formula.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V1.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Arith.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Compare.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Compare.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Data.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Derived.Lemmas.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Derived.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.Formula.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.V2.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Reflection.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.ReflexiveTransitiveClosure.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.ReflexiveTransitiveClosure.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Relational.Comp.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Relational.Relational.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.ST.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sealed.Inhabited.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sealed.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Equiv.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Equiv.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Permutation.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Permutation.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Properties.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Properties.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.Sorted.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Seq.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Ambient.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Permutation.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Permutation.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Seq.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Seq.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.Util.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Sequence.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Set.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Set.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.SizeT.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.SizeT.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Squash.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Squash.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.SquashProperties.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.String.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.StrongExcludedMiddle.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Errors.Msg.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Pprint.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Reflection.Types.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Reflection.V1.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Reflection.V1.Data.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Reflection.V2.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Reflection.V2.Data.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Syntax.Syntax.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Tactics.Common.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Tactics.Result.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Tactics.Types.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Tactics.V1.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.Tactics.V2.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Stubs.TypeChecker.Core.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.TSet.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.TSet.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Arith.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.BV.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.BreakVC.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.BreakVC.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Builtins.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Canon.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CanonCommMonoid.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CanonCommMonoidSimple.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CanonCommSemiring.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CanonCommSwaps.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CanonMonoid.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CheckLN.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.CheckLN.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Common.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Common.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Derived.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Effect.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Effect.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Logic.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.MApply.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.MApply.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.MkProjectors.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.MkProjectors.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.NamedView.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.NamedView.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Parametricity.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Parametricity.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.PatternMatching.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Print.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Result.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Result.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.SMT.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Simplifier.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.SyntaxHelpers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.TypeRepr.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.TypeRepr.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Typeclasses.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Typeclasses.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Types.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Unseal.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Util.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V1.Derived.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V1.Logic.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V1.SyntaxHelpers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V1.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V2.Derived.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V2.Logic.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V2.SyntaxCoercions.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V2.SyntaxHelpers.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.V2.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.Visit.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Tactics.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.TaggedUnion.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.TaggedUnion.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Tcp.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.TwoLevelHeap.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt128.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt128.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt16.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt16.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt32.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt32.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt64.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt64.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt8.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.UInt8.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Udp.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Universe.PCM.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Universe.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Universe.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Util.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.VConfig.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Vector.Base.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Vector.Base.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Vector.Properties.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Vector.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.WellFounded.Util.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.WellFounded.Util.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.WellFounded.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.WellFoundedRelation.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.WellFoundedRelation.fsti.hints (100%) rename ulib/{.cache => .hints}/FStar.Witnessed.Core.fst.hints (100%) rename ulib/{.cache => .hints}/FStar.Witnessed.Core.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.Buffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferCompat.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferOps.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferView.Down.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferView.Down.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferView.Up.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferView.Up.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferView.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.BufferView.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.Comment.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Comment.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.ConstBuffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.ConstBuffer.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.Endianness.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Failure.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.Ignore.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.ImmutableBuffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Lens.Buffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Lens.Tuple2.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Lens.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Literal.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.Modifies.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.ModifiesPat.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Monotonic.Buffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Monotonic.Buffer.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.PrefixFreezableBuffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.PrefixFreezableBuffer.fsti.hints (100%) rename ulib/{.cache => .hints}/LowStar.Printf.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.RVector.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Regional.Instances.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Regional.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.ToFStarBuffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.UninitializedBuffer.fst.hints (100%) rename ulib/{.cache => .hints}/LowStar.Vector.fst.hints (100%) rename ulib/{.cache => .hints}/prims.fst.hints (100%) diff --git a/ulib/.cache/FStar.Algebra.CommMonoid.Equiv.fst.hints b/ulib/.hints/FStar.Algebra.CommMonoid.Equiv.fst.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.CommMonoid.Equiv.fst.hints rename to ulib/.hints/FStar.Algebra.CommMonoid.Equiv.fst.hints diff --git a/ulib/.cache/FStar.Algebra.CommMonoid.Fold.Nested.fst.hints b/ulib/.hints/FStar.Algebra.CommMonoid.Fold.Nested.fst.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.CommMonoid.Fold.Nested.fst.hints rename to ulib/.hints/FStar.Algebra.CommMonoid.Fold.Nested.fst.hints diff --git a/ulib/.cache/FStar.Algebra.CommMonoid.Fold.Nested.fsti.hints b/ulib/.hints/FStar.Algebra.CommMonoid.Fold.Nested.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.CommMonoid.Fold.Nested.fsti.hints rename to ulib/.hints/FStar.Algebra.CommMonoid.Fold.Nested.fsti.hints diff --git a/ulib/.cache/FStar.Algebra.CommMonoid.Fold.fst.hints b/ulib/.hints/FStar.Algebra.CommMonoid.Fold.fst.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.CommMonoid.Fold.fst.hints rename to ulib/.hints/FStar.Algebra.CommMonoid.Fold.fst.hints diff --git a/ulib/.cache/FStar.Algebra.CommMonoid.Fold.fsti.hints b/ulib/.hints/FStar.Algebra.CommMonoid.Fold.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.CommMonoid.Fold.fsti.hints rename to ulib/.hints/FStar.Algebra.CommMonoid.Fold.fsti.hints diff --git a/ulib/.cache/FStar.Algebra.CommMonoid.fst.hints b/ulib/.hints/FStar.Algebra.CommMonoid.fst.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.CommMonoid.fst.hints rename to ulib/.hints/FStar.Algebra.CommMonoid.fst.hints diff --git a/ulib/.cache/FStar.Algebra.Monoid.fst.hints b/ulib/.hints/FStar.Algebra.Monoid.fst.hints similarity index 100% rename from ulib/.cache/FStar.Algebra.Monoid.fst.hints rename to ulib/.hints/FStar.Algebra.Monoid.fst.hints diff --git a/ulib/.cache/FStar.All.fst.hints b/ulib/.hints/FStar.All.fst.hints similarity index 100% rename from ulib/.cache/FStar.All.fst.hints rename to ulib/.hints/FStar.All.fst.hints diff --git a/ulib/.cache/FStar.Array.fst.hints b/ulib/.hints/FStar.Array.fst.hints similarity index 100% rename from ulib/.cache/FStar.Array.fst.hints rename to ulib/.hints/FStar.Array.fst.hints diff --git a/ulib/.cache/FStar.Array.fsti.hints b/ulib/.hints/FStar.Array.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Array.fsti.hints rename to ulib/.hints/FStar.Array.fsti.hints diff --git a/ulib/.cache/FStar.Axiomatic.Array.fst.hints b/ulib/.hints/FStar.Axiomatic.Array.fst.hints similarity index 100% rename from ulib/.cache/FStar.Axiomatic.Array.fst.hints rename to ulib/.hints/FStar.Axiomatic.Array.fst.hints diff --git a/ulib/.cache/FStar.BV.fst.hints b/ulib/.hints/FStar.BV.fst.hints similarity index 100% rename from ulib/.cache/FStar.BV.fst.hints rename to ulib/.hints/FStar.BV.fst.hints diff --git a/ulib/.cache/FStar.BV.fsti.hints b/ulib/.hints/FStar.BV.fsti.hints similarity index 100% rename from ulib/.cache/FStar.BV.fsti.hints rename to ulib/.hints/FStar.BV.fsti.hints diff --git a/ulib/.cache/FStar.BaseTypes.fsti.hints b/ulib/.hints/FStar.BaseTypes.fsti.hints similarity index 100% rename from ulib/.cache/FStar.BaseTypes.fsti.hints rename to ulib/.hints/FStar.BaseTypes.fsti.hints diff --git a/ulib/.cache/FStar.BigOps.fst.hints b/ulib/.hints/FStar.BigOps.fst.hints similarity index 100% rename from ulib/.cache/FStar.BigOps.fst.hints rename to ulib/.hints/FStar.BigOps.fst.hints diff --git a/ulib/.cache/FStar.BigOps.fsti.hints b/ulib/.hints/FStar.BigOps.fsti.hints similarity index 100% rename from ulib/.cache/FStar.BigOps.fsti.hints rename to ulib/.hints/FStar.BigOps.fsti.hints diff --git a/ulib/.cache/FStar.BitVector.fst.hints b/ulib/.hints/FStar.BitVector.fst.hints similarity index 100% rename from ulib/.cache/FStar.BitVector.fst.hints rename to ulib/.hints/FStar.BitVector.fst.hints diff --git a/ulib/.cache/FStar.Buffer.Quantifiers.fst.hints b/ulib/.hints/FStar.Buffer.Quantifiers.fst.hints similarity index 100% rename from ulib/.cache/FStar.Buffer.Quantifiers.fst.hints rename to ulib/.hints/FStar.Buffer.Quantifiers.fst.hints diff --git a/ulib/.cache/FStar.Buffer.fst.hints b/ulib/.hints/FStar.Buffer.fst.hints similarity index 100% rename from ulib/.cache/FStar.Buffer.fst.hints rename to ulib/.hints/FStar.Buffer.fst.hints diff --git a/ulib/.cache/FStar.BufferNG.fst.hints b/ulib/.hints/FStar.BufferNG.fst.hints similarity index 100% rename from ulib/.cache/FStar.BufferNG.fst.hints rename to ulib/.hints/FStar.BufferNG.fst.hints diff --git a/ulib/.cache/FStar.Bytes.fsti.hints b/ulib/.hints/FStar.Bytes.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Bytes.fsti.hints rename to ulib/.hints/FStar.Bytes.fsti.hints diff --git a/ulib/.cache/FStar.Calc.fst.hints b/ulib/.hints/FStar.Calc.fst.hints similarity index 100% rename from ulib/.cache/FStar.Calc.fst.hints rename to ulib/.hints/FStar.Calc.fst.hints diff --git a/ulib/.cache/FStar.Calc.fsti.hints b/ulib/.hints/FStar.Calc.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Calc.fsti.hints rename to ulib/.hints/FStar.Calc.fsti.hints diff --git a/ulib/.cache/FStar.Cardinality.Cantor.fst.hints b/ulib/.hints/FStar.Cardinality.Cantor.fst.hints similarity index 100% rename from ulib/.cache/FStar.Cardinality.Cantor.fst.hints rename to ulib/.hints/FStar.Cardinality.Cantor.fst.hints diff --git a/ulib/.cache/FStar.Cardinality.Cantor.fsti.hints b/ulib/.hints/FStar.Cardinality.Cantor.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Cardinality.Cantor.fsti.hints rename to ulib/.hints/FStar.Cardinality.Cantor.fsti.hints diff --git a/ulib/.cache/FStar.Cardinality.Universes.fst.hints b/ulib/.hints/FStar.Cardinality.Universes.fst.hints similarity index 100% rename from ulib/.cache/FStar.Cardinality.Universes.fst.hints rename to ulib/.hints/FStar.Cardinality.Universes.fst.hints diff --git a/ulib/.cache/FStar.Cardinality.Universes.fsti.hints b/ulib/.hints/FStar.Cardinality.Universes.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Cardinality.Universes.fsti.hints rename to ulib/.hints/FStar.Cardinality.Universes.fsti.hints diff --git a/ulib/.cache/FStar.Char.fsti.hints b/ulib/.hints/FStar.Char.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Char.fsti.hints rename to ulib/.hints/FStar.Char.fsti.hints diff --git a/ulib/.cache/FStar.Class.Add.fst.hints b/ulib/.hints/FStar.Class.Add.fst.hints similarity index 100% rename from ulib/.cache/FStar.Class.Add.fst.hints rename to ulib/.hints/FStar.Class.Add.fst.hints diff --git a/ulib/.cache/FStar.Class.Embeddable.fst.hints b/ulib/.hints/FStar.Class.Embeddable.fst.hints similarity index 100% rename from ulib/.cache/FStar.Class.Embeddable.fst.hints rename to ulib/.hints/FStar.Class.Embeddable.fst.hints diff --git a/ulib/.cache/FStar.Class.Embeddable.fsti.hints b/ulib/.hints/FStar.Class.Embeddable.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Class.Embeddable.fsti.hints rename to ulib/.hints/FStar.Class.Embeddable.fsti.hints diff --git a/ulib/.cache/FStar.Class.Eq.Raw.fst.hints b/ulib/.hints/FStar.Class.Eq.Raw.fst.hints similarity index 100% rename from ulib/.cache/FStar.Class.Eq.Raw.fst.hints rename to ulib/.hints/FStar.Class.Eq.Raw.fst.hints diff --git a/ulib/.cache/FStar.Class.Eq.fst.hints b/ulib/.hints/FStar.Class.Eq.fst.hints similarity index 100% rename from ulib/.cache/FStar.Class.Eq.fst.hints rename to ulib/.hints/FStar.Class.Eq.fst.hints diff --git a/ulib/.cache/FStar.Class.Printable.fst.hints b/ulib/.hints/FStar.Class.Printable.fst.hints similarity index 100% rename from ulib/.cache/FStar.Class.Printable.fst.hints rename to ulib/.hints/FStar.Class.Printable.fst.hints diff --git a/ulib/.cache/FStar.Class.TotalOrder.Raw.fst.hints b/ulib/.hints/FStar.Class.TotalOrder.Raw.fst.hints similarity index 100% rename from ulib/.cache/FStar.Class.TotalOrder.Raw.fst.hints rename to ulib/.hints/FStar.Class.TotalOrder.Raw.fst.hints diff --git a/ulib/.cache/FStar.Classical.Sugar.fst.hints b/ulib/.hints/FStar.Classical.Sugar.fst.hints similarity index 100% rename from ulib/.cache/FStar.Classical.Sugar.fst.hints rename to ulib/.hints/FStar.Classical.Sugar.fst.hints diff --git a/ulib/.cache/FStar.Classical.Sugar.fsti.hints b/ulib/.hints/FStar.Classical.Sugar.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Classical.Sugar.fsti.hints rename to ulib/.hints/FStar.Classical.Sugar.fsti.hints diff --git a/ulib/.cache/FStar.Classical.fst.hints b/ulib/.hints/FStar.Classical.fst.hints similarity index 100% rename from ulib/.cache/FStar.Classical.fst.hints rename to ulib/.hints/FStar.Classical.fst.hints diff --git a/ulib/.cache/FStar.Classical.fsti.hints b/ulib/.hints/FStar.Classical.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Classical.fsti.hints rename to ulib/.hints/FStar.Classical.fsti.hints diff --git a/ulib/.cache/FStar.ConstantTime.Integers.fst.hints b/ulib/.hints/FStar.ConstantTime.Integers.fst.hints similarity index 100% rename from ulib/.cache/FStar.ConstantTime.Integers.fst.hints rename to ulib/.hints/FStar.ConstantTime.Integers.fst.hints diff --git a/ulib/.cache/FStar.ConstantTime.Integers.fsti.hints b/ulib/.hints/FStar.ConstantTime.Integers.fsti.hints similarity index 100% rename from ulib/.cache/FStar.ConstantTime.Integers.fsti.hints rename to ulib/.hints/FStar.ConstantTime.Integers.fsti.hints diff --git a/ulib/.cache/FStar.Constructive.fst.hints b/ulib/.hints/FStar.Constructive.fst.hints similarity index 100% rename from ulib/.cache/FStar.Constructive.fst.hints rename to ulib/.hints/FStar.Constructive.fst.hints diff --git a/ulib/.cache/FStar.Crypto.fst.hints b/ulib/.hints/FStar.Crypto.fst.hints similarity index 100% rename from ulib/.cache/FStar.Crypto.fst.hints rename to ulib/.hints/FStar.Crypto.fst.hints diff --git a/ulib/.cache/FStar.Date.fsti.hints b/ulib/.hints/FStar.Date.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Date.fsti.hints rename to ulib/.hints/FStar.Date.fsti.hints diff --git a/ulib/.cache/FStar.DependentMap.fst.hints b/ulib/.hints/FStar.DependentMap.fst.hints similarity index 100% rename from ulib/.cache/FStar.DependentMap.fst.hints rename to ulib/.hints/FStar.DependentMap.fst.hints diff --git a/ulib/.cache/FStar.DependentMap.fsti.hints b/ulib/.hints/FStar.DependentMap.fsti.hints similarity index 100% rename from ulib/.cache/FStar.DependentMap.fsti.hints rename to ulib/.hints/FStar.DependentMap.fsti.hints diff --git a/ulib/.cache/FStar.Dyn.fst.hints b/ulib/.hints/FStar.Dyn.fst.hints similarity index 100% rename from ulib/.cache/FStar.Dyn.fst.hints rename to ulib/.hints/FStar.Dyn.fst.hints diff --git a/ulib/.cache/FStar.Dyn.fsti.hints b/ulib/.hints/FStar.Dyn.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Dyn.fsti.hints rename to ulib/.hints/FStar.Dyn.fsti.hints diff --git a/ulib/.cache/FStar.Endianness.fst.hints b/ulib/.hints/FStar.Endianness.fst.hints similarity index 100% rename from ulib/.cache/FStar.Endianness.fst.hints rename to ulib/.hints/FStar.Endianness.fst.hints diff --git a/ulib/.cache/FStar.Endianness.fsti.hints b/ulib/.hints/FStar.Endianness.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Endianness.fsti.hints rename to ulib/.hints/FStar.Endianness.fsti.hints diff --git a/ulib/.cache/FStar.ErasedLogic.fst.hints b/ulib/.hints/FStar.ErasedLogic.fst.hints similarity index 100% rename from ulib/.cache/FStar.ErasedLogic.fst.hints rename to ulib/.hints/FStar.ErasedLogic.fst.hints diff --git a/ulib/.cache/FStar.Error.fst.hints b/ulib/.hints/FStar.Error.fst.hints similarity index 100% rename from ulib/.cache/FStar.Error.fst.hints rename to ulib/.hints/FStar.Error.fst.hints diff --git a/ulib/.cache/FStar.Exn.fst.hints b/ulib/.hints/FStar.Exn.fst.hints similarity index 100% rename from ulib/.cache/FStar.Exn.fst.hints rename to ulib/.hints/FStar.Exn.fst.hints diff --git a/ulib/.cache/FStar.Fin.fst.hints b/ulib/.hints/FStar.Fin.fst.hints similarity index 100% rename from ulib/.cache/FStar.Fin.fst.hints rename to ulib/.hints/FStar.Fin.fst.hints diff --git a/ulib/.cache/FStar.Fin.fsti.hints b/ulib/.hints/FStar.Fin.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Fin.fsti.hints rename to ulib/.hints/FStar.Fin.fsti.hints diff --git a/ulib/.cache/FStar.FiniteMap.Ambient.fst.hints b/ulib/.hints/FStar.FiniteMap.Ambient.fst.hints similarity index 100% rename from ulib/.cache/FStar.FiniteMap.Ambient.fst.hints rename to ulib/.hints/FStar.FiniteMap.Ambient.fst.hints diff --git a/ulib/.cache/FStar.FiniteMap.Base.fst.hints b/ulib/.hints/FStar.FiniteMap.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.FiniteMap.Base.fst.hints rename to ulib/.hints/FStar.FiniteMap.Base.fst.hints diff --git a/ulib/.cache/FStar.FiniteMap.Base.fsti.hints b/ulib/.hints/FStar.FiniteMap.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.FiniteMap.Base.fsti.hints rename to ulib/.hints/FStar.FiniteMap.Base.fsti.hints diff --git a/ulib/.cache/FStar.FiniteSet.Ambient.fst.hints b/ulib/.hints/FStar.FiniteSet.Ambient.fst.hints similarity index 100% rename from ulib/.cache/FStar.FiniteSet.Ambient.fst.hints rename to ulib/.hints/FStar.FiniteSet.Ambient.fst.hints diff --git a/ulib/.cache/FStar.FiniteSet.Base.fst.hints b/ulib/.hints/FStar.FiniteSet.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.FiniteSet.Base.fst.hints rename to ulib/.hints/FStar.FiniteSet.Base.fst.hints diff --git a/ulib/.cache/FStar.FiniteSet.Base.fsti.hints b/ulib/.hints/FStar.FiniteSet.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.FiniteSet.Base.fsti.hints rename to ulib/.hints/FStar.FiniteSet.Base.fsti.hints diff --git a/ulib/.cache/FStar.Float.fsti.hints b/ulib/.hints/FStar.Float.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Float.fsti.hints rename to ulib/.hints/FStar.Float.fsti.hints diff --git a/ulib/.cache/FStar.FunctionalExtensionality.fst.hints b/ulib/.hints/FStar.FunctionalExtensionality.fst.hints similarity index 100% rename from ulib/.cache/FStar.FunctionalExtensionality.fst.hints rename to ulib/.hints/FStar.FunctionalExtensionality.fst.hints diff --git a/ulib/.cache/FStar.FunctionalExtensionality.fsti.hints b/ulib/.hints/FStar.FunctionalExtensionality.fsti.hints similarity index 100% rename from ulib/.cache/FStar.FunctionalExtensionality.fsti.hints rename to ulib/.hints/FStar.FunctionalExtensionality.fsti.hints diff --git a/ulib/.cache/FStar.FunctionalQueue.fst.hints b/ulib/.hints/FStar.FunctionalQueue.fst.hints similarity index 100% rename from ulib/.cache/FStar.FunctionalQueue.fst.hints rename to ulib/.hints/FStar.FunctionalQueue.fst.hints diff --git a/ulib/.cache/FStar.FunctionalQueue.fsti.hints b/ulib/.hints/FStar.FunctionalQueue.fsti.hints similarity index 100% rename from ulib/.cache/FStar.FunctionalQueue.fsti.hints rename to ulib/.hints/FStar.FunctionalQueue.fsti.hints diff --git a/ulib/.cache/FStar.Functions.fst.hints b/ulib/.hints/FStar.Functions.fst.hints similarity index 100% rename from ulib/.cache/FStar.Functions.fst.hints rename to ulib/.hints/FStar.Functions.fst.hints diff --git a/ulib/.cache/FStar.Functions.fsti.hints b/ulib/.hints/FStar.Functions.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Functions.fsti.hints rename to ulib/.hints/FStar.Functions.fsti.hints diff --git a/ulib/.cache/FStar.GSet.fst.hints b/ulib/.hints/FStar.GSet.fst.hints similarity index 100% rename from ulib/.cache/FStar.GSet.fst.hints rename to ulib/.hints/FStar.GSet.fst.hints diff --git a/ulib/.cache/FStar.GSet.fsti.hints b/ulib/.hints/FStar.GSet.fsti.hints similarity index 100% rename from ulib/.cache/FStar.GSet.fsti.hints rename to ulib/.hints/FStar.GSet.fsti.hints diff --git a/ulib/.cache/FStar.Ghost.Pull.fsti.hints b/ulib/.hints/FStar.Ghost.Pull.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Ghost.Pull.fsti.hints rename to ulib/.hints/FStar.Ghost.Pull.fsti.hints diff --git a/ulib/.cache/FStar.Ghost.fst.hints b/ulib/.hints/FStar.Ghost.fst.hints similarity index 100% rename from ulib/.cache/FStar.Ghost.fst.hints rename to ulib/.hints/FStar.Ghost.fst.hints diff --git a/ulib/.cache/FStar.Ghost.fsti.hints b/ulib/.hints/FStar.Ghost.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Ghost.fsti.hints rename to ulib/.hints/FStar.Ghost.fsti.hints diff --git a/ulib/.cache/FStar.GhostSet.fst.hints b/ulib/.hints/FStar.GhostSet.fst.hints similarity index 100% rename from ulib/.cache/FStar.GhostSet.fst.hints rename to ulib/.hints/FStar.GhostSet.fst.hints diff --git a/ulib/.cache/FStar.GhostSet.fsti.hints b/ulib/.hints/FStar.GhostSet.fsti.hints similarity index 100% rename from ulib/.cache/FStar.GhostSet.fsti.hints rename to ulib/.hints/FStar.GhostSet.fsti.hints diff --git a/ulib/.cache/FStar.Heap.fst.hints b/ulib/.hints/FStar.Heap.fst.hints similarity index 100% rename from ulib/.cache/FStar.Heap.fst.hints rename to ulib/.hints/FStar.Heap.fst.hints diff --git a/ulib/.cache/FStar.HyperStack.All.fst.hints b/ulib/.hints/FStar.HyperStack.All.fst.hints similarity index 100% rename from ulib/.cache/FStar.HyperStack.All.fst.hints rename to ulib/.hints/FStar.HyperStack.All.fst.hints diff --git a/ulib/.cache/FStar.HyperStack.IO.fst.hints b/ulib/.hints/FStar.HyperStack.IO.fst.hints similarity index 100% rename from ulib/.cache/FStar.HyperStack.IO.fst.hints rename to ulib/.hints/FStar.HyperStack.IO.fst.hints diff --git a/ulib/.cache/FStar.HyperStack.ST.fst.hints b/ulib/.hints/FStar.HyperStack.ST.fst.hints similarity index 100% rename from ulib/.cache/FStar.HyperStack.ST.fst.hints rename to ulib/.hints/FStar.HyperStack.ST.fst.hints diff --git a/ulib/.cache/FStar.HyperStack.ST.fsti.hints b/ulib/.hints/FStar.HyperStack.ST.fsti.hints similarity index 100% rename from ulib/.cache/FStar.HyperStack.ST.fsti.hints rename to ulib/.hints/FStar.HyperStack.ST.fsti.hints diff --git a/ulib/.cache/FStar.HyperStack.fst.hints b/ulib/.hints/FStar.HyperStack.fst.hints similarity index 100% rename from ulib/.cache/FStar.HyperStack.fst.hints rename to ulib/.hints/FStar.HyperStack.fst.hints diff --git a/ulib/.cache/FStar.IFC.fst.hints b/ulib/.hints/FStar.IFC.fst.hints similarity index 100% rename from ulib/.cache/FStar.IFC.fst.hints rename to ulib/.hints/FStar.IFC.fst.hints diff --git a/ulib/.cache/FStar.IFC.fsti.hints b/ulib/.hints/FStar.IFC.fsti.hints similarity index 100% rename from ulib/.cache/FStar.IFC.fsti.hints rename to ulib/.hints/FStar.IFC.fsti.hints diff --git a/ulib/.cache/FStar.IO.fst.hints b/ulib/.hints/FStar.IO.fst.hints similarity index 100% rename from ulib/.cache/FStar.IO.fst.hints rename to ulib/.hints/FStar.IO.fst.hints diff --git a/ulib/.cache/FStar.ImmutableArray.Base.fsti.hints b/ulib/.hints/FStar.ImmutableArray.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.ImmutableArray.Base.fsti.hints rename to ulib/.hints/FStar.ImmutableArray.Base.fsti.hints diff --git a/ulib/.cache/FStar.ImmutableArray.fsti.hints b/ulib/.hints/FStar.ImmutableArray.fsti.hints similarity index 100% rename from ulib/.cache/FStar.ImmutableArray.fsti.hints rename to ulib/.hints/FStar.ImmutableArray.fsti.hints diff --git a/ulib/.cache/FStar.IndefiniteDescription.fst.hints b/ulib/.hints/FStar.IndefiniteDescription.fst.hints similarity index 100% rename from ulib/.cache/FStar.IndefiniteDescription.fst.hints rename to ulib/.hints/FStar.IndefiniteDescription.fst.hints diff --git a/ulib/.cache/FStar.IndefiniteDescription.fsti.hints b/ulib/.hints/FStar.IndefiniteDescription.fsti.hints similarity index 100% rename from ulib/.cache/FStar.IndefiniteDescription.fsti.hints rename to ulib/.hints/FStar.IndefiniteDescription.fsti.hints diff --git a/ulib/.cache/FStar.Int.Cast.Full.fst.hints b/ulib/.hints/FStar.Int.Cast.Full.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int.Cast.Full.fst.hints rename to ulib/.hints/FStar.Int.Cast.Full.fst.hints diff --git a/ulib/.cache/FStar.Int.Cast.fst.hints b/ulib/.hints/FStar.Int.Cast.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int.Cast.fst.hints rename to ulib/.hints/FStar.Int.Cast.fst.hints diff --git a/ulib/.cache/FStar.Int.fst.hints b/ulib/.hints/FStar.Int.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int.fst.hints rename to ulib/.hints/FStar.Int.fst.hints diff --git a/ulib/.cache/FStar.Int.fsti.hints b/ulib/.hints/FStar.Int.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Int.fsti.hints rename to ulib/.hints/FStar.Int.fsti.hints diff --git a/ulib/.cache/FStar.Int128.fst.hints b/ulib/.hints/FStar.Int128.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int128.fst.hints rename to ulib/.hints/FStar.Int128.fst.hints diff --git a/ulib/.cache/FStar.Int128.fsti.hints b/ulib/.hints/FStar.Int128.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Int128.fsti.hints rename to ulib/.hints/FStar.Int128.fsti.hints diff --git a/ulib/.cache/FStar.Int16.fst.hints b/ulib/.hints/FStar.Int16.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int16.fst.hints rename to ulib/.hints/FStar.Int16.fst.hints diff --git a/ulib/.cache/FStar.Int16.fsti.hints b/ulib/.hints/FStar.Int16.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Int16.fsti.hints rename to ulib/.hints/FStar.Int16.fsti.hints diff --git a/ulib/.cache/FStar.Int32.fst.hints b/ulib/.hints/FStar.Int32.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int32.fst.hints rename to ulib/.hints/FStar.Int32.fst.hints diff --git a/ulib/.cache/FStar.Int32.fsti.hints b/ulib/.hints/FStar.Int32.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Int32.fsti.hints rename to ulib/.hints/FStar.Int32.fsti.hints diff --git a/ulib/.cache/FStar.Int64.fst.hints b/ulib/.hints/FStar.Int64.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int64.fst.hints rename to ulib/.hints/FStar.Int64.fst.hints diff --git a/ulib/.cache/FStar.Int64.fsti.hints b/ulib/.hints/FStar.Int64.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Int64.fsti.hints rename to ulib/.hints/FStar.Int64.fsti.hints diff --git a/ulib/.cache/FStar.Int8.fst.hints b/ulib/.hints/FStar.Int8.fst.hints similarity index 100% rename from ulib/.cache/FStar.Int8.fst.hints rename to ulib/.hints/FStar.Int8.fst.hints diff --git a/ulib/.cache/FStar.Int8.fsti.hints b/ulib/.hints/FStar.Int8.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Int8.fsti.hints rename to ulib/.hints/FStar.Int8.fsti.hints diff --git a/ulib/.cache/FStar.IntegerIntervals.fst.hints b/ulib/.hints/FStar.IntegerIntervals.fst.hints similarity index 100% rename from ulib/.cache/FStar.IntegerIntervals.fst.hints rename to ulib/.hints/FStar.IntegerIntervals.fst.hints diff --git a/ulib/.cache/FStar.Integers.fst.hints b/ulib/.hints/FStar.Integers.fst.hints similarity index 100% rename from ulib/.cache/FStar.Integers.fst.hints rename to ulib/.hints/FStar.Integers.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.Base.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.Base.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.Base.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.Effectful.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.Effectful.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.Effectful.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.Effectful.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.ExploreTerm.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.ExploreTerm.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.ExploreTerm.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.ExploreTerm.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.Output.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.Output.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.Output.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.Output.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.PostProcess.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.PostProcess.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.PostProcess.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.PostProcess.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.Propositions.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.Propositions.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.Propositions.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.Propositions.fst.hints diff --git a/ulib/.cache/FStar.InteractiveHelpers.fst.hints b/ulib/.hints/FStar.InteractiveHelpers.fst.hints similarity index 100% rename from ulib/.cache/FStar.InteractiveHelpers.fst.hints rename to ulib/.hints/FStar.InteractiveHelpers.fst.hints diff --git a/ulib/.cache/FStar.Issue.fsti.hints b/ulib/.hints/FStar.Issue.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Issue.fsti.hints rename to ulib/.hints/FStar.Issue.fsti.hints diff --git a/ulib/.cache/FStar.LexicographicOrdering.fst.hints b/ulib/.hints/FStar.LexicographicOrdering.fst.hints similarity index 100% rename from ulib/.cache/FStar.LexicographicOrdering.fst.hints rename to ulib/.hints/FStar.LexicographicOrdering.fst.hints diff --git a/ulib/.cache/FStar.LexicographicOrdering.fsti.hints b/ulib/.hints/FStar.LexicographicOrdering.fsti.hints similarity index 100% rename from ulib/.cache/FStar.LexicographicOrdering.fsti.hints rename to ulib/.hints/FStar.LexicographicOrdering.fsti.hints diff --git a/ulib/.cache/FStar.List.Pure.Base.fst.hints b/ulib/.hints/FStar.List.Pure.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.Pure.Base.fst.hints rename to ulib/.hints/FStar.List.Pure.Base.fst.hints diff --git a/ulib/.cache/FStar.List.Pure.Properties.fst.hints b/ulib/.hints/FStar.List.Pure.Properties.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.Pure.Properties.fst.hints rename to ulib/.hints/FStar.List.Pure.Properties.fst.hints diff --git a/ulib/.cache/FStar.List.Pure.fst.hints b/ulib/.hints/FStar.List.Pure.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.Pure.fst.hints rename to ulib/.hints/FStar.List.Pure.fst.hints diff --git a/ulib/.cache/FStar.List.Tot.Base.fst.hints b/ulib/.hints/FStar.List.Tot.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.Tot.Base.fst.hints rename to ulib/.hints/FStar.List.Tot.Base.fst.hints diff --git a/ulib/.cache/FStar.List.Tot.Properties.fst.hints b/ulib/.hints/FStar.List.Tot.Properties.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.Tot.Properties.fst.hints rename to ulib/.hints/FStar.List.Tot.Properties.fst.hints diff --git a/ulib/.cache/FStar.List.Tot.fst.hints b/ulib/.hints/FStar.List.Tot.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.Tot.fst.hints rename to ulib/.hints/FStar.List.Tot.fst.hints diff --git a/ulib/.cache/FStar.List.fst.hints b/ulib/.hints/FStar.List.fst.hints similarity index 100% rename from ulib/.cache/FStar.List.fst.hints rename to ulib/.hints/FStar.List.fst.hints diff --git a/ulib/.cache/FStar.MRef.fst.hints b/ulib/.hints/FStar.MRef.fst.hints similarity index 100% rename from ulib/.cache/FStar.MRef.fst.hints rename to ulib/.hints/FStar.MRef.fst.hints diff --git a/ulib/.cache/FStar.MRef.fsti.hints b/ulib/.hints/FStar.MRef.fsti.hints similarity index 100% rename from ulib/.cache/FStar.MRef.fsti.hints rename to ulib/.hints/FStar.MRef.fsti.hints diff --git a/ulib/.cache/FStar.MST.fst.hints b/ulib/.hints/FStar.MST.fst.hints similarity index 100% rename from ulib/.cache/FStar.MST.fst.hints rename to ulib/.hints/FStar.MST.fst.hints diff --git a/ulib/.cache/FStar.MSTTotal.fst.hints b/ulib/.hints/FStar.MSTTotal.fst.hints similarity index 100% rename from ulib/.cache/FStar.MSTTotal.fst.hints rename to ulib/.hints/FStar.MSTTotal.fst.hints diff --git a/ulib/.cache/FStar.Map.fst.hints b/ulib/.hints/FStar.Map.fst.hints similarity index 100% rename from ulib/.cache/FStar.Map.fst.hints rename to ulib/.hints/FStar.Map.fst.hints diff --git a/ulib/.cache/FStar.Map.fsti.hints b/ulib/.hints/FStar.Map.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Map.fsti.hints rename to ulib/.hints/FStar.Map.fsti.hints diff --git a/ulib/.cache/FStar.MarkovsPrinciple.fst.hints b/ulib/.hints/FStar.MarkovsPrinciple.fst.hints similarity index 100% rename from ulib/.cache/FStar.MarkovsPrinciple.fst.hints rename to ulib/.hints/FStar.MarkovsPrinciple.fst.hints diff --git a/ulib/.cache/FStar.Math.Euclid.fst.hints b/ulib/.hints/FStar.Math.Euclid.fst.hints similarity index 100% rename from ulib/.cache/FStar.Math.Euclid.fst.hints rename to ulib/.hints/FStar.Math.Euclid.fst.hints diff --git a/ulib/.cache/FStar.Math.Euclid.fsti.hints b/ulib/.hints/FStar.Math.Euclid.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Math.Euclid.fsti.hints rename to ulib/.hints/FStar.Math.Euclid.fsti.hints diff --git a/ulib/.cache/FStar.Math.Fermat.fst.hints b/ulib/.hints/FStar.Math.Fermat.fst.hints similarity index 100% rename from ulib/.cache/FStar.Math.Fermat.fst.hints rename to ulib/.hints/FStar.Math.Fermat.fst.hints diff --git a/ulib/.cache/FStar.Math.Fermat.fsti.hints b/ulib/.hints/FStar.Math.Fermat.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Math.Fermat.fsti.hints rename to ulib/.hints/FStar.Math.Fermat.fsti.hints diff --git a/ulib/.cache/FStar.Math.Lemmas.fst.hints b/ulib/.hints/FStar.Math.Lemmas.fst.hints similarity index 100% rename from ulib/.cache/FStar.Math.Lemmas.fst.hints rename to ulib/.hints/FStar.Math.Lemmas.fst.hints diff --git a/ulib/.cache/FStar.Math.Lemmas.fsti.hints b/ulib/.hints/FStar.Math.Lemmas.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Math.Lemmas.fsti.hints rename to ulib/.hints/FStar.Math.Lemmas.fsti.hints diff --git a/ulib/.cache/FStar.Math.Lib.fst.hints b/ulib/.hints/FStar.Math.Lib.fst.hints similarity index 100% rename from ulib/.cache/FStar.Math.Lib.fst.hints rename to ulib/.hints/FStar.Math.Lib.fst.hints diff --git a/ulib/.cache/FStar.Matrix.fst.hints b/ulib/.hints/FStar.Matrix.fst.hints similarity index 100% rename from ulib/.cache/FStar.Matrix.fst.hints rename to ulib/.hints/FStar.Matrix.fst.hints diff --git a/ulib/.cache/FStar.Matrix.fsti.hints b/ulib/.hints/FStar.Matrix.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Matrix.fsti.hints rename to ulib/.hints/FStar.Matrix.fsti.hints diff --git a/ulib/.cache/FStar.Matrix2.fsti.hints b/ulib/.hints/FStar.Matrix2.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Matrix2.fsti.hints rename to ulib/.hints/FStar.Matrix2.fsti.hints diff --git a/ulib/.cache/FStar.Modifies.fst.hints b/ulib/.hints/FStar.Modifies.fst.hints similarity index 100% rename from ulib/.cache/FStar.Modifies.fst.hints rename to ulib/.hints/FStar.Modifies.fst.hints diff --git a/ulib/.cache/FStar.Modifies.fsti.hints b/ulib/.hints/FStar.Modifies.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Modifies.fsti.hints rename to ulib/.hints/FStar.Modifies.fsti.hints diff --git a/ulib/.cache/FStar.ModifiesGen.fst.hints b/ulib/.hints/FStar.ModifiesGen.fst.hints similarity index 100% rename from ulib/.cache/FStar.ModifiesGen.fst.hints rename to ulib/.hints/FStar.ModifiesGen.fst.hints diff --git a/ulib/.cache/FStar.ModifiesGen.fsti.hints b/ulib/.hints/FStar.ModifiesGen.fsti.hints similarity index 100% rename from ulib/.cache/FStar.ModifiesGen.fsti.hints rename to ulib/.hints/FStar.ModifiesGen.fsti.hints diff --git a/ulib/.cache/FStar.Monotonic.DependentMap.fst.hints b/ulib/.hints/FStar.Monotonic.DependentMap.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.DependentMap.fst.hints rename to ulib/.hints/FStar.Monotonic.DependentMap.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.DependentMap.fsti.hints b/ulib/.hints/FStar.Monotonic.DependentMap.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.DependentMap.fsti.hints rename to ulib/.hints/FStar.Monotonic.DependentMap.fsti.hints diff --git a/ulib/.cache/FStar.Monotonic.Heap.fst.hints b/ulib/.hints/FStar.Monotonic.Heap.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Heap.fst.hints rename to ulib/.hints/FStar.Monotonic.Heap.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.Heap.fsti.hints b/ulib/.hints/FStar.Monotonic.Heap.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Heap.fsti.hints rename to ulib/.hints/FStar.Monotonic.Heap.fsti.hints diff --git a/ulib/.cache/FStar.Monotonic.HyperHeap.fst.hints b/ulib/.hints/FStar.Monotonic.HyperHeap.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.HyperHeap.fst.hints rename to ulib/.hints/FStar.Monotonic.HyperHeap.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.HyperHeap.fsti.hints b/ulib/.hints/FStar.Monotonic.HyperHeap.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.HyperHeap.fsti.hints rename to ulib/.hints/FStar.Monotonic.HyperHeap.fsti.hints diff --git a/ulib/.cache/FStar.Monotonic.HyperStack.fst.hints b/ulib/.hints/FStar.Monotonic.HyperStack.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.HyperStack.fst.hints rename to ulib/.hints/FStar.Monotonic.HyperStack.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.HyperStack.fsti.hints b/ulib/.hints/FStar.Monotonic.HyperStack.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.HyperStack.fsti.hints rename to ulib/.hints/FStar.Monotonic.HyperStack.fsti.hints diff --git a/ulib/.cache/FStar.Monotonic.Map.fst.hints b/ulib/.hints/FStar.Monotonic.Map.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Map.fst.hints rename to ulib/.hints/FStar.Monotonic.Map.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.Pure.fst.hints b/ulib/.hints/FStar.Monotonic.Pure.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Pure.fst.hints rename to ulib/.hints/FStar.Monotonic.Pure.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.Seq.fst.hints b/ulib/.hints/FStar.Monotonic.Seq.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Seq.fst.hints rename to ulib/.hints/FStar.Monotonic.Seq.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.Witnessed.fst.hints b/ulib/.hints/FStar.Monotonic.Witnessed.fst.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Witnessed.fst.hints rename to ulib/.hints/FStar.Monotonic.Witnessed.fst.hints diff --git a/ulib/.cache/FStar.Monotonic.Witnessed.fsti.hints b/ulib/.hints/FStar.Monotonic.Witnessed.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Monotonic.Witnessed.fsti.hints rename to ulib/.hints/FStar.Monotonic.Witnessed.fsti.hints diff --git a/ulib/.cache/FStar.Mul.fst.hints b/ulib/.hints/FStar.Mul.fst.hints similarity index 100% rename from ulib/.cache/FStar.Mul.fst.hints rename to ulib/.hints/FStar.Mul.fst.hints diff --git a/ulib/.cache/FStar.NMST.fst.hints b/ulib/.hints/FStar.NMST.fst.hints similarity index 100% rename from ulib/.cache/FStar.NMST.fst.hints rename to ulib/.hints/FStar.NMST.fst.hints diff --git a/ulib/.cache/FStar.NMSTTotal.fst.hints b/ulib/.hints/FStar.NMSTTotal.fst.hints similarity index 100% rename from ulib/.cache/FStar.NMSTTotal.fst.hints rename to ulib/.hints/FStar.NMSTTotal.fst.hints diff --git a/ulib/.cache/FStar.Option.fst.hints b/ulib/.hints/FStar.Option.fst.hints similarity index 100% rename from ulib/.cache/FStar.Option.fst.hints rename to ulib/.hints/FStar.Option.fst.hints diff --git a/ulib/.cache/FStar.OrdMap.fst.hints b/ulib/.hints/FStar.OrdMap.fst.hints similarity index 100% rename from ulib/.cache/FStar.OrdMap.fst.hints rename to ulib/.hints/FStar.OrdMap.fst.hints diff --git a/ulib/.cache/FStar.OrdMap.fsti.hints b/ulib/.hints/FStar.OrdMap.fsti.hints similarity index 100% rename from ulib/.cache/FStar.OrdMap.fsti.hints rename to ulib/.hints/FStar.OrdMap.fsti.hints diff --git a/ulib/.cache/FStar.OrdMapProps.fst.hints b/ulib/.hints/FStar.OrdMapProps.fst.hints similarity index 100% rename from ulib/.cache/FStar.OrdMapProps.fst.hints rename to ulib/.hints/FStar.OrdMapProps.fst.hints diff --git a/ulib/.cache/FStar.OrdSet.fst.hints b/ulib/.hints/FStar.OrdSet.fst.hints similarity index 100% rename from ulib/.cache/FStar.OrdSet.fst.hints rename to ulib/.hints/FStar.OrdSet.fst.hints diff --git a/ulib/.cache/FStar.OrdSet.fsti.hints b/ulib/.hints/FStar.OrdSet.fsti.hints similarity index 100% rename from ulib/.cache/FStar.OrdSet.fsti.hints rename to ulib/.hints/FStar.OrdSet.fsti.hints diff --git a/ulib/.cache/FStar.OrdSetProps.fst.hints b/ulib/.hints/FStar.OrdSetProps.fst.hints similarity index 100% rename from ulib/.cache/FStar.OrdSetProps.fst.hints rename to ulib/.hints/FStar.OrdSetProps.fst.hints diff --git a/ulib/.cache/FStar.Order.fst.hints b/ulib/.hints/FStar.Order.fst.hints similarity index 100% rename from ulib/.cache/FStar.Order.fst.hints rename to ulib/.hints/FStar.Order.fst.hints diff --git a/ulib/.cache/FStar.PCM.fst.hints b/ulib/.hints/FStar.PCM.fst.hints similarity index 100% rename from ulib/.cache/FStar.PCM.fst.hints rename to ulib/.hints/FStar.PCM.fst.hints diff --git a/ulib/.cache/FStar.Parse.fst.hints b/ulib/.hints/FStar.Parse.fst.hints similarity index 100% rename from ulib/.cache/FStar.Parse.fst.hints rename to ulib/.hints/FStar.Parse.fst.hints diff --git a/ulib/.cache/FStar.PartialMap.fst.hints b/ulib/.hints/FStar.PartialMap.fst.hints similarity index 100% rename from ulib/.cache/FStar.PartialMap.fst.hints rename to ulib/.hints/FStar.PartialMap.fst.hints diff --git a/ulib/.cache/FStar.PartialMap.fsti.hints b/ulib/.hints/FStar.PartialMap.fsti.hints similarity index 100% rename from ulib/.cache/FStar.PartialMap.fsti.hints rename to ulib/.hints/FStar.PartialMap.fsti.hints diff --git a/ulib/.cache/FStar.Pervasives.Native.fst.hints b/ulib/.hints/FStar.Pervasives.Native.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pervasives.Native.fst.hints rename to ulib/.hints/FStar.Pervasives.Native.fst.hints diff --git a/ulib/.cache/FStar.Pervasives.fst.hints b/ulib/.hints/FStar.Pervasives.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pervasives.fst.hints rename to ulib/.hints/FStar.Pervasives.fst.hints diff --git a/ulib/.cache/FStar.Pervasives.fsti.hints b/ulib/.hints/FStar.Pervasives.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Pervasives.fsti.hints rename to ulib/.hints/FStar.Pervasives.fsti.hints diff --git a/ulib/.cache/FStar.Pointer.Base.fst.hints b/ulib/.hints/FStar.Pointer.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Base.fst.hints rename to ulib/.hints/FStar.Pointer.Base.fst.hints diff --git a/ulib/.cache/FStar.Pointer.Base.fsti.hints b/ulib/.hints/FStar.Pointer.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Base.fsti.hints rename to ulib/.hints/FStar.Pointer.Base.fsti.hints diff --git a/ulib/.cache/FStar.Pointer.Derived1.fst.hints b/ulib/.hints/FStar.Pointer.Derived1.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Derived1.fst.hints rename to ulib/.hints/FStar.Pointer.Derived1.fst.hints diff --git a/ulib/.cache/FStar.Pointer.Derived1.fsti.hints b/ulib/.hints/FStar.Pointer.Derived1.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Derived1.fsti.hints rename to ulib/.hints/FStar.Pointer.Derived1.fsti.hints diff --git a/ulib/.cache/FStar.Pointer.Derived2.fst.hints b/ulib/.hints/FStar.Pointer.Derived2.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Derived2.fst.hints rename to ulib/.hints/FStar.Pointer.Derived2.fst.hints diff --git a/ulib/.cache/FStar.Pointer.Derived2.fsti.hints b/ulib/.hints/FStar.Pointer.Derived2.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Derived2.fsti.hints rename to ulib/.hints/FStar.Pointer.Derived2.fsti.hints diff --git a/ulib/.cache/FStar.Pointer.Derived3.fst.hints b/ulib/.hints/FStar.Pointer.Derived3.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Derived3.fst.hints rename to ulib/.hints/FStar.Pointer.Derived3.fst.hints diff --git a/ulib/.cache/FStar.Pointer.Derived3.fsti.hints b/ulib/.hints/FStar.Pointer.Derived3.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.Derived3.fsti.hints rename to ulib/.hints/FStar.Pointer.Derived3.fsti.hints diff --git a/ulib/.cache/FStar.Pointer.fst.hints b/ulib/.hints/FStar.Pointer.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pointer.fst.hints rename to ulib/.hints/FStar.Pointer.fst.hints diff --git a/ulib/.cache/FStar.PredicateExtensionality.fst.hints b/ulib/.hints/FStar.PredicateExtensionality.fst.hints similarity index 100% rename from ulib/.cache/FStar.PredicateExtensionality.fst.hints rename to ulib/.hints/FStar.PredicateExtensionality.fst.hints diff --git a/ulib/.cache/FStar.Preorder.fst.hints b/ulib/.hints/FStar.Preorder.fst.hints similarity index 100% rename from ulib/.cache/FStar.Preorder.fst.hints rename to ulib/.hints/FStar.Preorder.fst.hints diff --git a/ulib/.cache/FStar.Printf.fst.hints b/ulib/.hints/FStar.Printf.fst.hints similarity index 100% rename from ulib/.cache/FStar.Printf.fst.hints rename to ulib/.hints/FStar.Printf.fst.hints diff --git a/ulib/.cache/FStar.PropositionalExtensionality.fst.hints b/ulib/.hints/FStar.PropositionalExtensionality.fst.hints similarity index 100% rename from ulib/.cache/FStar.PropositionalExtensionality.fst.hints rename to ulib/.hints/FStar.PropositionalExtensionality.fst.hints diff --git a/ulib/.cache/FStar.PtrdiffT.fst.hints b/ulib/.hints/FStar.PtrdiffT.fst.hints similarity index 100% rename from ulib/.cache/FStar.PtrdiffT.fst.hints rename to ulib/.hints/FStar.PtrdiffT.fst.hints diff --git a/ulib/.cache/FStar.PtrdiffT.fsti.hints b/ulib/.hints/FStar.PtrdiffT.fsti.hints similarity index 100% rename from ulib/.cache/FStar.PtrdiffT.fsti.hints rename to ulib/.hints/FStar.PtrdiffT.fsti.hints diff --git a/ulib/.cache/FStar.Pure.BreakVC.fst.hints b/ulib/.hints/FStar.Pure.BreakVC.fst.hints similarity index 100% rename from ulib/.cache/FStar.Pure.BreakVC.fst.hints rename to ulib/.hints/FStar.Pure.BreakVC.fst.hints diff --git a/ulib/.cache/FStar.Pure.BreakVC.fsti.hints b/ulib/.hints/FStar.Pure.BreakVC.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Pure.BreakVC.fsti.hints rename to ulib/.hints/FStar.Pure.BreakVC.fsti.hints diff --git a/ulib/.cache/FStar.Range.fsti.hints b/ulib/.hints/FStar.Range.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Range.fsti.hints rename to ulib/.hints/FStar.Range.fsti.hints diff --git a/ulib/.cache/FStar.Real.Old.fst.hints b/ulib/.hints/FStar.Real.Old.fst.hints similarity index 100% rename from ulib/.cache/FStar.Real.Old.fst.hints rename to ulib/.hints/FStar.Real.Old.fst.hints diff --git a/ulib/.cache/FStar.Real.Old.fsti.hints b/ulib/.hints/FStar.Real.Old.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Real.Old.fsti.hints rename to ulib/.hints/FStar.Real.Old.fsti.hints diff --git a/ulib/.cache/FStar.Real.fsti.hints b/ulib/.hints/FStar.Real.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Real.fsti.hints rename to ulib/.hints/FStar.Real.fsti.hints diff --git a/ulib/.cache/FStar.Ref.fst.hints b/ulib/.hints/FStar.Ref.fst.hints similarity index 100% rename from ulib/.cache/FStar.Ref.fst.hints rename to ulib/.hints/FStar.Ref.fst.hints diff --git a/ulib/.cache/FStar.RefinementExtensionality.fst.hints b/ulib/.hints/FStar.RefinementExtensionality.fst.hints similarity index 100% rename from ulib/.cache/FStar.RefinementExtensionality.fst.hints rename to ulib/.hints/FStar.RefinementExtensionality.fst.hints diff --git a/ulib/.cache/FStar.RefinementExtensionality.fsti.hints b/ulib/.hints/FStar.RefinementExtensionality.fsti.hints similarity index 100% rename from ulib/.cache/FStar.RefinementExtensionality.fsti.hints rename to ulib/.hints/FStar.RefinementExtensionality.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.Const.fst.hints b/ulib/.hints/FStar.Reflection.Const.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.Const.fst.hints rename to ulib/.hints/FStar.Reflection.Const.fst.hints diff --git a/ulib/.cache/FStar.Reflection.Formula.fst.hints b/ulib/.hints/FStar.Reflection.Formula.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.Formula.fst.hints rename to ulib/.hints/FStar.Reflection.Formula.fst.hints diff --git a/ulib/.cache/FStar.Reflection.TermEq.Simple.fst.hints b/ulib/.hints/FStar.Reflection.TermEq.Simple.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.TermEq.Simple.fst.hints rename to ulib/.hints/FStar.Reflection.TermEq.Simple.fst.hints diff --git a/ulib/.cache/FStar.Reflection.TermEq.Simple.fsti.hints b/ulib/.hints/FStar.Reflection.TermEq.Simple.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.TermEq.Simple.fsti.hints rename to ulib/.hints/FStar.Reflection.TermEq.Simple.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.TermEq.fst.hints b/ulib/.hints/FStar.Reflection.TermEq.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.TermEq.fst.hints rename to ulib/.hints/FStar.Reflection.TermEq.fst.hints diff --git a/ulib/.cache/FStar.Reflection.TermEq.fsti.hints b/ulib/.hints/FStar.Reflection.TermEq.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.TermEq.fsti.hints rename to ulib/.hints/FStar.Reflection.TermEq.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.Typing.Builtins.fsti.hints b/ulib/.hints/FStar.Reflection.Typing.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.Typing.Builtins.fsti.hints rename to ulib/.hints/FStar.Reflection.Typing.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.Typing.fst.hints b/ulib/.hints/FStar.Reflection.Typing.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.Typing.fst.hints rename to ulib/.hints/FStar.Reflection.Typing.fst.hints diff --git a/ulib/.cache/FStar.Reflection.Typing.fsti.hints b/ulib/.hints/FStar.Reflection.Typing.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.Typing.fsti.hints rename to ulib/.hints/FStar.Reflection.Typing.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V1.Builtins.fsti.hints b/ulib/.hints/FStar.Reflection.V1.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.Builtins.fsti.hints rename to ulib/.hints/FStar.Reflection.V1.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V1.Compare.fsti.hints b/ulib/.hints/FStar.Reflection.V1.Compare.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.Compare.fsti.hints rename to ulib/.hints/FStar.Reflection.V1.Compare.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V1.Data.fsti.hints b/ulib/.hints/FStar.Reflection.V1.Data.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.Data.fsti.hints rename to ulib/.hints/FStar.Reflection.V1.Data.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V1.Derived.Lemmas.fst.hints b/ulib/.hints/FStar.Reflection.V1.Derived.Lemmas.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.Derived.Lemmas.fst.hints rename to ulib/.hints/FStar.Reflection.V1.Derived.Lemmas.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V1.Derived.fst.hints b/ulib/.hints/FStar.Reflection.V1.Derived.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.Derived.fst.hints rename to ulib/.hints/FStar.Reflection.V1.Derived.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V1.Formula.fst.hints b/ulib/.hints/FStar.Reflection.V1.Formula.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.Formula.fst.hints rename to ulib/.hints/FStar.Reflection.V1.Formula.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V1.fst.hints b/ulib/.hints/FStar.Reflection.V1.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V1.fst.hints rename to ulib/.hints/FStar.Reflection.V1.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Arith.fst.hints b/ulib/.hints/FStar.Reflection.V2.Arith.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Arith.fst.hints rename to ulib/.hints/FStar.Reflection.V2.Arith.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Builtins.fsti.hints b/ulib/.hints/FStar.Reflection.V2.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Builtins.fsti.hints rename to ulib/.hints/FStar.Reflection.V2.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Compare.fst.hints b/ulib/.hints/FStar.Reflection.V2.Compare.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Compare.fst.hints rename to ulib/.hints/FStar.Reflection.V2.Compare.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Compare.fsti.hints b/ulib/.hints/FStar.Reflection.V2.Compare.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Compare.fsti.hints rename to ulib/.hints/FStar.Reflection.V2.Compare.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Data.fsti.hints b/ulib/.hints/FStar.Reflection.V2.Data.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Data.fsti.hints rename to ulib/.hints/FStar.Reflection.V2.Data.fsti.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Derived.Lemmas.fst.hints b/ulib/.hints/FStar.Reflection.V2.Derived.Lemmas.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Derived.Lemmas.fst.hints rename to ulib/.hints/FStar.Reflection.V2.Derived.Lemmas.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Derived.fst.hints b/ulib/.hints/FStar.Reflection.V2.Derived.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Derived.fst.hints rename to ulib/.hints/FStar.Reflection.V2.Derived.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V2.Formula.fst.hints b/ulib/.hints/FStar.Reflection.V2.Formula.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.Formula.fst.hints rename to ulib/.hints/FStar.Reflection.V2.Formula.fst.hints diff --git a/ulib/.cache/FStar.Reflection.V2.fst.hints b/ulib/.hints/FStar.Reflection.V2.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.V2.fst.hints rename to ulib/.hints/FStar.Reflection.V2.fst.hints diff --git a/ulib/.cache/FStar.Reflection.fst.hints b/ulib/.hints/FStar.Reflection.fst.hints similarity index 100% rename from ulib/.cache/FStar.Reflection.fst.hints rename to ulib/.hints/FStar.Reflection.fst.hints diff --git a/ulib/.cache/FStar.ReflexiveTransitiveClosure.fst.hints b/ulib/.hints/FStar.ReflexiveTransitiveClosure.fst.hints similarity index 100% rename from ulib/.cache/FStar.ReflexiveTransitiveClosure.fst.hints rename to ulib/.hints/FStar.ReflexiveTransitiveClosure.fst.hints diff --git a/ulib/.cache/FStar.ReflexiveTransitiveClosure.fsti.hints b/ulib/.hints/FStar.ReflexiveTransitiveClosure.fsti.hints similarity index 100% rename from ulib/.cache/FStar.ReflexiveTransitiveClosure.fsti.hints rename to ulib/.hints/FStar.ReflexiveTransitiveClosure.fsti.hints diff --git a/ulib/.cache/FStar.Relational.Comp.fst.hints b/ulib/.hints/FStar.Relational.Comp.fst.hints similarity index 100% rename from ulib/.cache/FStar.Relational.Comp.fst.hints rename to ulib/.hints/FStar.Relational.Comp.fst.hints diff --git a/ulib/.cache/FStar.Relational.Relational.fst.hints b/ulib/.hints/FStar.Relational.Relational.fst.hints similarity index 100% rename from ulib/.cache/FStar.Relational.Relational.fst.hints rename to ulib/.hints/FStar.Relational.Relational.fst.hints diff --git a/ulib/.cache/FStar.ST.fst.hints b/ulib/.hints/FStar.ST.fst.hints similarity index 100% rename from ulib/.cache/FStar.ST.fst.hints rename to ulib/.hints/FStar.ST.fst.hints diff --git a/ulib/.cache/FStar.Sealed.Inhabited.fst.hints b/ulib/.hints/FStar.Sealed.Inhabited.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sealed.Inhabited.fst.hints rename to ulib/.hints/FStar.Sealed.Inhabited.fst.hints diff --git a/ulib/.cache/FStar.Sealed.fsti.hints b/ulib/.hints/FStar.Sealed.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Sealed.fsti.hints rename to ulib/.hints/FStar.Sealed.fsti.hints diff --git a/ulib/.cache/FStar.Seq.Base.fst.hints b/ulib/.hints/FStar.Seq.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Base.fst.hints rename to ulib/.hints/FStar.Seq.Base.fst.hints diff --git a/ulib/.cache/FStar.Seq.Base.fsti.hints b/ulib/.hints/FStar.Seq.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Base.fsti.hints rename to ulib/.hints/FStar.Seq.Base.fsti.hints diff --git a/ulib/.cache/FStar.Seq.Equiv.fst.hints b/ulib/.hints/FStar.Seq.Equiv.fst.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Equiv.fst.hints rename to ulib/.hints/FStar.Seq.Equiv.fst.hints diff --git a/ulib/.cache/FStar.Seq.Equiv.fsti.hints b/ulib/.hints/FStar.Seq.Equiv.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Equiv.fsti.hints rename to ulib/.hints/FStar.Seq.Equiv.fsti.hints diff --git a/ulib/.cache/FStar.Seq.Permutation.fst.hints b/ulib/.hints/FStar.Seq.Permutation.fst.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Permutation.fst.hints rename to ulib/.hints/FStar.Seq.Permutation.fst.hints diff --git a/ulib/.cache/FStar.Seq.Permutation.fsti.hints b/ulib/.hints/FStar.Seq.Permutation.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Permutation.fsti.hints rename to ulib/.hints/FStar.Seq.Permutation.fsti.hints diff --git a/ulib/.cache/FStar.Seq.Properties.fst.hints b/ulib/.hints/FStar.Seq.Properties.fst.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Properties.fst.hints rename to ulib/.hints/FStar.Seq.Properties.fst.hints diff --git a/ulib/.cache/FStar.Seq.Properties.fsti.hints b/ulib/.hints/FStar.Seq.Properties.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Properties.fsti.hints rename to ulib/.hints/FStar.Seq.Properties.fsti.hints diff --git a/ulib/.cache/FStar.Seq.Sorted.fst.hints b/ulib/.hints/FStar.Seq.Sorted.fst.hints similarity index 100% rename from ulib/.cache/FStar.Seq.Sorted.fst.hints rename to ulib/.hints/FStar.Seq.Sorted.fst.hints diff --git a/ulib/.cache/FStar.Seq.fst.hints b/ulib/.hints/FStar.Seq.fst.hints similarity index 100% rename from ulib/.cache/FStar.Seq.fst.hints rename to ulib/.hints/FStar.Seq.fst.hints diff --git a/ulib/.cache/FStar.Sequence.Ambient.fst.hints b/ulib/.hints/FStar.Sequence.Ambient.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Ambient.fst.hints rename to ulib/.hints/FStar.Sequence.Ambient.fst.hints diff --git a/ulib/.cache/FStar.Sequence.Base.fst.hints b/ulib/.hints/FStar.Sequence.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Base.fst.hints rename to ulib/.hints/FStar.Sequence.Base.fst.hints diff --git a/ulib/.cache/FStar.Sequence.Base.fsti.hints b/ulib/.hints/FStar.Sequence.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Base.fsti.hints rename to ulib/.hints/FStar.Sequence.Base.fsti.hints diff --git a/ulib/.cache/FStar.Sequence.Permutation.fst.hints b/ulib/.hints/FStar.Sequence.Permutation.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Permutation.fst.hints rename to ulib/.hints/FStar.Sequence.Permutation.fst.hints diff --git a/ulib/.cache/FStar.Sequence.Permutation.fsti.hints b/ulib/.hints/FStar.Sequence.Permutation.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Permutation.fsti.hints rename to ulib/.hints/FStar.Sequence.Permutation.fsti.hints diff --git a/ulib/.cache/FStar.Sequence.Seq.fst.hints b/ulib/.hints/FStar.Sequence.Seq.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Seq.fst.hints rename to ulib/.hints/FStar.Sequence.Seq.fst.hints diff --git a/ulib/.cache/FStar.Sequence.Seq.fsti.hints b/ulib/.hints/FStar.Sequence.Seq.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Seq.fsti.hints rename to ulib/.hints/FStar.Sequence.Seq.fsti.hints diff --git a/ulib/.cache/FStar.Sequence.Util.fst.hints b/ulib/.hints/FStar.Sequence.Util.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.Util.fst.hints rename to ulib/.hints/FStar.Sequence.Util.fst.hints diff --git a/ulib/.cache/FStar.Sequence.fst.hints b/ulib/.hints/FStar.Sequence.fst.hints similarity index 100% rename from ulib/.cache/FStar.Sequence.fst.hints rename to ulib/.hints/FStar.Sequence.fst.hints diff --git a/ulib/.cache/FStar.Set.fst.hints b/ulib/.hints/FStar.Set.fst.hints similarity index 100% rename from ulib/.cache/FStar.Set.fst.hints rename to ulib/.hints/FStar.Set.fst.hints diff --git a/ulib/.cache/FStar.Set.fsti.hints b/ulib/.hints/FStar.Set.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Set.fsti.hints rename to ulib/.hints/FStar.Set.fsti.hints diff --git a/ulib/.cache/FStar.SizeT.fst.hints b/ulib/.hints/FStar.SizeT.fst.hints similarity index 100% rename from ulib/.cache/FStar.SizeT.fst.hints rename to ulib/.hints/FStar.SizeT.fst.hints diff --git a/ulib/.cache/FStar.SizeT.fsti.hints b/ulib/.hints/FStar.SizeT.fsti.hints similarity index 100% rename from ulib/.cache/FStar.SizeT.fsti.hints rename to ulib/.hints/FStar.SizeT.fsti.hints diff --git a/ulib/.cache/FStar.Squash.fst.hints b/ulib/.hints/FStar.Squash.fst.hints similarity index 100% rename from ulib/.cache/FStar.Squash.fst.hints rename to ulib/.hints/FStar.Squash.fst.hints diff --git a/ulib/.cache/FStar.Squash.fsti.hints b/ulib/.hints/FStar.Squash.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Squash.fsti.hints rename to ulib/.hints/FStar.Squash.fsti.hints diff --git a/ulib/.cache/FStar.SquashProperties.fst.hints b/ulib/.hints/FStar.SquashProperties.fst.hints similarity index 100% rename from ulib/.cache/FStar.SquashProperties.fst.hints rename to ulib/.hints/FStar.SquashProperties.fst.hints diff --git a/ulib/.cache/FStar.String.fsti.hints b/ulib/.hints/FStar.String.fsti.hints similarity index 100% rename from ulib/.cache/FStar.String.fsti.hints rename to ulib/.hints/FStar.String.fsti.hints diff --git a/ulib/.cache/FStar.StrongExcludedMiddle.fst.hints b/ulib/.hints/FStar.StrongExcludedMiddle.fst.hints similarity index 100% rename from ulib/.cache/FStar.StrongExcludedMiddle.fst.hints rename to ulib/.hints/FStar.StrongExcludedMiddle.fst.hints diff --git a/ulib/.cache/FStar.Stubs.Errors.Msg.fsti.hints b/ulib/.hints/FStar.Stubs.Errors.Msg.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Errors.Msg.fsti.hints rename to ulib/.hints/FStar.Stubs.Errors.Msg.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Pprint.fsti.hints b/ulib/.hints/FStar.Stubs.Pprint.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Pprint.fsti.hints rename to ulib/.hints/FStar.Stubs.Pprint.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Reflection.Types.fsti.hints b/ulib/.hints/FStar.Stubs.Reflection.Types.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Reflection.Types.fsti.hints rename to ulib/.hints/FStar.Stubs.Reflection.Types.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Reflection.V1.Builtins.fsti.hints b/ulib/.hints/FStar.Stubs.Reflection.V1.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Reflection.V1.Builtins.fsti.hints rename to ulib/.hints/FStar.Stubs.Reflection.V1.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Reflection.V1.Data.fsti.hints b/ulib/.hints/FStar.Stubs.Reflection.V1.Data.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Reflection.V1.Data.fsti.hints rename to ulib/.hints/FStar.Stubs.Reflection.V1.Data.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Reflection.V2.Builtins.fsti.hints b/ulib/.hints/FStar.Stubs.Reflection.V2.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Reflection.V2.Builtins.fsti.hints rename to ulib/.hints/FStar.Stubs.Reflection.V2.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Reflection.V2.Data.fsti.hints b/ulib/.hints/FStar.Stubs.Reflection.V2.Data.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Reflection.V2.Data.fsti.hints rename to ulib/.hints/FStar.Stubs.Reflection.V2.Data.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Syntax.Syntax.fsti.hints b/ulib/.hints/FStar.Stubs.Syntax.Syntax.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Syntax.Syntax.fsti.hints rename to ulib/.hints/FStar.Stubs.Syntax.Syntax.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Tactics.Common.fsti.hints b/ulib/.hints/FStar.Stubs.Tactics.Common.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Tactics.Common.fsti.hints rename to ulib/.hints/FStar.Stubs.Tactics.Common.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Tactics.Result.fsti.hints b/ulib/.hints/FStar.Stubs.Tactics.Result.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Tactics.Result.fsti.hints rename to ulib/.hints/FStar.Stubs.Tactics.Result.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Tactics.Types.fsti.hints b/ulib/.hints/FStar.Stubs.Tactics.Types.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Tactics.Types.fsti.hints rename to ulib/.hints/FStar.Stubs.Tactics.Types.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Tactics.V1.Builtins.fsti.hints b/ulib/.hints/FStar.Stubs.Tactics.V1.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Tactics.V1.Builtins.fsti.hints rename to ulib/.hints/FStar.Stubs.Tactics.V1.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.Tactics.V2.Builtins.fsti.hints b/ulib/.hints/FStar.Stubs.Tactics.V2.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.Tactics.V2.Builtins.fsti.hints rename to ulib/.hints/FStar.Stubs.Tactics.V2.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Stubs.TypeChecker.Core.fsti.hints b/ulib/.hints/FStar.Stubs.TypeChecker.Core.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Stubs.TypeChecker.Core.fsti.hints rename to ulib/.hints/FStar.Stubs.TypeChecker.Core.fsti.hints diff --git a/ulib/.cache/FStar.TSet.fst.hints b/ulib/.hints/FStar.TSet.fst.hints similarity index 100% rename from ulib/.cache/FStar.TSet.fst.hints rename to ulib/.hints/FStar.TSet.fst.hints diff --git a/ulib/.cache/FStar.TSet.fsti.hints b/ulib/.hints/FStar.TSet.fsti.hints similarity index 100% rename from ulib/.cache/FStar.TSet.fsti.hints rename to ulib/.hints/FStar.TSet.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Arith.fst.hints b/ulib/.hints/FStar.Tactics.Arith.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Arith.fst.hints rename to ulib/.hints/FStar.Tactics.Arith.fst.hints diff --git a/ulib/.cache/FStar.Tactics.BV.fst.hints b/ulib/.hints/FStar.Tactics.BV.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.BV.fst.hints rename to ulib/.hints/FStar.Tactics.BV.fst.hints diff --git a/ulib/.cache/FStar.Tactics.BreakVC.fst.hints b/ulib/.hints/FStar.Tactics.BreakVC.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.BreakVC.fst.hints rename to ulib/.hints/FStar.Tactics.BreakVC.fst.hints diff --git a/ulib/.cache/FStar.Tactics.BreakVC.fsti.hints b/ulib/.hints/FStar.Tactics.BreakVC.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.BreakVC.fsti.hints rename to ulib/.hints/FStar.Tactics.BreakVC.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Builtins.fsti.hints b/ulib/.hints/FStar.Tactics.Builtins.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Builtins.fsti.hints rename to ulib/.hints/FStar.Tactics.Builtins.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Canon.fst.hints b/ulib/.hints/FStar.Tactics.Canon.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Canon.fst.hints rename to ulib/.hints/FStar.Tactics.Canon.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CanonCommMonoid.fst.hints b/ulib/.hints/FStar.Tactics.CanonCommMonoid.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CanonCommMonoid.fst.hints rename to ulib/.hints/FStar.Tactics.CanonCommMonoid.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.hints b/ulib/.hints/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.hints rename to ulib/.hints/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CanonCommMonoidSimple.fst.hints b/ulib/.hints/FStar.Tactics.CanonCommMonoidSimple.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CanonCommMonoidSimple.fst.hints rename to ulib/.hints/FStar.Tactics.CanonCommMonoidSimple.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CanonCommSemiring.fst.hints b/ulib/.hints/FStar.Tactics.CanonCommSemiring.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CanonCommSemiring.fst.hints rename to ulib/.hints/FStar.Tactics.CanonCommSemiring.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CanonCommSwaps.fst.hints b/ulib/.hints/FStar.Tactics.CanonCommSwaps.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CanonCommSwaps.fst.hints rename to ulib/.hints/FStar.Tactics.CanonCommSwaps.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CanonMonoid.fst.hints b/ulib/.hints/FStar.Tactics.CanonMonoid.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CanonMonoid.fst.hints rename to ulib/.hints/FStar.Tactics.CanonMonoid.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CheckLN.fst.hints b/ulib/.hints/FStar.Tactics.CheckLN.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CheckLN.fst.hints rename to ulib/.hints/FStar.Tactics.CheckLN.fst.hints diff --git a/ulib/.cache/FStar.Tactics.CheckLN.fsti.hints b/ulib/.hints/FStar.Tactics.CheckLN.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.CheckLN.fsti.hints rename to ulib/.hints/FStar.Tactics.CheckLN.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Common.fst.hints b/ulib/.hints/FStar.Tactics.Common.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Common.fst.hints rename to ulib/.hints/FStar.Tactics.Common.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Common.fsti.hints b/ulib/.hints/FStar.Tactics.Common.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Common.fsti.hints rename to ulib/.hints/FStar.Tactics.Common.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Derived.fst.hints b/ulib/.hints/FStar.Tactics.Derived.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Derived.fst.hints rename to ulib/.hints/FStar.Tactics.Derived.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Effect.fst.hints b/ulib/.hints/FStar.Tactics.Effect.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Effect.fst.hints rename to ulib/.hints/FStar.Tactics.Effect.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Effect.fsti.hints b/ulib/.hints/FStar.Tactics.Effect.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Effect.fsti.hints rename to ulib/.hints/FStar.Tactics.Effect.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Logic.fst.hints b/ulib/.hints/FStar.Tactics.Logic.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Logic.fst.hints rename to ulib/.hints/FStar.Tactics.Logic.fst.hints diff --git a/ulib/.cache/FStar.Tactics.MApply.fst.hints b/ulib/.hints/FStar.Tactics.MApply.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.MApply.fst.hints rename to ulib/.hints/FStar.Tactics.MApply.fst.hints diff --git a/ulib/.cache/FStar.Tactics.MApply.fsti.hints b/ulib/.hints/FStar.Tactics.MApply.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.MApply.fsti.hints rename to ulib/.hints/FStar.Tactics.MApply.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.MkProjectors.fst.hints b/ulib/.hints/FStar.Tactics.MkProjectors.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.MkProjectors.fst.hints rename to ulib/.hints/FStar.Tactics.MkProjectors.fst.hints diff --git a/ulib/.cache/FStar.Tactics.MkProjectors.fsti.hints b/ulib/.hints/FStar.Tactics.MkProjectors.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.MkProjectors.fsti.hints rename to ulib/.hints/FStar.Tactics.MkProjectors.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.NamedView.fst.hints b/ulib/.hints/FStar.Tactics.NamedView.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.NamedView.fst.hints rename to ulib/.hints/FStar.Tactics.NamedView.fst.hints diff --git a/ulib/.cache/FStar.Tactics.NamedView.fsti.hints b/ulib/.hints/FStar.Tactics.NamedView.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.NamedView.fsti.hints rename to ulib/.hints/FStar.Tactics.NamedView.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Parametricity.fst.hints b/ulib/.hints/FStar.Tactics.Parametricity.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Parametricity.fst.hints rename to ulib/.hints/FStar.Tactics.Parametricity.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Parametricity.fsti.hints b/ulib/.hints/FStar.Tactics.Parametricity.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Parametricity.fsti.hints rename to ulib/.hints/FStar.Tactics.Parametricity.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.PatternMatching.fst.hints b/ulib/.hints/FStar.Tactics.PatternMatching.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.PatternMatching.fst.hints rename to ulib/.hints/FStar.Tactics.PatternMatching.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Print.fst.hints b/ulib/.hints/FStar.Tactics.Print.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Print.fst.hints rename to ulib/.hints/FStar.Tactics.Print.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Result.fst.hints b/ulib/.hints/FStar.Tactics.Result.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Result.fst.hints rename to ulib/.hints/FStar.Tactics.Result.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Result.fsti.hints b/ulib/.hints/FStar.Tactics.Result.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Result.fsti.hints rename to ulib/.hints/FStar.Tactics.Result.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.SMT.fst.hints b/ulib/.hints/FStar.Tactics.SMT.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.SMT.fst.hints rename to ulib/.hints/FStar.Tactics.SMT.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Simplifier.fst.hints b/ulib/.hints/FStar.Tactics.Simplifier.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Simplifier.fst.hints rename to ulib/.hints/FStar.Tactics.Simplifier.fst.hints diff --git a/ulib/.cache/FStar.Tactics.SyntaxHelpers.fst.hints b/ulib/.hints/FStar.Tactics.SyntaxHelpers.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.SyntaxHelpers.fst.hints rename to ulib/.hints/FStar.Tactics.SyntaxHelpers.fst.hints diff --git a/ulib/.cache/FStar.Tactics.TypeRepr.fst.hints b/ulib/.hints/FStar.Tactics.TypeRepr.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.TypeRepr.fst.hints rename to ulib/.hints/FStar.Tactics.TypeRepr.fst.hints diff --git a/ulib/.cache/FStar.Tactics.TypeRepr.fsti.hints b/ulib/.hints/FStar.Tactics.TypeRepr.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.TypeRepr.fsti.hints rename to ulib/.hints/FStar.Tactics.TypeRepr.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Typeclasses.fst.hints b/ulib/.hints/FStar.Tactics.Typeclasses.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Typeclasses.fst.hints rename to ulib/.hints/FStar.Tactics.Typeclasses.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Typeclasses.fsti.hints b/ulib/.hints/FStar.Tactics.Typeclasses.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Typeclasses.fsti.hints rename to ulib/.hints/FStar.Tactics.Typeclasses.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Types.fsti.hints b/ulib/.hints/FStar.Tactics.Types.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Types.fsti.hints rename to ulib/.hints/FStar.Tactics.Types.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Unseal.fsti.hints b/ulib/.hints/FStar.Tactics.Unseal.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Unseal.fsti.hints rename to ulib/.hints/FStar.Tactics.Unseal.fsti.hints diff --git a/ulib/.cache/FStar.Tactics.Util.fst.hints b/ulib/.hints/FStar.Tactics.Util.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Util.fst.hints rename to ulib/.hints/FStar.Tactics.Util.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V1.Derived.fst.hints b/ulib/.hints/FStar.Tactics.V1.Derived.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V1.Derived.fst.hints rename to ulib/.hints/FStar.Tactics.V1.Derived.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V1.Logic.fst.hints b/ulib/.hints/FStar.Tactics.V1.Logic.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V1.Logic.fst.hints rename to ulib/.hints/FStar.Tactics.V1.Logic.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V1.SyntaxHelpers.fst.hints b/ulib/.hints/FStar.Tactics.V1.SyntaxHelpers.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V1.SyntaxHelpers.fst.hints rename to ulib/.hints/FStar.Tactics.V1.SyntaxHelpers.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V1.fst.hints b/ulib/.hints/FStar.Tactics.V1.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V1.fst.hints rename to ulib/.hints/FStar.Tactics.V1.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V2.Derived.fst.hints b/ulib/.hints/FStar.Tactics.V2.Derived.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V2.Derived.fst.hints rename to ulib/.hints/FStar.Tactics.V2.Derived.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V2.Logic.fst.hints b/ulib/.hints/FStar.Tactics.V2.Logic.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V2.Logic.fst.hints rename to ulib/.hints/FStar.Tactics.V2.Logic.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V2.SyntaxCoercions.fst.hints b/ulib/.hints/FStar.Tactics.V2.SyntaxCoercions.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V2.SyntaxCoercions.fst.hints rename to ulib/.hints/FStar.Tactics.V2.SyntaxCoercions.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V2.SyntaxHelpers.fst.hints b/ulib/.hints/FStar.Tactics.V2.SyntaxHelpers.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V2.SyntaxHelpers.fst.hints rename to ulib/.hints/FStar.Tactics.V2.SyntaxHelpers.fst.hints diff --git a/ulib/.cache/FStar.Tactics.V2.fst.hints b/ulib/.hints/FStar.Tactics.V2.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.V2.fst.hints rename to ulib/.hints/FStar.Tactics.V2.fst.hints diff --git a/ulib/.cache/FStar.Tactics.Visit.fst.hints b/ulib/.hints/FStar.Tactics.Visit.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.Visit.fst.hints rename to ulib/.hints/FStar.Tactics.Visit.fst.hints diff --git a/ulib/.cache/FStar.Tactics.fst.hints b/ulib/.hints/FStar.Tactics.fst.hints similarity index 100% rename from ulib/.cache/FStar.Tactics.fst.hints rename to ulib/.hints/FStar.Tactics.fst.hints diff --git a/ulib/.cache/FStar.TaggedUnion.fst.hints b/ulib/.hints/FStar.TaggedUnion.fst.hints similarity index 100% rename from ulib/.cache/FStar.TaggedUnion.fst.hints rename to ulib/.hints/FStar.TaggedUnion.fst.hints diff --git a/ulib/.cache/FStar.TaggedUnion.fsti.hints b/ulib/.hints/FStar.TaggedUnion.fsti.hints similarity index 100% rename from ulib/.cache/FStar.TaggedUnion.fsti.hints rename to ulib/.hints/FStar.TaggedUnion.fsti.hints diff --git a/ulib/.cache/FStar.Tcp.fsti.hints b/ulib/.hints/FStar.Tcp.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Tcp.fsti.hints rename to ulib/.hints/FStar.Tcp.fsti.hints diff --git a/ulib/.cache/FStar.TwoLevelHeap.fst.hints b/ulib/.hints/FStar.TwoLevelHeap.fst.hints similarity index 100% rename from ulib/.cache/FStar.TwoLevelHeap.fst.hints rename to ulib/.hints/FStar.TwoLevelHeap.fst.hints diff --git a/ulib/.cache/FStar.UInt.fst.hints b/ulib/.hints/FStar.UInt.fst.hints similarity index 100% rename from ulib/.cache/FStar.UInt.fst.hints rename to ulib/.hints/FStar.UInt.fst.hints diff --git a/ulib/.cache/FStar.UInt.fsti.hints b/ulib/.hints/FStar.UInt.fsti.hints similarity index 100% rename from ulib/.cache/FStar.UInt.fsti.hints rename to ulib/.hints/FStar.UInt.fsti.hints diff --git a/ulib/.cache/FStar.UInt128.fst.hints b/ulib/.hints/FStar.UInt128.fst.hints similarity index 100% rename from ulib/.cache/FStar.UInt128.fst.hints rename to ulib/.hints/FStar.UInt128.fst.hints diff --git a/ulib/.cache/FStar.UInt128.fsti.hints b/ulib/.hints/FStar.UInt128.fsti.hints similarity index 100% rename from ulib/.cache/FStar.UInt128.fsti.hints rename to ulib/.hints/FStar.UInt128.fsti.hints diff --git a/ulib/.cache/FStar.UInt16.fst.hints b/ulib/.hints/FStar.UInt16.fst.hints similarity index 100% rename from ulib/.cache/FStar.UInt16.fst.hints rename to ulib/.hints/FStar.UInt16.fst.hints diff --git a/ulib/.cache/FStar.UInt16.fsti.hints b/ulib/.hints/FStar.UInt16.fsti.hints similarity index 100% rename from ulib/.cache/FStar.UInt16.fsti.hints rename to ulib/.hints/FStar.UInt16.fsti.hints diff --git a/ulib/.cache/FStar.UInt32.fst.hints b/ulib/.hints/FStar.UInt32.fst.hints similarity index 100% rename from ulib/.cache/FStar.UInt32.fst.hints rename to ulib/.hints/FStar.UInt32.fst.hints diff --git a/ulib/.cache/FStar.UInt32.fsti.hints b/ulib/.hints/FStar.UInt32.fsti.hints similarity index 100% rename from ulib/.cache/FStar.UInt32.fsti.hints rename to ulib/.hints/FStar.UInt32.fsti.hints diff --git a/ulib/.cache/FStar.UInt64.fst.hints b/ulib/.hints/FStar.UInt64.fst.hints similarity index 100% rename from ulib/.cache/FStar.UInt64.fst.hints rename to ulib/.hints/FStar.UInt64.fst.hints diff --git a/ulib/.cache/FStar.UInt64.fsti.hints b/ulib/.hints/FStar.UInt64.fsti.hints similarity index 100% rename from ulib/.cache/FStar.UInt64.fsti.hints rename to ulib/.hints/FStar.UInt64.fsti.hints diff --git a/ulib/.cache/FStar.UInt8.fst.hints b/ulib/.hints/FStar.UInt8.fst.hints similarity index 100% rename from ulib/.cache/FStar.UInt8.fst.hints rename to ulib/.hints/FStar.UInt8.fst.hints diff --git a/ulib/.cache/FStar.UInt8.fsti.hints b/ulib/.hints/FStar.UInt8.fsti.hints similarity index 100% rename from ulib/.cache/FStar.UInt8.fsti.hints rename to ulib/.hints/FStar.UInt8.fsti.hints diff --git a/ulib/.cache/FStar.Udp.fsti.hints b/ulib/.hints/FStar.Udp.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Udp.fsti.hints rename to ulib/.hints/FStar.Udp.fsti.hints diff --git a/ulib/.cache/FStar.Universe.PCM.fst.hints b/ulib/.hints/FStar.Universe.PCM.fst.hints similarity index 100% rename from ulib/.cache/FStar.Universe.PCM.fst.hints rename to ulib/.hints/FStar.Universe.PCM.fst.hints diff --git a/ulib/.cache/FStar.Universe.fst.hints b/ulib/.hints/FStar.Universe.fst.hints similarity index 100% rename from ulib/.cache/FStar.Universe.fst.hints rename to ulib/.hints/FStar.Universe.fst.hints diff --git a/ulib/.cache/FStar.Universe.fsti.hints b/ulib/.hints/FStar.Universe.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Universe.fsti.hints rename to ulib/.hints/FStar.Universe.fsti.hints diff --git a/ulib/.cache/FStar.Util.fst.hints b/ulib/.hints/FStar.Util.fst.hints similarity index 100% rename from ulib/.cache/FStar.Util.fst.hints rename to ulib/.hints/FStar.Util.fst.hints diff --git a/ulib/.cache/FStar.VConfig.fsti.hints b/ulib/.hints/FStar.VConfig.fsti.hints similarity index 100% rename from ulib/.cache/FStar.VConfig.fsti.hints rename to ulib/.hints/FStar.VConfig.fsti.hints diff --git a/ulib/.cache/FStar.Vector.Base.fst.hints b/ulib/.hints/FStar.Vector.Base.fst.hints similarity index 100% rename from ulib/.cache/FStar.Vector.Base.fst.hints rename to ulib/.hints/FStar.Vector.Base.fst.hints diff --git a/ulib/.cache/FStar.Vector.Base.fsti.hints b/ulib/.hints/FStar.Vector.Base.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Vector.Base.fsti.hints rename to ulib/.hints/FStar.Vector.Base.fsti.hints diff --git a/ulib/.cache/FStar.Vector.Properties.fst.hints b/ulib/.hints/FStar.Vector.Properties.fst.hints similarity index 100% rename from ulib/.cache/FStar.Vector.Properties.fst.hints rename to ulib/.hints/FStar.Vector.Properties.fst.hints diff --git a/ulib/.cache/FStar.Vector.fst.hints b/ulib/.hints/FStar.Vector.fst.hints similarity index 100% rename from ulib/.cache/FStar.Vector.fst.hints rename to ulib/.hints/FStar.Vector.fst.hints diff --git a/ulib/.cache/FStar.WellFounded.Util.fst.hints b/ulib/.hints/FStar.WellFounded.Util.fst.hints similarity index 100% rename from ulib/.cache/FStar.WellFounded.Util.fst.hints rename to ulib/.hints/FStar.WellFounded.Util.fst.hints diff --git a/ulib/.cache/FStar.WellFounded.Util.fsti.hints b/ulib/.hints/FStar.WellFounded.Util.fsti.hints similarity index 100% rename from ulib/.cache/FStar.WellFounded.Util.fsti.hints rename to ulib/.hints/FStar.WellFounded.Util.fsti.hints diff --git a/ulib/.cache/FStar.WellFounded.fst.hints b/ulib/.hints/FStar.WellFounded.fst.hints similarity index 100% rename from ulib/.cache/FStar.WellFounded.fst.hints rename to ulib/.hints/FStar.WellFounded.fst.hints diff --git a/ulib/.cache/FStar.WellFoundedRelation.fst.hints b/ulib/.hints/FStar.WellFoundedRelation.fst.hints similarity index 100% rename from ulib/.cache/FStar.WellFoundedRelation.fst.hints rename to ulib/.hints/FStar.WellFoundedRelation.fst.hints diff --git a/ulib/.cache/FStar.WellFoundedRelation.fsti.hints b/ulib/.hints/FStar.WellFoundedRelation.fsti.hints similarity index 100% rename from ulib/.cache/FStar.WellFoundedRelation.fsti.hints rename to ulib/.hints/FStar.WellFoundedRelation.fsti.hints diff --git a/ulib/.cache/FStar.Witnessed.Core.fst.hints b/ulib/.hints/FStar.Witnessed.Core.fst.hints similarity index 100% rename from ulib/.cache/FStar.Witnessed.Core.fst.hints rename to ulib/.hints/FStar.Witnessed.Core.fst.hints diff --git a/ulib/.cache/FStar.Witnessed.Core.fsti.hints b/ulib/.hints/FStar.Witnessed.Core.fsti.hints similarity index 100% rename from ulib/.cache/FStar.Witnessed.Core.fsti.hints rename to ulib/.hints/FStar.Witnessed.Core.fsti.hints diff --git a/ulib/.cache/LowStar.Buffer.fst.hints b/ulib/.hints/LowStar.Buffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Buffer.fst.hints rename to ulib/.hints/LowStar.Buffer.fst.hints diff --git a/ulib/.cache/LowStar.BufferCompat.fst.hints b/ulib/.hints/LowStar.BufferCompat.fst.hints similarity index 100% rename from ulib/.cache/LowStar.BufferCompat.fst.hints rename to ulib/.hints/LowStar.BufferCompat.fst.hints diff --git a/ulib/.cache/LowStar.BufferOps.fst.hints b/ulib/.hints/LowStar.BufferOps.fst.hints similarity index 100% rename from ulib/.cache/LowStar.BufferOps.fst.hints rename to ulib/.hints/LowStar.BufferOps.fst.hints diff --git a/ulib/.cache/LowStar.BufferView.Down.fst.hints b/ulib/.hints/LowStar.BufferView.Down.fst.hints similarity index 100% rename from ulib/.cache/LowStar.BufferView.Down.fst.hints rename to ulib/.hints/LowStar.BufferView.Down.fst.hints diff --git a/ulib/.cache/LowStar.BufferView.Down.fsti.hints b/ulib/.hints/LowStar.BufferView.Down.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.BufferView.Down.fsti.hints rename to ulib/.hints/LowStar.BufferView.Down.fsti.hints diff --git a/ulib/.cache/LowStar.BufferView.Up.fst.hints b/ulib/.hints/LowStar.BufferView.Up.fst.hints similarity index 100% rename from ulib/.cache/LowStar.BufferView.Up.fst.hints rename to ulib/.hints/LowStar.BufferView.Up.fst.hints diff --git a/ulib/.cache/LowStar.BufferView.Up.fsti.hints b/ulib/.hints/LowStar.BufferView.Up.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.BufferView.Up.fsti.hints rename to ulib/.hints/LowStar.BufferView.Up.fsti.hints diff --git a/ulib/.cache/LowStar.BufferView.fst.hints b/ulib/.hints/LowStar.BufferView.fst.hints similarity index 100% rename from ulib/.cache/LowStar.BufferView.fst.hints rename to ulib/.hints/LowStar.BufferView.fst.hints diff --git a/ulib/.cache/LowStar.BufferView.fsti.hints b/ulib/.hints/LowStar.BufferView.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.BufferView.fsti.hints rename to ulib/.hints/LowStar.BufferView.fsti.hints diff --git a/ulib/.cache/LowStar.Comment.fst.hints b/ulib/.hints/LowStar.Comment.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Comment.fst.hints rename to ulib/.hints/LowStar.Comment.fst.hints diff --git a/ulib/.cache/LowStar.Comment.fsti.hints b/ulib/.hints/LowStar.Comment.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.Comment.fsti.hints rename to ulib/.hints/LowStar.Comment.fsti.hints diff --git a/ulib/.cache/LowStar.ConstBuffer.fst.hints b/ulib/.hints/LowStar.ConstBuffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.ConstBuffer.fst.hints rename to ulib/.hints/LowStar.ConstBuffer.fst.hints diff --git a/ulib/.cache/LowStar.ConstBuffer.fsti.hints b/ulib/.hints/LowStar.ConstBuffer.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.ConstBuffer.fsti.hints rename to ulib/.hints/LowStar.ConstBuffer.fsti.hints diff --git a/ulib/.cache/LowStar.Endianness.fst.hints b/ulib/.hints/LowStar.Endianness.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Endianness.fst.hints rename to ulib/.hints/LowStar.Endianness.fst.hints diff --git a/ulib/.cache/LowStar.Failure.fsti.hints b/ulib/.hints/LowStar.Failure.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.Failure.fsti.hints rename to ulib/.hints/LowStar.Failure.fsti.hints diff --git a/ulib/.cache/LowStar.Ignore.fsti.hints b/ulib/.hints/LowStar.Ignore.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.Ignore.fsti.hints rename to ulib/.hints/LowStar.Ignore.fsti.hints diff --git a/ulib/.cache/LowStar.ImmutableBuffer.fst.hints b/ulib/.hints/LowStar.ImmutableBuffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.ImmutableBuffer.fst.hints rename to ulib/.hints/LowStar.ImmutableBuffer.fst.hints diff --git a/ulib/.cache/LowStar.Lens.Buffer.fst.hints b/ulib/.hints/LowStar.Lens.Buffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Lens.Buffer.fst.hints rename to ulib/.hints/LowStar.Lens.Buffer.fst.hints diff --git a/ulib/.cache/LowStar.Lens.Tuple2.fst.hints b/ulib/.hints/LowStar.Lens.Tuple2.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Lens.Tuple2.fst.hints rename to ulib/.hints/LowStar.Lens.Tuple2.fst.hints diff --git a/ulib/.cache/LowStar.Lens.fst.hints b/ulib/.hints/LowStar.Lens.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Lens.fst.hints rename to ulib/.hints/LowStar.Lens.fst.hints diff --git a/ulib/.cache/LowStar.Literal.fsti.hints b/ulib/.hints/LowStar.Literal.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.Literal.fsti.hints rename to ulib/.hints/LowStar.Literal.fsti.hints diff --git a/ulib/.cache/LowStar.Modifies.fst.hints b/ulib/.hints/LowStar.Modifies.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Modifies.fst.hints rename to ulib/.hints/LowStar.Modifies.fst.hints diff --git a/ulib/.cache/LowStar.ModifiesPat.fst.hints b/ulib/.hints/LowStar.ModifiesPat.fst.hints similarity index 100% rename from ulib/.cache/LowStar.ModifiesPat.fst.hints rename to ulib/.hints/LowStar.ModifiesPat.fst.hints diff --git a/ulib/.cache/LowStar.Monotonic.Buffer.fst.hints b/ulib/.hints/LowStar.Monotonic.Buffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Monotonic.Buffer.fst.hints rename to ulib/.hints/LowStar.Monotonic.Buffer.fst.hints diff --git a/ulib/.cache/LowStar.Monotonic.Buffer.fsti.hints b/ulib/.hints/LowStar.Monotonic.Buffer.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.Monotonic.Buffer.fsti.hints rename to ulib/.hints/LowStar.Monotonic.Buffer.fsti.hints diff --git a/ulib/.cache/LowStar.PrefixFreezableBuffer.fst.hints b/ulib/.hints/LowStar.PrefixFreezableBuffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.PrefixFreezableBuffer.fst.hints rename to ulib/.hints/LowStar.PrefixFreezableBuffer.fst.hints diff --git a/ulib/.cache/LowStar.PrefixFreezableBuffer.fsti.hints b/ulib/.hints/LowStar.PrefixFreezableBuffer.fsti.hints similarity index 100% rename from ulib/.cache/LowStar.PrefixFreezableBuffer.fsti.hints rename to ulib/.hints/LowStar.PrefixFreezableBuffer.fsti.hints diff --git a/ulib/.cache/LowStar.Printf.fst.hints b/ulib/.hints/LowStar.Printf.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Printf.fst.hints rename to ulib/.hints/LowStar.Printf.fst.hints diff --git a/ulib/.cache/LowStar.RVector.fst.hints b/ulib/.hints/LowStar.RVector.fst.hints similarity index 100% rename from ulib/.cache/LowStar.RVector.fst.hints rename to ulib/.hints/LowStar.RVector.fst.hints diff --git a/ulib/.cache/LowStar.Regional.Instances.fst.hints b/ulib/.hints/LowStar.Regional.Instances.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Regional.Instances.fst.hints rename to ulib/.hints/LowStar.Regional.Instances.fst.hints diff --git a/ulib/.cache/LowStar.Regional.fst.hints b/ulib/.hints/LowStar.Regional.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Regional.fst.hints rename to ulib/.hints/LowStar.Regional.fst.hints diff --git a/ulib/.cache/LowStar.ToFStarBuffer.fst.hints b/ulib/.hints/LowStar.ToFStarBuffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.ToFStarBuffer.fst.hints rename to ulib/.hints/LowStar.ToFStarBuffer.fst.hints diff --git a/ulib/.cache/LowStar.UninitializedBuffer.fst.hints b/ulib/.hints/LowStar.UninitializedBuffer.fst.hints similarity index 100% rename from ulib/.cache/LowStar.UninitializedBuffer.fst.hints rename to ulib/.hints/LowStar.UninitializedBuffer.fst.hints diff --git a/ulib/.cache/LowStar.Vector.fst.hints b/ulib/.hints/LowStar.Vector.fst.hints similarity index 100% rename from ulib/.cache/LowStar.Vector.fst.hints rename to ulib/.hints/LowStar.Vector.fst.hints diff --git a/ulib/.cache/prims.fst.hints b/ulib/.hints/prims.fst.hints similarity index 100% rename from ulib/.cache/prims.fst.hints rename to ulib/.hints/prims.fst.hints diff --git a/ulib/Makefile.verify b/ulib/Makefile.verify index 6897c05601a..43143b765c0 100644 --- a/ulib/Makefile.verify +++ b/ulib/Makefile.verify @@ -28,7 +28,7 @@ FSTAR_FILES += $(filter-out $(FLAKY), \ endif endif -WITH_CACHE_DIR=--cache_dir .cache --hint_dir .cache +WITH_CACHE_DIR=--cache_dir .cache --hint_dir .hints # 271 -> pattern uses theory symbols # 330 -> experimental feature