Skip to content

Commit

Permalink
WIP import griotte
Browse files Browse the repository at this point in the history
  • Loading branch information
JuneRousseau committed Jan 16, 2025
1 parent d7be2f8 commit edf82ba
Show file tree
Hide file tree
Showing 31 changed files with 6,178 additions and 6,524 deletions.
8 changes: 7 additions & 1 deletion _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,13 @@ theories/proofmode/proofmode_instr_rules.v
theories/proofmode/proofmode.v
theories/proofmode/register_tactics.v

# MCerise
theories/sts.v
theories/region_invariants.v
theories/region_invariants_transitions.v
theories/monotone.v


# Unary Logical Relation
theories/seal_store.v
theories/logrel.v
Expand All @@ -81,7 +88,6 @@ theories/ftlr/UnSeal.v
theories/fundamental.v

# Misc for examples
theories/monotone.v
theories/examples/addr_reg_sample.v
theories/proofmode/disjoint_regions_tactics.v
theories/proofmode/mkregion_helpers.v
Expand Down
3 changes: 2 additions & 1 deletion theories/examples/macros/macros.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ From iris.proofmode Require Import proofmode.
Require Import Eqdep_dec List.
From cap_machine Require Import rules logrel.
From cap_machine.proofmode Require Import tactics_helpers map_simpl solve_pure.
From cap_machine Require Export iris_extra addr_reg_sample contiguous malloc assert.
From cap_machine Require Export iris_extra addr_reg_sample contiguous.
From cap_machine Require Export malloc assert.

Section macros.
Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
Expand Down
255 changes: 0 additions & 255 deletions theories/exercises/cerise_modularity.v

This file was deleted.

Loading

0 comments on commit edf82ba

Please sign in to comment.