diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 5 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 26 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 5 |
3 files changed, 9 insertions, 27 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index d0f83836de..5e725e182d 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -727,7 +727,6 @@ and intern_match_rule onlytac ist = function and intern_genarg ist x = match genarg_tag x with - | IntOrVarArgType -> map_raw wit_int_or_var intern_int_or_var ist x | IdentArgType -> let lf = ref Id.Set.empty in map_raw wit_ident (intern_ident lf) ist x @@ -735,8 +734,6 @@ and intern_genarg ist x = map_raw wit_var intern_hyp ist x | ConstrArgType -> map_raw wit_constr intern_constr ist x - | ConstrMayEvalArgType -> - map_raw wit_constr_may_eval intern_constr_may_eval ist x | OpenConstrArgType -> map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x | ListArgType _ -> @@ -836,6 +833,7 @@ let () = Genintern.register_intern0 wit_clause_dft_concl intern_clause let () = + Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); @@ -844,6 +842,7 @@ let () = Genintern.register_intern0 wit_red_expr (lift intern_red_expr); Genintern.register_intern0 wit_bindings (lift intern_bindings); Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings); + Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval); () (***************************************************************************) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5a6834ab5d..37d9f1825e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1259,8 +1259,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in match tag with - | IntOrVarArgType -> - Ftactic.return (mk_int_or_var_value ist (Genarg.out_gen (glbwit wit_int_or_var) x)) | IdentArgType -> Ftactic.return (value_of_ident (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))) @@ -1270,20 +1268,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with 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 Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) - | ConstrMayEvalArgType -> - let (sigma,c_interp) = - interp_constr_may_eval ist env sigma - (Genarg.out_gen (glbwit wit_constr_may_eval) x) - in - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in Ftactic.return (Value.of_list ans) - | ListArgType IntOrVarArgType -> - let wit = glbwit (wit_list wit_int_or_var) in - let ans = List.map (mk_int_or_var_value ist) (Genarg.out_gen wit x) in - Ftactic.return (Value.of_list ans) | ListArgType IdentArgType -> let wit = glbwit (wit_list wit_ident) in let mk_ident x = value_of_ident (interp_ident ist env sigma x) in @@ -1638,9 +1626,6 @@ and interp_genarg ist env sigma concl gl x = let evdref = ref sigma in let rec interp_genarg x = match genarg_tag x with - | IntOrVarArgType -> - in_gen (topwit wit_int_or_var) - (interp_int_or_var ist (Genarg.out_gen (glbwit wit_int_or_var) x)) | IdentArgType -> in_gen (topwit wit_ident) (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x)) @@ -1652,10 +1637,6 @@ and interp_genarg ist env sigma concl gl x = in evdref := sigma; in_gen (topwit wit_constr) c_interp - | ConstrMayEvalArgType -> - let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (Genarg.out_gen (glbwit wit_constr_may_eval) x) in - evdref := sigma; - in_gen (topwit wit_constr_may_eval) c_interp | OpenConstrArgType -> let expected_type = WithoutTypeConstraint in in_gen (topwit wit_open_constr) @@ -1703,7 +1684,7 @@ and interp_genarg ist env sigma concl gl x = and global_genarg = let rec global_tag = function - | IntOrVarArgType -> true + | ExtraArgType "int_or_var" -> true (** FIXME *) | ListArgType t | OptArgType t -> global_tag t | PairArgType (t1,t2) -> global_tag t1 && global_tag t2 | _ -> false @@ -2335,6 +2316,7 @@ let interp_constr_with_bindings' ist gl c = (project gl, pack_sigma (sigma, c)) let () = + Geninterp.register_interp0 wit_int_or_var (fun ist gl n -> project gl, interp_int_or_var ist n); Geninterp.register_interp0 wit_ref (lift interp_reference); Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern); Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause); @@ -2343,7 +2325,9 @@ let () = Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr); Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis); Geninterp.register_interp0 wit_bindings interp_bindings'; - Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings' + Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; + Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval); + () let () = let interp ist gl tac = diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 2884e318b8..0c96653626 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -280,14 +280,11 @@ 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 -> 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)) - | ConstrMayEvalArgType -> - in_gen (glbwit wit_constr_may_eval) (subst_raw_may_eval subst (out_gen (glbwit wit_constr_may_eval) x)) | OpenConstrArgType -> in_gen (glbwit wit_open_constr) ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x))) @@ -322,6 +319,7 @@ and subst_genarg subst (x:glob_generic_argument) = (** Registering *) let () = + Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); Genintern.register_subst0 wit_tactic subst_tactic; @@ -332,4 +330,5 @@ let () = Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis; Genintern.register_subst0 wit_bindings subst_bindings; Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings; + Genintern.register_subst0 wit_constr_may_eval subst_raw_may_eval; () |