diff options
| author | Pierre-Marie Pédrot | 2015-12-18 17:18:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-21 19:36:38 +0100 |
| commit | 329b5b9ed526d572d7df066dc99486e1dcb9e4cc (patch) | |
| tree | 1cad1cd1c7371c8cefc9287dd32d190e12757d1c /tactics | |
| parent | b2beb9087628de23679a831e6273b91816f1ed27 (diff) | |
Removing the now useless genarg generic argument.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/taccoerce.ml | 5 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
4 files changed, 2 insertions, 11 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index f856fd842b..88e36be14a 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -44,10 +44,7 @@ struct type t = Val.t -let rec normalize v = v (** FIXME *) -(* if has_type v (topwit wit_genarg) then *) -(* normalize (out_gen (topwit wit_genarg) v) *) -(* else v *) +let normalize v = v let of_constr c = in_gen (topwit wit_constr) c diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index ac1229f2f7..d0f83836de 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -733,8 +733,6 @@ and intern_genarg ist x = map_raw wit_ident (intern_ident lf) ist x | VarArgType -> map_raw wit_var intern_hyp ist x - | GenArgType -> - map_raw wit_genarg intern_genarg ist x | ConstrArgType -> map_raw wit_constr intern_constr ist x | ConstrMayEvalArgType -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1760341d11..f87dc663bc 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1266,7 +1266,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (Genarg.out_gen (glbwit wit_ident) x))) | VarArgType -> Ftactic.return (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x)) - | GenArgType -> f (Genarg.out_gen (glbwit wit_genarg) x) | OpenConstrArgType -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (Genarg.out_gen (glbwit wit_open_constr) x))) gl in @@ -1647,8 +1646,6 @@ and interp_genarg ist env sigma concl gl x = (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x)) | VarArgType -> in_gen (topwit wit_var) (interp_hyp ist env sigma (Genarg.out_gen (glbwit wit_var) x)) - | GenArgType -> - interp_genarg (Genarg.out_gen (glbwit wit_genarg) x) | ConstrArgType -> let (sigma,c_interp) = interp_constr ist env !evdref (Genarg.out_gen (glbwit wit_constr) x) @@ -1706,7 +1703,7 @@ and interp_genarg ist env sigma concl gl x = and global_genarg = let rec global_tag = function - | IntOrVarArgType | GenArgType -> true + | IntOrVarArgType -> true | ListArgType t | OptArgType t -> global_tag t | PairArgType (t1,t2) -> global_tag t1 && global_tag t2 | _ -> false diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 6d32aa81b9..2884e318b8 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -284,7 +284,6 @@ and subst_genarg subst (x:glob_generic_argument) = | 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 -> in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x)) | ConstrMayEvalArgType -> |