diff options
| author | Emilio Jesus Gallego Arias | 2017-11-19 05:11:18 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-19 17:42:48 +0100 |
| commit | 094b577f61f105f0a92f3f84d7e739884dd993a7 (patch) | |
| tree | 33b39e64d139d2079734a84359707c2fa12451c3 /parsing | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
[parser] Remove unnecessary statically initialized hook.
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
2 files changed, 1 insertions, 7 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index d51b8b54e5..7f50fd22ac 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -440,7 +440,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CNotation (notation , env) | ForPattern -> fun notation loc env -> let invalid = List.exists (fun (_, b) -> not b) env.binders in - let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in + let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in CAst.make ~loc @@ CPatNotation (notation, env, []) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a5b58b8553..82306bb9f5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -129,12 +129,6 @@ let test_plural_form_types loc kwd = function warn_plural_command ~loc:!@loc kwd | _ -> () -let fresh_var env c = - Namegen.next_ident_away (Id.of_string "pat") - (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env) - -let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var - (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion |