

@2677

8 years 
campbell 
Retain the pointer for the function called in frontend call states
so …



@2428

8 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2391

8 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2353

8 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@1713

9 years 
campbell 
Add a distinguished final state to the frontend languages to match up …



@1605

9 years 
sacerdot 
Porting to last standard library of Matita.



@1566

9 years 
campbell 
Pacify changes to destruct tactic.



@1521

9 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1510

9 years 
sacerdot 
All files ported to new dependent inversion.



@1352

9 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1350

9 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1344

9 years 
sacerdot 
Ported to new destruct.



@1244

9 years 
campbell 
Sort out Clight semantics equivalence proof for new SmallstepExec?.



@1216

9 years 
campbell 
Update Clight semantics equivalence proof to match changes in …



@961

9 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@891

9 years 
campbell 
Revise proofs affected by recent matita change.



@798

9 years 
campbell 
Fix usual matita tactic mistake.



@797

9 years 
campbell 
Add error messages wherever the error monad is used.
Sticks to …



@732

9 years 
campbell 
Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma



@708

10 years 
campbell 
Use a more normalizefriendly definition of clight_exec to make the …



@702

10 years 
campbell 
Refine smallstep executable semantics abstraction a little.
Some …



@700

10 years 
campbell 
Get Clight semantics going again (except for problems CexecEquiv? that …



@694

10 years 
campbell 
Start moving Clight into common directory.


copied from Deliverables/D3.1/Csemantics/CexecEquiv.ma:



@487

10 years 
campbell 
Port Clight semantics to the newnew matita syntax.
