diff options
| author | Pierre-Marie Pédrot | 2013-12-19 20:02:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-19 20:10:23 +0100 |
| commit | 631298df172c1e034d6898ff13d5d5aabb9a5098 (patch) | |
| tree | b43a195fe510f6692aa5b17c48358a630f04cb1b /tactics | |
| parent | cfeb55070713c8131ca0f95c6c374c624b36a895 (diff) | |
Removing the useless pattern ident genarg.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 14 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 4 |
3 files changed, 12 insertions, 12 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 7f676c157a..c787ebbda8 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -714,10 +714,10 @@ and intern_genarg ist x = | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (intern_or_var ist (out_gen (rawwit wit_int_or_var) x)) - | IdentArgType b -> + | IdentArgType -> let lf = ref Id.Set.empty in - in_gen (glbwit (wit_ident_gen b)) - (intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x)) + in_gen (glbwit wit_ident) + (intern_ident lf ist (out_gen (rawwit wit_ident) x)) | VarArgType -> in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x)) | GenArgType -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 16fc73cfdf..b697d3635c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1327,9 +1327,9 @@ and interp_genarg ist env sigma concl gl x = | IntOrVarArgType -> in_gen (topwit wit_int_or_var) (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x))) - | IdentArgType b -> - in_gen (topwit (wit_ident_gen b)) - (interp_fresh_ident ist env (out_gen (glbwit (wit_ident_gen b)) x)) + | IdentArgType -> + in_gen (topwit wit_ident) + (interp_fresh_ident ist env (out_gen (glbwit wit_ident) x)) | VarArgType -> in_gen (topwit wit_var) (interp_hyp ist env (out_gen (glbwit wit_var) x)) | GenArgType -> @@ -1981,10 +1981,10 @@ and interp_atomic ist tac = match tag with | IntOrVarArgType -> (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))) - | IdentArgType b -> + | IdentArgType -> Proofview.Goal.lift begin Goal.return (value_of_ident (interp_fresh_ident ist env - (out_gen (glbwit (wit_ident_gen b)) x))) + (out_gen (glbwit wit_ident) x))) end | VarArgType -> Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x)) @@ -2025,8 +2025,8 @@ and interp_atomic ist tac = let wit = glbwit (wit_list wit_int_or_var) in let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans)) - | ListArgType (IdentArgType b) -> - let wit = glbwit (wit_list (wit_ident_gen b)) in + | ListArgType IdentArgType -> + let wit = glbwit (wit_list wit_ident) in let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in let ans = List.map mk_ident (out_gen wit x) in (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans)) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 206dec104a..d3cc6adc50 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -295,8 +295,8 @@ and subst_match_rule subst = function and subst_genarg subst (x:glob_generic_argument) = match genarg_tag x with | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x) - | IdentArgType b -> - in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x) + | IdentArgType -> + in_gen (glbwit wit_ident) (out_gen (glbwit wit_ident) x) | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x) | GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x)) | ConstrArgType -> |