aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/q_coqast.ml42
-rw-r--r--interp/constrarg.ml6
-rw-r--r--interp/constrarg.mli4
-rw-r--r--lib/genarg.ml7
-rw-r--r--lib/genarg.mli2
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--printing/pptactic.ml7
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml14
-rw-r--r--tactics/tacsubst.ml4
11 files changed, 23 insertions, 33 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 934b9b117..093a561d6 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -31,7 +31,7 @@ let mk_extraarg loc s =
let rec make_wit loc = function
| IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
- | IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >>
+ | IdentArgType -> <:expr< Constrarg.wit_ident >>
| VarArgType -> <:expr< Constrarg.wit_var >>
| QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
| GenArgType -> <:expr< Constrarg.wit_genarg >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3e11bf5a8..b3f60dee6 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -203,7 +203,7 @@ let mlexpr_of_red_expr = function
let rec mlexpr_of_argtype loc = function
| Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
- | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
+ | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
| Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 4f20dd560..846fb5b93 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -39,11 +39,7 @@ let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type =
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
Genarg.make0 None "tactic"
-let wit_ident_gen b = unsafe_of_type (IdentArgType b)
-
-let wit_ident = wit_ident_gen true
-
-let wit_pattern_ident = wit_ident_gen false
+let wit_ident = unsafe_of_type IdentArgType
let wit_var = unsafe_of_type VarArgType
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index b83c20065..1654d2719 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -36,10 +36,6 @@ val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
val wit_ident : Id.t uniform_genarg_type
-val wit_pattern_ident : Id.t uniform_genarg_type
-
-val wit_ident_gen : bool -> Id.t uniform_genarg_type
-
val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 6520669fa..3fb815510 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -12,7 +12,7 @@ open Util
type argument_type =
(* Basic types *)
| IntOrVarArgType
- | IdentArgType of bool
+ | IdentArgType
| VarArgType
(* Specific types *)
| GenArgType
@@ -30,7 +30,7 @@ type argument_type =
let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
| IntOrVarArgType, IntOrVarArgType -> true
-| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
+| IdentArgType, IdentArgType -> true
| VarArgType, VarArgType -> true
| GenArgType, GenArgType -> true
| ConstrArgType, ConstrArgType -> true
@@ -49,8 +49,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
let rec pr_argument_type = function
| IntOrVarArgType -> str "int_or_var"
-| IdentArgType true -> str "ident"
-| IdentArgType false -> str "pattern_ident"
+| IdentArgType -> str "ident"
| VarArgType -> str "var"
| GenArgType -> str "genarg"
| ConstrArgType -> str "constr"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 51c261742..f275b0d00 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -191,7 +191,7 @@ val app_pair :
type argument_type =
(** Basic types *)
| IntOrVarArgType
- | IdentArgType of bool
+ | IdentArgType
| VarArgType
(** Specific types *)
| GenArgType
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d25efa72a..e26ecbea3 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -322,7 +322,7 @@ module Prim =
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
- let pattern_ident = gec_gen (rawwit wit_pattern_ident) "pattern_ident"
+ let pattern_ident = Gram.entry_create "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"
(* A synonym of ident - maybe ident will be located one day *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index cb09784c1..ae3b41e23 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -141,12 +141,11 @@ let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
let with_evars ev s = if ev then "e" ^ s else s
-let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
| IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
- | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
+ | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
| GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
@@ -180,7 +179,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
let rec pr_glb_generic prc prlc prtac prpat x =
match Genarg.genarg_tag x with
| IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
- | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
+ | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
| GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
@@ -215,7 +214,7 @@ let rec pr_glb_generic prc prlc prtac prpat x =
let rec pr_top_generic prc prlc prtac prpat x =
match Genarg.genarg_tag x with
| IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
- | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
+ | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
| VarArgType -> pr_id (out_gen (topwit wit_var) x)
| GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (topwit wit_constr) x)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 7f676c157..c787ebbda 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -714,10 +714,10 @@ and intern_genarg ist x =
| IntOrVarArgType ->
in_gen (glbwit wit_int_or_var)
(intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
- | IdentArgType b ->
+ | IdentArgType ->
let lf = ref Id.Set.empty in
- in_gen (glbwit (wit_ident_gen b))
- (intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
+ in_gen (glbwit wit_ident)
+ (intern_ident lf ist (out_gen (rawwit wit_ident) x))
| VarArgType ->
in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
| GenArgType ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 16fc73cfd..b697d3635 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1327,9 +1327,9 @@ and interp_genarg ist env sigma concl gl x =
| IntOrVarArgType ->
in_gen (topwit wit_int_or_var)
(ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
- | IdentArgType b ->
- in_gen (topwit (wit_ident_gen b))
- (interp_fresh_ident ist env (out_gen (glbwit (wit_ident_gen b)) x))
+ | IdentArgType ->
+ in_gen (topwit wit_ident)
+ (interp_fresh_ident ist env (out_gen (glbwit wit_ident) x))
| VarArgType ->
in_gen (topwit wit_var) (interp_hyp ist env (out_gen (glbwit wit_var) x))
| GenArgType ->
@@ -1981,10 +1981,10 @@ and interp_atomic ist tac =
match tag with
| IntOrVarArgType ->
(Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
- | IdentArgType b ->
+ | IdentArgType ->
Proofview.Goal.lift begin
Goal.return (value_of_ident (interp_fresh_ident ist env
- (out_gen (glbwit (wit_ident_gen b)) x)))
+ (out_gen (glbwit wit_ident) x)))
end
| VarArgType ->
Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
@@ -2025,8 +2025,8 @@ and interp_atomic ist tac =
let wit = glbwit (wit_list wit_int_or_var) in
let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
(Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
- | ListArgType (IdentArgType b) ->
- let wit = glbwit (wit_list (wit_ident_gen b)) in
+ | ListArgType IdentArgType ->
+ let wit = glbwit (wit_list wit_ident) in
let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
let ans = List.map mk_ident (out_gen wit x) in
(Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 206dec104..d3cc6adc5 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -295,8 +295,8 @@ 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 b ->
- in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) 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)
| GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
| ConstrArgType ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:16:07 +0000