aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_ltac.ml41
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/g_xml.ml41
-rw-r--r--parsing/grammar.mllib4
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--parsing/ppconstr.ml2
-rw-r--r--parsing/ppconstr.mli1
-rw-r--r--parsing/pptactic.ml5
-rw-r--r--parsing/printer.ml2
-rw-r--r--parsing/q_coqast.ml478
11 files changed, 54 insertions, 49 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e2edbb096..811fd58ff 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -18,6 +18,7 @@ open Prim
open Tactic
open Tok
open Misctypes
+open Genredexpr
let fail_default_value = ArgArg 0
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 55c03a481..4c1d747ea 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -11,7 +11,7 @@ open Pcoq
open Errors
open Util
open Tacexpr
-open Glob_term
+open Genredexpr
open Genarg
open Topconstr
open Libnames
@@ -22,7 +22,7 @@ open Misctypes
open Locus
open Decl_kinds
-let all_with delta = Tacops.make_red_flag [FBeta;FIota;FZeta;delta]
+let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
let tactic_kw = [ "->"; "<-" ; "by" ]
let _ = List.iter Lexer.add_keyword tactic_kw
@@ -327,7 +327,7 @@ GEXTEND Gram
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flag -> Tacops.make_red_flag s
+ [ [ s = LIST1 red_flag -> Redops.make_red_flag s
| d = delta_flag -> all_with d
] ]
;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 34e0d9532..83c5e6f31 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -819,7 +819,7 @@ GEXTEND Gram
[ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
fun g -> VernacCheckMayEval (Some r, g, c)
| IDENT "Compute"; c = lconstr ->
- fun g -> VernacCheckMayEval (Some (Glob_term.CbvVm None), g, c)
+ fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c)
| IDENT "Check"; c = lconstr ->
fun g -> VernacCheckMayEval (None, g, c) ] ]
;
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 7c26ac124..50270f863 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -22,6 +22,7 @@ open Detyping
open Tok
open Misctypes
open Decl_kinds
+open Genredexpr
(* Generic xml parser without raw data *)
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index caf3d8508..c2dce0231 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -63,13 +63,12 @@ Evd
Reductionops
Inductiveops
Miscops
-Glob_term
+Glob_ops
Detyping
Pattern
Topconstr
Genarg
Ppextend
-Tacops
Tok
Lexer
Extend
@@ -84,6 +83,7 @@ Argextend
Tacextend
Vernacextend
+Redops
G_prim
G_tactic
G_ltac
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5bc6bddd9..e113bb711 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -18,6 +18,7 @@ open Tacexpr
open Libnames
open Compat
open Misctypes
+open Genredexpr
(** The parser of Coq *)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 45ea77d13..6b2e206b6 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -18,12 +18,12 @@ open Ppextend
open Topconstr
open Term
open Pattern
-open Glob_term
open Constrextern
open Termops
open Decl_kinds
open Misctypes
open Locus
+open Genredexpr
(*i*)
let sep_v = fun _ -> str"," ++ spc()
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 1497c90e7..390869cf7 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -18,6 +18,7 @@ open Errors
open Util
open Misctypes
open Locus
+open Genredexpr
val extract_lam_binders :
constr_expr -> local_binder list * constr_expr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 58ce29a04..5d03b6028 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -23,6 +23,7 @@ open Printer
open Misctypes
open Locus
open Decl_kinds
+open Genredexpr
let pr_global x = Nametab.pr_global_env Idset.empty x
@@ -650,7 +651,7 @@ and pr_atom1 = function
| TacIntroMove (None,MoveLast) as t -> pr_atom0 t
| TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
| TacIntroMove (ido,hto) ->
- hov 1 (str"intro" ++ pr_opt pr_id ido ++ Tacops.pr_move_location pr_ident hto)
+ hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscops.pr_move_location pr_ident hto)
| TacAssumption as t -> pr_atom0 t
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
| TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -764,7 +765,7 @@ and pr_atom1 = function
assert b;
hov 1
(str "move" ++ brk (1,1) ++ pr_ident id1 ++
- Tacops.pr_move_location pr_ident id2)
+ Miscops.pr_move_location pr_ident id2)
| TacRename l ->
hov 1
(str "rename" ++ brk (1,1) ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 20fbda2d7..a932a608f 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -519,7 +519,7 @@ let pr_prim_rule = function
| Move (withdep,id1,id2) ->
(str (if withdep then "dependent " else "") ++
- str"move " ++ pr_id id1 ++ Tacops.pr_move_location pr_id id2)
+ str"move " ++ pr_id id1 ++ Miscops.pr_move_location pr_id id2)
| Order ord ->
(str"order " ++ pr_sequence pr_id ord)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index c4581fe1e..a75d1f6cc 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -108,17 +108,17 @@ let mlexpr_of_clause cl =
Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >>
let mlexpr_of_red_flags {
- Glob_term.rBeta = bb;
- Glob_term.rIota = bi;
- Glob_term.rZeta = bz;
- Glob_term.rDelta = bd;
- Glob_term.rConst = l
+ Genredexpr.rBeta = bb;
+ Genredexpr.rIota = bi;
+ Genredexpr.rZeta = bz;
+ Genredexpr.rDelta = bd;
+ Genredexpr.rConst = l
} = <:expr< {
- Glob_term.rBeta = $mlexpr_of_bool bb$;
- Glob_term.rIota = $mlexpr_of_bool bi$;
- Glob_term.rZeta = $mlexpr_of_bool bz$;
- Glob_term.rDelta = $mlexpr_of_bool bd$;
- Glob_term.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
+ Genredexpr.rBeta = $mlexpr_of_bool bb$;
+ Genredexpr.rIota = $mlexpr_of_bool bi$;
+ Genredexpr.rZeta = $mlexpr_of_bool bz$;
+ Genredexpr.rDelta = $mlexpr_of_bool bd$;
+ Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
} >>
let mlexpr_of_explicitation = function
@@ -162,25 +162,25 @@ let mlexpr_of_occ_constr =
mlexpr_of_occurrences mlexpr_of_constr
let mlexpr_of_red_expr = function
- | Glob_term.Red b -> <:expr< Glob_term.Red $mlexpr_of_bool b$ >>
- | Glob_term.Hnf -> <:expr< Glob_term.Hnf >>
- | Glob_term.Simpl o -> <:expr< Glob_term.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
- | Glob_term.Cbv f ->
- <:expr< Glob_term.Cbv $mlexpr_of_red_flags f$ >>
- | Glob_term.Lazy f ->
- <:expr< Glob_term.Lazy $mlexpr_of_red_flags f$ >>
- | Glob_term.Unfold l ->
+ | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
+ | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
+ | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+ | Genredexpr.Cbv f ->
+ <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
+ | Genredexpr.Lazy f ->
+ <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >>
+ | Genredexpr.Unfold l ->
let f1 = mlexpr_of_by_notation mlexpr_of_reference in
let f = mlexpr_of_list (mlexpr_of_occurrences f1) in
- <:expr< Glob_term.Unfold $f l$ >>
- | Glob_term.Fold l ->
- <:expr< Glob_term.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
- | Glob_term.Pattern l ->
+ <:expr< Genredexpr.Unfold $f l$ >>
+ | Genredexpr.Fold l ->
+ <:expr< Genredexpr.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
+ | Genredexpr.Pattern l ->
let f = mlexpr_of_list mlexpr_of_occ_constr in
- <:expr< Glob_term.Pattern $f l$ >>
- | Glob_term.CbvVm o -> <:expr< Glob_term.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
- | Glob_term.ExtraRedExpr s ->
- <:expr< Glob_term.ExtraRedExpr $mlexpr_of_string s$ >>
+ <:expr< Genredexpr.Pattern $f l$ >>
+ | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+ | Genredexpr.ExtraRedExpr s ->
+ <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
let rec mlexpr_of_argtype loc = function
| Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >>
@@ -210,15 +210,15 @@ let rec mlexpr_of_argtype loc = function
| Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
let rec mlexpr_of_may_eval f = function
- | Glob_term.ConstrEval (r,c) ->
- <:expr< Glob_term.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
- | Glob_term.ConstrContext ((loc,id),c) ->
+ | Genredexpr.ConstrEval (r,c) ->
+ <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
+ | Genredexpr.ConstrContext ((loc,id),c) ->
let id = mlexpr_of_ident id in
- <:expr< Glob_term.ConstrContext (loc,$id$) $f c$ >>
- | Glob_term.ConstrTypeOf c ->
- <:expr< Glob_term.ConstrTypeOf $mlexpr_of_constr c$ >>
- | Glob_term.ConstrTerm c ->
- <:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >>
+ <:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >>
+ | Genredexpr.ConstrTypeOf c ->
+ <:expr< Genredexpr.ConstrTypeOf $mlexpr_of_constr c$ >>
+ | Genredexpr.ConstrTerm c ->
+ <:expr< Genredexpr.ConstrTerm $mlexpr_of_constr c$ >>
let mlexpr_of_binding_kind = function
| Misctypes.ExplicitBindings l ->
@@ -236,10 +236,10 @@ let mlexpr_of_constr_with_binding =
mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
let mlexpr_of_move_location f = function
- | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >>
- | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >>
- | Tacexpr.MoveFirst -> <:expr< Tacexpr.MoveFirst >>
- | Tacexpr.MoveLast -> <:expr< Tacexpr.MoveLast >>
+ | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >>
+ | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >>
+ | Misctypes.MoveFirst -> <:expr< Misctypes.MoveFirst >>
+ | Misctypes.MoveLast -> <:expr< Misctypes.MoveLast >>
let mlexpr_of_induction_arg = function
| Tacexpr.ElimOnConstr c ->
@@ -487,7 +487,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
and mlexpr_of_tactic_arg = function
| Tacexpr.MetaIdArg (loc,true,id) -> anti loc id
| Tacexpr.MetaIdArg (loc,false,id) ->
- <:expr< Tacexpr.ConstrMayEval (Glob_term.ConstrTerm $anti loc id$) >>
+ <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
| Tacexpr.TacCall (loc,t,tl) ->
<:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
| Tacexpr.Tacexp t ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:46:10 +0000