Merge PR #10919: factorize or_var_map

Reviewed-by: ppedrot
Reviewed-by: vbgl

4 files changed, 14 insertions, 12 deletions

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 9b52b710c1..1b00a93834 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -182,10 +182,6 @@ let mkCLambdaN_simple bl c = match bl with
 
 let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc
 
-let map_int_or_var f = function
-  | ArgArg x -> ArgArg (f x)
-  | ArgVar _ as y -> y
-
 let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
 
 let merge_occurrences loc cl = function
@@ -269,7 +265,7 @@ GRAMMAR EXTEND Gram
     [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
       | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
 	  (* have used int_or_var instead of nat_or_var for compatibility *)
-	   { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ]
+         { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
   ;
   occs:
     [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b6e7dd64b0..bf5d49f678 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -76,25 +76,21 @@ let subst_and_short_name f (c,n) =
 (*  assert (n=None); *)(* since tacdef are strictly globalized *)
   (f c,None)
 
-let subst_or_var f =  let open Locus in function
-  | ArgVar _ as x -> x
-  | ArgArg x -> ArgArg (f x)
-
 let subst_located f = Loc.map f
 
 let subst_reference subst =
-  subst_or_var (subst_located (subst_kn subst))
+  Locusops.or_var_map (subst_located (subst_kn subst))
 
 (*CSC: subst_global_reference is used "only" for RefArgType, that propagates
   to the syntactic non-terminals "global", used in commands such as
   Print. It is also used for non-evaluable references. *)
 
 let subst_global_reference subst =
-  subst_or_var (subst_located (subst_global_reference subst))
+  Locusops.or_var_map (subst_located (subst_global_reference subst))
 
 let subst_evaluable subst =
   let subst_eval_ref = subst_evaluable_reference subst in
-    subst_or_var (subst_and_short_name subst_eval_ref)
+    Locusops.or_var_map (subst_and_short_name subst_eval_ref)
 
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 02c8f6a2a8..9c6cf090a2 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -10,6 +10,12 @@
 
 open Locus
 
+(** Utilities on or_var *)
+
+let or_var_map f = function
+  | ArgArg x -> ArgArg (f x)
+  | ArgVar _ as y -> y
+
 (** Utilities on occurrences *)
 
 let occurrences_map f = function
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 195dbec935..47d2ffe797 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -11,6 +11,10 @@
 open Names
 open Locus
 
+(** Utilities on or_var *)
+
+val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var
+
 (** Utilities on occurrences *)
 
 val occurrences_map :