Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
29 November 2022, 16:31:34 UTC
Revision 9f4a2f7c153fe8a1566c8c0ff1bd796083ef587a authored by Pierre-Yves Strub on 03 November 2022, 05:50:59 UTC, committed by Pierre-Yves Strub on 07 November 2022, 20:30:11 UTC 
[ec-runtest]: add the possibility to exclude file based on the name
 
The entry is `file_exclude`. It is a space-separated list of
globs. A file is excluded if its basename matches any of the glob.

See `fnmatch.fnmatch` of the standard Python libraries to get a
description of which glob patterns are supported.

Fix #303
1 parent 8d4e67d
Raw File
Tip revision: 9f4a2f7c153fe8a1566c8c0ff1bd796083ef587a authored by Pierre-Yves Strub on 03 November 2022, 05:50:59 UTC
[ec-runtest]: add the possibility to exclude file based on the name
Tip revision: 9f4a2f7
ecTheoryReplay.mli 
(* ------------------------------------------------------------------ *)
open EcSymbols
open EcPath
open EcParsetree
open EcTheory
open EcThCloning

(* ------------------------------------------------------------------ *)
type ovoptions = {
  clo_abstract : bool;
}

type 'a ovrenv = {
  ovre_ovrd     : EcThCloning.evclone;
  ovre_rnms     : EcThCloning.renaming list;
  ovre_ntclr    : EcPath.Sp.t;
  ovre_opath    : EcPath.path;
  ovre_npath    : EcPath.path;
  ovre_prefix   : (symbol list) EcUtils.pair;
  ovre_glproof  : (ptactic_core option * evtags option) list;
  ovre_abstract : bool;
  ovre_local    : EcTypes.is_local;
  ovre_hooks    : 'a ovrhooks;
}

and 'a ovrhooks = {
  henv      : 'a -> EcSection.scenv;
  hadd_item : 'a -> EcTheory.import -> EcTheory.theory_item_r -> 'a;
  hthenter  : 'a -> thmode -> symbol -> EcTypes.is_local -> 'a;
  hthexit   : 'a -> [`Full | `ClearOnly | `No] -> 'a;
  herr      : 'b . ?loc:EcLocation.t -> string -> 'b;
}

(* -------------------------------------------------------------------- *)
val replay : 'a ovrhooks
  -> abstract:bool -> local:is_local -> incl:bool
  -> clears:Sp.t -> renames:(renaming list)
  -> opath:path -> npath:path -> evclone
  -> 'a -> symbol * theory_item list
  ->  axclone list * 'a
back to top