diff options
Diffstat (limited to 'contrib/subtac/sast.ml')
| -rw-r--r-- | contrib/subtac/sast.ml | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/contrib/subtac/sast.ml b/contrib/subtac/sast.ml deleted file mode 100644 index 4d0ca759d..000000000 --- a/contrib/subtac/sast.ml +++ /dev/null @@ -1,25 +0,0 @@ -open Names -open Util - -type const = CNat of int | CInt of int | CBool of bool - -type term = - SIdent of identifier located - | SLambda of (identifier located * type_ located) * term located - | SApp of term located * term located - | SLetIn of (name located) * (term located) * term located - | SLetTuple of (name located) list * term located * term located - | SIfThenElse of (term located) * (term located) * (term located) - | SSumInf of (term located) * (term located) - | SSumDep of (identifier located * term located) * (term located * type_ located) -and lettuple_el = (identifier located) option * term_loc * type_loc option -and term_loc = term located -and type_ = - | TApp of type_loc * type_loc - | TPi of (name located * type_loc) * type_loc - | TSigma of (name located * type_loc) * type_loc - | TSubset of (identifier located * type_loc) * type_loc - | TIdent of identifier located - | TTerm of term_loc - -and type_loc = type_ located |