diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/dhyp.ml | 2 | ||||
-rw-r--r-- | tactics/evar_tactics.mli | 2 | ||||
-rw-r--r-- | tactics/extraargs.ml4 | 8 | ||||
-rw-r--r-- | tactics/extraargs.mli | 4 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 12 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 108 | ||||
-rw-r--r-- | tactics/tacinterp.mli | 10 |
7 files changed, 73 insertions, 73 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index d9addd1f0..e1e04c8ef 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -290,7 +290,7 @@ let applyDestructor cls discard dd gls = match cl, dd.d_code with | Some id, (Some x, tac) -> let arg = - ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in + ConstrMayEval(ConstrTerm (GRef(dummy_loc,VarRef id),None)) in TacLetIn (false, [(dummy_loc, x), arg], tac) | None, (None, tac) -> tac | _, (Some _,_) -> error "Destructor expects an hypothesis." diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index dc8168ca8..40b628315 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -11,7 +11,7 @@ open Names open Tacexpr open Termops -val instantiate : int -> Tacinterp.interp_sign * Rawterm.rawconstr -> +val instantiate : int -> Tacinterp.interp_sign * Rawterm.glob_constr -> (identifier * hyp_location_flag, unit) location -> tactic (*i diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 25a64c3dd..e31428f7c 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -103,17 +103,17 @@ let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c -let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw +let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_glob_constr raw let pr_raw = pr_rawc () () () let interp_raw ist gl (t,_) = (ist,t) let glob_raw = Tacinterp.intern_constr -let subst_raw = Tacinterp.subst_rawconstr_and_expr +let subst_raw = Tacinterp.subst_glob_constr_and_expr ARGUMENT EXTEND raw - TYPED AS rawconstr + TYPED AS glob_constr PRINTED BY pr_rawc INTERPRETED BY interp_raw @@ -123,7 +123,7 @@ ARGUMENT EXTEND raw RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - GLOB_TYPED AS rawconstr_and_expr + GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ lconstr(c) ] -> [ c ] END diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index f27642678..66c251971 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -25,9 +25,9 @@ val wit_occurrences : (int list) typed_abstract_argument_type val pr_occurrences : int list Rawterm.or_var -> Pp.std_ppcmds val rawwit_raw : constr_expr raw_abstract_argument_type -val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type +val wit_raw : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type val raw : constr_expr Pcoq.Gram.entry -val pr_raw : (Tacinterp.interp_sign * Rawterm.rawconstr) -> Pp.std_ppcmds +val pr_raw : (Tacinterp.interp_sign * Rawterm.glob_constr) -> Pp.std_ppcmds type 'id gen_place= ('id * hyp_location_flag,unit) location diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 78a1f51b7..9a9ef164e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -540,12 +540,12 @@ let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function - | RVar (_,id) as x -> + | GVar (_,id) as x -> if id = tid then (decr occref; if !occref = 0 then x - else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) + else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) else x - | c -> map_rawconstr_left_to_right substrec c in + | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t in if !occref > 0 then Termops.error_invalid_occurrence [occ] else t' @@ -554,10 +554,10 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | RHole (_,Evd.QuestionMark(Evd.Define true)) -> + | GHole (_,Evd.QuestionMark(Evd.Define true)) -> decr occref; if !occref = 0 then tc - else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) - | c -> map_rawconstr_left_to_right substrec c + else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) + | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d4ac859ad..f193c537a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -371,12 +371,12 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict & find_hyp id ist -> - RVar (dloc,id), Some (CRef r) + GVar (dloc,id), Some (CRef r) | Ident (_,id) as r when find_ctxvar id ist -> - RVar (dloc,id), if strict then None else Some (CRef r) + GVar (dloc,id), if strict then None else Some (CRef r) | r -> let loc,_ as lqid = qualid_of_reference r in - RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) + GRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) let intern_move_location ist = function | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id) @@ -502,7 +502,7 @@ let intern_induction_arg ist = function if !strict_check then (* If in a defined tactic, no intros-until *) match intern_constr ist (CRef (Ident (dloc,id))) with - | RVar (loc,id),_ -> ElimOnIdent (loc,id) + | GVar (loc,id),_ -> ElimOnIdent (loc,id) | c -> ElimOnConstr (c,NoBindings) else ElimOnIdent (loc,id) @@ -555,7 +555,7 @@ let intern_typed_pattern ist p = let dummy_pat = PRel 0 in (* we cannot ensure in non strict mode that the pattern is closed *) (* keeping a constr_expr copy is too complicated and we want anyway to *) - (* type it, so we remember the pattern as a rawconstr only *) + (* type it, so we remember the pattern as a glob_constr only *) (intern_constr_gen true false ist p,dummy_pat) let intern_typed_pattern_with_occurrences ist (l,p) = @@ -870,7 +870,7 @@ and intern_tacarg strict ist = function let id = id_of_string s in if find_ltacvar id ist then if istac then Reference (ArgVar (adjust_loc loc,id)) - else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None)) + else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None)) else error_syntactic_metavariables_not_allowed loc | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f | TacCall (loc,f,l) -> @@ -1332,7 +1332,7 @@ let constr_list_of_VList env = function let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with - | RVar (_,id), _ -> + | GVar (_,id), _ -> sigma, List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) | _ -> @@ -1417,7 +1417,7 @@ let interp_may_eval f ist gl = function f ist gl c with e -> debugging_exception_step ist false e (fun () -> - str"interpretation of term " ++ pr_rawconstr_env (pf_env gl) (fst c)); + str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c)); raise e (* Interprets a constr expression possibly to first evaluate *) @@ -1553,11 +1553,11 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = let loc_of_bindings = function | NoBindings -> dummy_loc -| ImplicitBindings l -> loc_of_rawconstr (fst (list_last l)) +| ImplicitBindings l -> loc_of_glob_constr (fst (list_last l)) | ExplicitBindings l -> pi1 (list_last l) let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = - let loc1 = loc_of_rawconstr c in + let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in @@ -1594,7 +1594,7 @@ let interp_induction_arg ist gl sigma arg = if Tactics.is_quantified_hypothesis id gl then sigma, ElimOnIdent (loc,id) else - let c = (RVar (loc,id),Some (CRef (Ident (loc,id)))) in + let c = (GVar (loc,id),Some (CRef (Ident (loc,id)))) in let c = interp_constr ist env sigma c in sigma, ElimOnConstr (c,NoBindings) @@ -2068,7 +2068,7 @@ and interp_genarg ist gl x = in_gen wit_sort (destSort (pf_interp_constr ist gl - (RSort (dloc,out_gen globwit_sort x), None))) + (GSort (dloc,out_gen globwit_sort x), None))) | ConstrArgType -> in_gen wit_constr (pf_interp_constr ist gl (out_gen globwit_constr x)) | ConstrMayEvalArgType -> @@ -2539,22 +2539,22 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x -let subst_rawconstr_and_expr subst (c,e) = +let subst_glob_constr_and_expr subst (c,e) = assert (e=None); (* e<>None only for toplevel tactics *) - (Detyping.subst_rawconstr subst c,None) + (Detyping.subst_glob_constr subst c,None) -let subst_rawconstr = subst_rawconstr_and_expr (* shortening *) +let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) let subst_binding subst (loc,b,c) = - (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c) + (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c) let subst_bindings subst = function | NoBindings -> NoBindings - | ImplicitBindings l -> ImplicitBindings (List.map (subst_rawconstr subst) l) + | ImplicitBindings l -> ImplicitBindings (List.map (subst_glob_constr subst) l) | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l) let subst_raw_with_bindings subst (c,bl) = - (subst_rawconstr subst c, subst_bindings subst bl) + (subst_glob_constr subst c, subst_bindings subst bl) let subst_induction_arg subst = function | ElimOnConstr c -> ElimOnConstr (subst_raw_with_bindings subst c) @@ -2598,17 +2598,17 @@ let subst_unfold subst (l,e) = let subst_flag subst red = { red with rConst = List.map (subst_evaluable subst) red.rConst } -let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c) +let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) -let subst_rawconstr_or_pattern subst (c,p) = - (subst_rawconstr subst c,subst_pattern subst p) +let subst_glob_constr_or_pattern subst (c,p) = + (subst_glob_constr subst c,subst_pattern subst p) let subst_pattern_with_occurrences subst (l,p) = - (l,subst_rawconstr_or_pattern subst p) + (l,subst_glob_constr_or_pattern subst p) let subst_redexp subst = function | Unfold l -> Unfold (List.map (subst_unfold subst) l) - | Fold l -> Fold (List.map (subst_rawconstr subst) l) + | Fold l -> Fold (List.map (subst_glob_constr subst) l) | Cbv f -> Cbv (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) @@ -2616,14 +2616,14 @@ let subst_redexp subst = function | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let subst_raw_may_eval subst = function - | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c) - | ConstrContext (locid,c) -> ConstrContext (locid,subst_rawconstr subst c) - | ConstrTypeOf c -> ConstrTypeOf (subst_rawconstr subst c) - | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c) + | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c) + | ConstrContext (locid,c) -> ConstrContext (locid,subst_glob_constr subst c) + | ConstrTypeOf c -> ConstrTypeOf (subst_glob_constr subst c) + | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_rawconstr_or_pattern subst pc)) - | Term pc -> Term (subst_rawconstr_or_pattern subst pc) + | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function | Hyp (locs,mp) :: tl -> @@ -2638,39 +2638,39 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Basic tactics *) | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x | TacAssumption as x -> x - | TacExact c -> TacExact (subst_rawconstr subst c) - | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) - | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c) + | TacExact c -> TacExact (subst_glob_constr subst c) + | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c) + | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c) | TacApply (a,ev,cb,cl) -> TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb,cl) | TacElim (ev,cb,cbo) -> TacElim (ev,subst_raw_with_bindings subst cb, Option.map (subst_raw_with_bindings subst) cbo) - | TacElimType c -> TacElimType (subst_rawconstr subst c) + | TacElimType c -> TacElimType (subst_glob_constr subst c) | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb) - | TacCaseType c -> TacCaseType (subst_rawconstr subst c) + | TacCaseType c -> TacCaseType (subst_glob_constr subst c) | TacFix (idopt,n) as x -> x | TacMutualFix (b,id,n,l) -> - TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l) + TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) | TacCofix idopt as x -> x | TacMutualCofix (b,id,l) -> - TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l) - | TacCut c -> TacCut (subst_rawconstr subst c) + TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) + | TacCut c -> TacCut (subst_glob_constr subst c) | TacAssert (b,na,c) -> - TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c) + TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) - | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_rawconstr subst c,clp,b) + | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c) + | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b) (* Automation tactics *) - | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l) - | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l) + | TacTrivial (lems,l) -> TacTrivial (List.map (subst_glob_constr subst) lems,l) + | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_glob_constr subst) lems,l) | TacAutoTDB n -> TacAutoTDB n | TacDestructHyp (b,id) -> TacDestructHyp(b,id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) - | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems) + | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_glob_constr subst) lems) (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) as x -> x @@ -2679,13 +2679,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with List.map (subst_induction_arg subst) lc, Option.map (subst_raw_with_bindings subst) cbo, ids) l, cls)) | TacDoubleInduction (h1,h2) as x -> x - | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) - | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) + | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c) + | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c) | TacDecompose (l,c) -> let l = List.map (subst_or_var (subst_inductive subst)) l in - TacDecompose (l,subst_rawconstr subst c) + TacDecompose (l,subst_glob_constr subst c) | TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l) - | TacLApply c -> TacLApply (subst_rawconstr subst c) + | TacLApply c -> TacLApply (subst_glob_constr subst c) (* Context management *) | TacClear _ as x -> x @@ -2704,12 +2704,12 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (op,c,cl) -> - TacChange (Option.map (subst_rawconstr_or_pattern subst) op, - subst_rawconstr subst c, cl) + TacChange (Option.map (subst_glob_constr_or_pattern subst) op, + subst_glob_constr subst c, cl) (* Equivalence relations *) | TacReflexivity | TacSymmetry _ as x -> x - | TacTransitivity c -> TacTransitivity (Option.map (subst_rawconstr subst) c) + | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c) (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> @@ -2718,10 +2718,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with b,m,subst_raw_with_bindings subst c) l, cl,Option.map (subst_tactic subst) by) | TacInversion (DepInversion (k,c,l),hyp) -> - TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp) + TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp) | TacInversion (NonDepInversion _,_) as x -> x | TacInversion (InversionUsing (c,cl),hyp) -> - TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp) + TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp) (* For extensions *) | TacExtend (_loc,opn,l) -> @@ -2808,7 +2808,7 @@ and subst_genarg subst (x:glob_generic_argument) = | SortArgType -> in_gen globwit_sort (out_gen globwit_sort x) | ConstrArgType -> - in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x)) + in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x)) | ConstrMayEvalArgType -> in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x)) | QuantHypArgType -> @@ -2819,7 +2819,7 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) | OpenConstrArgType b -> in_gen (globwit_open_constr_gen b) - ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x))) + ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x)) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ee3401a08..ca5acad31 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -96,11 +96,11 @@ val intern_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr val intern_constr : - glob_sign -> constr_expr -> rawconstr_and_expr + glob_sign -> constr_expr -> glob_constr_and_expr val intern_constr_with_bindings : glob_sign -> constr_expr * constr_expr Rawterm.bindings -> - rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings + glob_constr_and_expr * glob_constr_and_expr Rawterm.bindings val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located @@ -108,8 +108,8 @@ val intern_hyp : val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument -val subst_rawconstr_and_expr : - substitution -> rawconstr_and_expr -> rawconstr_and_expr +val subst_glob_constr_and_expr : + substitution -> glob_constr_and_expr -> glob_constr_and_expr (** Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value @@ -127,7 +127,7 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier -val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings +val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings (** Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr |