diff options
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r-- | interp/topconstr.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index abdde1f54..dd656d479 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -20,7 +20,7 @@ open Constrexpr_ops let oldfashion_patterns = ref (true) -let write_oldfashion_patterns = Goptions.declare_bool_option { +let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments"; @@ -244,18 +244,6 @@ let rec replace_vars_constr_expr l = function | c -> map_constr_expr_with_binders List.remove_assoc replace_vars_constr_expr l c -(**********************************************************************) -(* Concrete syntax for modules and modules types *) - -type with_declaration_ast = - | CWith_Module of identifier list Loc.located * qualid Loc.located - | CWith_Definition of identifier list Loc.located * constr_expr - -type module_ast = - | CMident of qualid Loc.located - | CMapply of Loc.t * module_ast * module_ast - | CMwith of Loc.t * module_ast * with_declaration_ast - (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) |