diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-11 21:40:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-14 18:23:32 +0100 |
| commit | 67b9b34d409c793dc449104525684852353ee064 (patch) | |
| tree | 50a061e5cbaea7507c226d94d33fdfc5d10bc5ee /tactics/tacsubst.ml | |
| parent | 00e27eac9fe207d754952c1ddb0e12861ee293c9 (diff) | |
Removing ident and var generic arguments.
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 754c88620..0061237bf 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -276,9 +276,6 @@ and subst_match_rule subst = function and subst_genarg subst (x:glob_generic_argument) = match genarg_tag x with - | IdentArgType -> - in_gen (glbwit wit_ident) (out_gen (glbwit wit_ident) x) - | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x) | ConstrArgType -> in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x)) | ListArgType _ -> @@ -314,6 +311,8 @@ and subst_genarg subst (x:glob_generic_argument) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_ident (fun _ v -> v); + Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); Genintern.register_subst0 wit_tactic subst_tactic; Genintern.register_subst0 wit_sort (fun _ v -> v); |