diff options
| -rw-r--r-- | grammar/q_coqast.ml4 | 4 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 2 | ||||
| -rw-r--r-- | printing/pptactic.ml | 4 | ||||
| -rw-r--r-- | printing/pptactic.mli | 1 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 26 |
5 files changed, 12 insertions, 25 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 360b96dc4a..d1f4587915 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -71,10 +71,6 @@ let mlexpr_of_intro_pattern = function let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) -let mlexpr_of_or_metaid f = function - | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> - | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> - let mlexpr_of_quantified_hypothesis = function | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d5a3328f02..609ee2f369 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -19,8 +19,6 @@ open Decl_kinds open Misctypes open Locus -type 'a or_metaid = AI of 'a | MetaId of Loc.t * string - type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = bool (* true = lazy false = eager *) type evars_flag = bool (* true = pose evars false = fail on evars *) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 90341a69b8..04e1a49232 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -82,10 +82,6 @@ let pr_or_var pr = function | ArgArg x -> pr x | ArgVar (_,s) -> pr_id s -let pr_or_metaid pr = function - | AI x -> pr x - | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable" - let pr_and_short_name pr (c,_) = pr c let pr_or_by_notation f = function diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 7dbdf80aac..82cb9c0a58 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -17,7 +17,6 @@ open Pattern open Misctypes val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds -val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 56adcc1783..c624a38d1a 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -102,8 +102,6 @@ let intern_hyp ist (loc,id as locid) = else Pretype_errors.error_var_not_found_loc loc id -let intern_hyp_or_metaid ist id = intern_hyp ist id - let intern_or_var ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) | ArgArg _ as x -> x @@ -143,8 +141,8 @@ let intern_constr_reference strict ist = function if strict then None else Some (CRef (r,None)) let intern_move_location ist = function - | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id) - | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id) + | MoveAfter id -> MoveAfter (intern_hyp ist id) + | MoveBefore id -> MoveBefore (intern_hyp ist id) | MoveFirst -> MoveFirst | MoveLast -> MoveLast @@ -213,7 +211,7 @@ let intern_non_tactic_reference strict ist r = let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x - | MsgIdent id -> MsgIdent (intern_hyp_or_metaid ist id) + | MsgIdent id -> MsgIdent (intern_hyp ist id) let intern_message ist = List.map (intern_message_token ist) @@ -366,9 +364,9 @@ let intern_red_expr ist = function | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r let intern_in_hyp_as ist lf (id,ipat) = - (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat) + (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat) -let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist) +let intern_hyp_list ist = List.map (intern_hyp ist) let intern_inversion_strength lf ist = function | NonDepInversion (k,idl,ids) -> @@ -383,7 +381,7 @@ let intern_inversion_strength lf ist = function (* Interprets an hypothesis name *) let intern_hyp_location ist ((occs,id),hl) = ((Locusops.occurrences_map (List.map (intern_or_var ist)) occs, - intern_hyp_or_metaid ist id), hl) + intern_hyp ist id), hl) (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function @@ -505,15 +503,15 @@ let rec intern_atomic lf ist x = | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in TacDecompose (l,intern_constr ist c) (* Context management *) - | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l) - | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l) + | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l) + | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l) | TacMove (dep,id1,id2) -> - TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2) + TacMove (dep,intern_hyp ist id1,intern_move_location ist id2) | TacRename l -> TacRename (List.map (fun (id1,id2) -> - intern_hyp_or_metaid ist id1, - intern_hyp_or_metaid ist id2) l) - | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l) + intern_hyp ist id1, + intern_hyp ist id2) l) + | TacRevert l -> TacRevert (List.map (intern_hyp ist) l) (* Constructors *) | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll) |