aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/q_coqast.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/q_coqast.ml4')
-rw-r--r--parsing/q_coqast.ml478
1 files changed, 39 insertions, 39 deletions
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 ->