Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
05 April 2024, 19:20:55 UTC
Revision 28694ef3e50aebb542df1881769aa41ad7fad77f authored by Pierre-Yves Strub on 19 August 2015, 19:27:18 UTC, committed by Pierre-Yves Strub on 19 August 2015, 19:27:18 UTC 
New vernacular command: `dump`
 
`dump "filename" (tactic)` aims at dumping to

  - filename.ec: the tactic executed
  - filename.0.ec: the initial goal
  - filename.$i.ec: the i-th goal after application of the tactic

In interactive mode (i.e. with stdin at its input), the tactic raw-text
cannot be read back and `filename.ec` is empty.

WARN: the generation of `filename.$i.ec` is not yet working.
1 parent de23cab
Raw File
Tip revision: 28694ef3e50aebb542df1881769aa41ad7fad77f authored by Pierre-Yves Strub on 19 August 2015, 19:27:18 UTC
New vernacular command: `dump`
Tip revision: 28694ef
COPYRIGHT.yaml 
entities:
  IMDEA : "IMDEA Software Institute"
  INRIA : "Inria"
copyrights:
  - pattern: ["src/*.ml*", "src/*/*.ml*"]
    style: "ocaml"
    license: "CeCILL-C-V1"
    copyrights:
      - { who: "IMDEA", date: "2012--2015" }
      - { who: "INRIA", date: "2012--2015" }
  - pattern: ["theories/*.ec", "theories/*/*.ec*"]
    style: "ocaml"
    license: "CeCILL-B-V1"
    copyrights:
      - { who: "IMDEA", date: "2012--2015" }
      - { who: "INRIA", date: "2012--2015" }
back to top