-
Jacques-Henri Jourdan authoredJacques-Henri Jourdan authored
_CoqProject 3.63 KiB
-Q theories lrust
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-arg -mangle-names -arg _
theories/util/basic.v
theories/util/vector.v
theories/util/update.v
theories/util/discrete_fun.v
theories/util/fancy_lists.v
theories/prophecy/syn_type.v
theories/prophecy/prophecy.v
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
theories/lifetime/model/creation.v
theories/lifetime/model/primitive.v
theories/lifetime/model/accessors.v
theories/lifetime/model/borrow.v
theories/lifetime/model/borrow_sep.v
theories/lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v
theories/lifetime/lifetime.v
theories/lifetime/at_borrow.v
theories/lifetime/na_borrow.v
theories/lifetime/frac_borrow.v
theories/lang/adequacy.v
theories/lang/heap.v
theories/lang/time.v
theories/lang/lang.v
theories/lang/lifting.v
theories/lang/notation.v
theories/lang/proofmode.v
theories/lang/races.v
theories/lang/tactics.v
theories/lang/lib/memcpy.v
theories/lang/lib/swap.v
theories/lang/lib/new_delete.v
theories/lang/lib/spawn.v
theories/lang/lib/lock.v
theories/lang/lib/tests.v
theories/typing/base.v
theories/typing/uniq_cmra.v
theories/typing/type.v
theories/typing/lft_contexts.v
theories/typing/type_context.v
theories/typing/cont_context.v
theories/typing/uninit.v
theories/typing/base_type.v
theories/typing/mod_ty.v
theories/typing/refined.v
theories/typing/own.v
theories/typing/uniq_util.v
theories/typing/uniq_bor.v
theories/typing/shr_bor.v
theories/typing/product.v
theories/typing/product_split.v
theories/typing/sum.v
theories/typing/array_util.v
theories/typing/array.v
theories/typing/array_idx.v
theories/typing/bool.v
theories/typing/int.v
theories/typing/function.v
theories/typing/programs.v
theories/typing/borrow.v
theories/typing/cont.v
theories/typing/fixpoint.v
theories/typing/type_sum.v
theories/typing/typing.v
theories/typing/soundness.v
theories/typing/uniq_array_util.v
theories/typing/lib/gfp.v
theories/typing/lib/panic.v
theories/typing/lib/loop.v
theories/typing/lib/option.v
theories/typing/lib/list.v
theories/typing/lib/maybe_uninit.v
theories/typing/lib/vec_util.v
theories/typing/lib/slice/slice.v
theories/typing/lib/slice/slice_basic.v
theories/typing/lib/slice/array_slice.v
theories/typing/lib/slice/slice_split.v
theories/typing/lib/slice/iter.v
theories/typing/lib/vec/vec.v
theories/typing/lib/vec/vec_basic.v
theories/typing/lib/vec/vec_slice.v
theories/typing/lib/vec/vec_index.v
theories/typing/lib/vec/vec_pushpop.v
theories/typing/lib/smallvec/smallvec.v
theories/typing/lib/smallvec/smallvec_basic.v
theories/typing/lib/smallvec/smallvec_slice.v
theories/typing/lib/smallvec/smallvec_index.v
theories/typing/lib/smallvec/smallvec_push.v
theories/typing/lib/smallvec/smallvec_pop.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
theories/typing/lib/swap.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
theories/typing/examples/inc_max.v
theories/typing/examples/odd_sum.v
theories/typing/examples/projection_toggle.v
theories/typing/examples/take_some_list.v
theories/typing/examples/get_sum_list.v
theories/typing/examples/inc_some_list.v
theories/typing/examples/split_uniq_list.v
theories/typing/examples/inc_vec.v
theories/typing/examples/inc_cell.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
theories/typing/examples/init_prod.v
theories/typing/examples/lazy_lft.v
theories/typing/examples/derived_rules.v