aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_ltac.ml46
-rw-r--r--parsing/g_ltacnew.ml46
-rw-r--r--parsing/pptactic.ml18
-rw-r--r--parsing/q_coqast.ml49
-rw-r--r--proofs/tacexpr.ml4
-rw-r--r--translate/pptacticnew.ml6
6 files changed, 29 insertions, 20 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index bd60dc672..59e93affb 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -49,7 +49,7 @@ let make_letin_clause _ = function
end
else
module Prelude = struct
-let fail_default_value = 0
+let fail_default_value = Genarg.ArgArg 0
let out_letin_clause loc = function
| LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
@@ -130,7 +130,7 @@ GEXTEND Gram
;
tactic_expr3:
[ [ IDENT "Try"; ta = tactic_expr3 -> TacTry ta
- | IDENT "Do"; n = natural; ta = tactic_expr3 -> TacDo (n,ta)
+ | IDENT "Do"; n = int_or_var; ta = tactic_expr3 -> TacDo (n,ta)
| IDENT "Repeat"; ta = tactic_expr3 -> TacRepeat ta
| IDENT "Progress"; ta = tactic_expr3 -> TacProgress ta
| IDENT "Info"; tc = tactic_expr3 -> TacInfo tc
@@ -167,7 +167,7 @@ GEXTEND Gram
| IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
TacSolve l
| IDENT "Idtac" ; s = [ s = STRING -> s | -> ""] -> TacId s
- | IDENT "Fail"; n = [ n = natural -> n | -> fail_default_value ];
+ | IDENT "Fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
| st = simple_tactic -> TacAtom (loc,st)
| "("; a = tactic_expr; ")" -> a
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 35f8e642e..e0ae3f39c 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -49,7 +49,7 @@ let make_letin_clause _ = function
end
else
module Prelude = struct
-let fail_default_value = 0
+let fail_default_value = Genarg.ArgArg 0
let out_letin_clause loc = function
| LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
@@ -81,7 +81,7 @@ GEXTEND Gram
[ ]
| "3" RIGHTA
[ IDENT "try"; ta = tactic_expr -> TacTry ta
- | IDENT "do"; n = natural; ta = tactic_expr -> TacDo (n,ta)
+ | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
| IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
| IDENT "progress"; ta = tactic_expr -> TacProgress ta
| IDENT "info"; tc = tactic_expr -> TacInfo tc
@@ -111,7 +111,7 @@ GEXTEND Gram
| IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
TacSolve l
| IDENT "idtac"; s = [ s = STRING -> s | -> ""] -> TacId s
- | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ];
+ | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
| st = simple_tactic -> TacAtom (loc,st)
| a = may_eval_arg -> TacArg(a)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 67033d008..c2ef0f288 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -257,7 +257,9 @@ let rec pr_raw_generic prc prlc prtac prref x =
| PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
| IntroPatternArgType -> pr_arg pr_intro_pattern
(out_gen rawwit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen rawwit_ident x))
+ | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen rawwit_ident x))
+ | HypArgType -> pr_arg
+ (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen rawwit_var x)
| RefArgType -> pr_arg prref (out_gen rawwit_ref x)
| SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
@@ -304,7 +306,8 @@ let rec pr_glob_generic prc prlc prtac x =
| PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
| IntroPatternArgType ->
pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen globwit_ident x))
+ | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen globwit_ident x))
+ | HypArgType -> pr_arg (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen globwit_var x)
| RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
| SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
@@ -353,6 +356,7 @@ let rec pr_generic prc prlc prtac x =
| IntroPatternArgType ->
pr_arg pr_intro_pattern (out_gen wit_intro_pattern x)
| IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen wit_ident x))
+ | HypArgType -> pr_arg prc (out_gen wit_var x)
| RefArgType -> pr_arg pr_global (out_gen wit_ref x)
| SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
| ConstrArgType -> pr_arg prc (out_gen wit_constr x)
@@ -596,7 +600,7 @@ and pr0 = function
| TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
| TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
| TacId "" -> str "Idtac"
- | TacFail (0,"") -> str "Fail"
+ | TacFail (ArgArg 0,"") -> str "Fail"
| TacAtom (_,t) -> pr_atom0 t
| TacArg c -> pr_tacarg c
| t -> str "(" ++ prtac t ++ str ")"
@@ -605,9 +609,9 @@ and pr0 = function
and pr1 = function
| TacAtom (_,t) -> pr_atom1 t
| TacId s -> str "Idtac \"" ++ str s ++ str "\""
- | TacFail (0,s) -> str "Fail \"" ++ str s ++ str "\""
- | TacFail (n,"") -> str "Fail " ++ int n
- | TacFail (n,s) -> str "Fail " ++ int n ++ str " \"" ++ str s ++ str "\""
+ | TacFail (ArgArg 0,s) -> str "Fail \"" ++ str s ++ str "\""
+ | TacFail (n,"") -> str "Fail " ++ pr_or_var int n
+ | TacFail (n,s) -> str "Fail " ++ pr_or_var int n ++ str " \"" ++ str s ++ str "\""
| t -> pr0 t
(* Orelse tactic expressions (printed as if parsed associating on the right
@@ -620,7 +624,7 @@ and pr2 = function
(* Non closed prefix tactic expressions *)
and pr3 = function
| TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t)
- | TacDo (n,t) -> hov 1 (str "Do " ++ int n ++ spc () ++ pr3 t)
+ | TacDo (n,t) -> hov 1 (str "Do " ++ pr_or_var int n ++ spc () ++ pr3 t)
| TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t)
| TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t)
| TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 9813b3774..c05a9e047 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -152,6 +152,10 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
let mlexpr_of_loc loc = <:expr< $dloc$ >>
+let mlexpr_of_or_var f = function
+ | Genarg.ArgArg x -> <:expr< Genarg.ArgArg $f x$ >>
+ | Genarg.ArgVar id -> <:expr< Genarg.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
+
let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int
@@ -252,6 +256,7 @@ let rec mlexpr_of_argtype loc = function
| Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
| Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
| Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
+ | Genarg.HypArgType -> <:expr< Genarg.HypArgType >>
| Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
| Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
| Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >>
@@ -478,13 +483,13 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
| Tacexpr.TacOrelse (t1,t2) ->
<:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
| Tacexpr.TacDo (n,t) ->
- <:expr< Tacexpr.TacDo $int:string_of_int n$ $mlexpr_of_tactic t$ >>
+ <:expr< Tacexpr.TacDo $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >>
| Tacexpr.TacRepeat t ->
<:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
| Tacexpr.TacProgress t ->
<:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
| Tacexpr.TacId s -> <:expr< Tacexpr.TacId $str:s$ >>
- | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $int:string_of_int n$ $str:s$ >>
+ | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $str:s$ >>
(*
| Tacexpr.TacInfo t -> TacInfo (loc,f t)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1be84372c..b8c2636c0 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -195,12 +195,12 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
| TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
| TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
| TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacDo of int * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
| TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
| TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
| TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option
| TacId of string
- | TacFail of int * string
+ | TacFail of int or_var * string
| TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
| TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index e5e3a1fa0..cbe659063 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -704,7 +704,7 @@ let rec pr_tac env inherited tac =
hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t),
ltactical
| TacDo (n,t) ->
- hov 1 (str "do " ++ int n ++ spc () ++ pr_tac env (ltactical,E) t),
+ hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ pr_tac env (ltactical,E) t),
ltactical
| TacRepeat t ->
hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t),
@@ -719,9 +719,9 @@ let rec pr_tac env inherited tac =
hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
pr_tac env (lorelse,E) t2),
lorelse
- | TacFail (0,"") -> str "fail", latom
+ | TacFail (ArgArg 0,"") -> str "fail", latom
| TacFail (n,s) ->
- str "fail" ++ (if n=0 then mt () else pr_arg int n) ++
+ str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
(if s="" then mt() else qsnew s), latom
| TacFirst tl ->
str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:24:35 +0000