diff options
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/g_tactic.ml4 | 4 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 10 | ||||
-rw-r--r-- | plugins/ltac/tacintern.ml | 6 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 6 | ||||
-rw-r--r-- | plugins/ltac/tacsubst.ml | 4 |
5 files changed, 15 insertions, 15 deletions
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 1674bb4ca..d1e5c810f 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -336,8 +336,8 @@ GEXTEND Gram | pat = naming_intropattern -> !@loc, IntroNaming pat ] ] ; simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ] + [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c) + | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index aec2e37fd..0dd6819fd 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -149,7 +149,7 @@ type 'a extra_genarg_printer = let pr_or_by_notation f = function | AN v -> f v - | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_located pr (loc,x) = pr x @@ -162,8 +162,8 @@ type 'a extra_genarg_printer = | NamedHyp id -> pr_id id let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -368,8 +368,8 @@ type 'a extra_genarg_printer = let pr_esubst prc l = let pr_qhyp = function - (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,NamedHyp id,c) -> + (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" + | (_,(NamedHyp id,c)) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" in prlist_with_sep spc pr_qhyp l diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index e7d4c1be9..ad9814b84 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -212,8 +212,8 @@ let intern_constr = intern_constr_gen false false let intern_type = intern_constr_gen false true (* Globalize bindings *) -let intern_binding ist (loc,b,c) = - (loc,intern_binding_name ist b,intern_constr ist c) +let intern_binding ist (loc,(b,c)) = + (loc,(intern_binding_name ist b,intern_constr ist c)) let intern_bindings ist = function | NoBindings -> NoBindings @@ -291,7 +291,7 @@ let intern_evaluable_global_reference ist r = let intern_evaluable_reference_or_by_notation ist = function | AN r -> intern_evaluable_global_reference ist r - | ByNotation (loc,ntn,sc) -> + | ByNotation (loc,(ntn,sc)) -> evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a8d8eda1d..aac63fcb2 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -987,9 +987,9 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id) with Not_found -> NamedHyp id -let interp_binding ist env sigma (loc,b,c) = +let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,interp_binding_name ist sigma b,c) + sigma, (loc,(interp_binding_name ist sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -1014,7 +1014,7 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = let loc_of_bindings = function | NoBindings -> Loc.ghost | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) -| ExplicitBindings l -> pi1 (List.last l) +| ExplicitBindings l -> fst (List.last l) let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fe3a9f3b2..9582ebd89 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -32,8 +32,8 @@ let subst_glob_constr_and_expr subst (c, e) = let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) -let subst_binding subst (loc,b,c) = - (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c) +let subst_binding subst (loc,(b,c)) = + (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c)) let subst_bindings subst = function | NoBindings -> NoBindings |