aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml420
-rw-r--r--parsing/g_ltac.ml43
-rw-r--r--parsing/g_prim.ml44
-rw-r--r--parsing/g_proofs.ml43
-rw-r--r--parsing/g_tactic.ml449
-rw-r--r--parsing/g_vernac.ml49
-rw-r--r--parsing/g_xml.ml48
-rw-r--r--parsing/grammar.mllib2
-rw-r--r--parsing/pcoq.mli3
-rw-r--r--parsing/ppconstr.ml33
-rw-r--r--parsing/ppconstr.mli3
-rw-r--r--parsing/pptactic.ml23
-rw-r--r--parsing/pptactic.mli1
-rw-r--r--parsing/prettyp.ml9
-rw-r--r--parsing/prettyp.mli2
-rw-r--r--parsing/q_constr.ml411
-rw-r--r--parsing/q_coqast.ml474
17 files changed, 144 insertions, 113 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 06d922a7c..c8ca6cbab 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -18,6 +18,8 @@ open Topconstr
open Util
open Tok
open Compat
+open Misctypes
+open Decl_kinds
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
@@ -29,7 +31,7 @@ let _ = List.iter Lexer.add_keyword constr_kw
let mk_cast = function
(c,(_,None)) -> c
- | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
+ | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv ty)
let binders_of_names l =
List.map (fun (loc, na) ->
@@ -38,7 +40,7 @@ let binders_of_names l =
let binders_of_lidents l =
List.map (fun (loc, id) ->
- LocalRawAssum ([loc, Name id], Default Glob_term.Explicit,
+ LocalRawAssum ([loc, Name id], Default Explicit,
CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -144,8 +146,8 @@ GEXTEND Gram
[ [ c = lconstr -> c ] ]
;
sort:
- [ [ "Set" -> GProp Pos
- | "Prop" -> GProp Null
+ [ [ "Set" -> GSet
+ | "Prop" -> GProp
| "Type" -> GType None ] ]
;
lconstr:
@@ -160,13 +162,13 @@ GEXTEND Gram
[ c = binder_constr -> c ]
| "100" RIGHTA
[ c1 = operconstr; "<:"; c2 = binder_constr ->
- CCast(loc,c1, CastConv (VMcast,c2))
+ CCast(loc,c1, CastVM c2)
| c1 = operconstr; "<:"; c2 = SELF ->
- CCast(loc,c1, CastConv (VMcast,c2))
+ CCast(loc,c1, CastVM c2)
| c1 = operconstr; ":";c2 = binder_constr ->
- CCast(loc,c1, CastConv (DEFAULTcast,c2))
+ CCast(loc,c1, CastConv c2)
| c1 = operconstr; ":"; c2 = SELF ->
- CCast(loc,c1, CastConv (DEFAULTcast,c2))
+ CCast(loc,c1, CastConv c2)
| c1 = operconstr; ":>" ->
CCast(loc,c1, CastCoerce) ]
| "99" RIGHTA [ ]
@@ -410,7 +412,7 @@ GEXTEND Gram
| "("; id=name; ":="; c=lconstr; ")" ->
[LocalRawDef (id,c)]
| "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+ [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))]
| "{"; id=name; "}" ->
[LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
| "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index bf0e13e02..e2edbb096 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -17,6 +17,7 @@ open Pcoq
open Prim
open Tactic
open Tok
+open Misctypes
let fail_default_value = ArgArg 0
@@ -177,7 +178,7 @@ GEXTEND Gram
let t, ty =
match mpv with
| Term t -> (match t with
- | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty)
+ | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty)
| _ -> mpv, None)
| _ -> mpv, None
in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty)
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index fd6fc7dd8..d6b2d8380 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -86,8 +86,8 @@ GEXTEND Gram
[ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ]
;
smart_global:
- [ [ c = reference -> Genarg.AN c
- | ntn = by_notation -> Genarg.ByNotation ntn ] ]
+ [ [ c = reference -> Misctypes.AN c
+ | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
;
qualid:
[ [ qid = basequalid -> loc, qid ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5f44a9e9c..6edb0bfc1 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -17,6 +17,7 @@ open Locality
open Prim
open Constr
open Tok
+open Misctypes
let thm_token = G_vernac.thm_token
@@ -113,6 +114,6 @@ GEXTEND Gram
;
constr_body:
[ [ ":="; c = lconstr -> c
- | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ]
+ | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,CastConv t) ] ]
;
END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8b72a5e93..7cbcd584c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -18,6 +18,9 @@ open Libnames
open Termops
open Tok
open Compat
+open Misctypes
+open Locus
+open Decl_kinds
let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
@@ -166,17 +169,17 @@ let mkCLambdaN_simple bl c =
let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
let map_int_or_var f = function
- | Glob_term.ArgArg x -> Glob_term.ArgArg (f x)
- | Glob_term.ArgVar _ as y -> y
+ | ArgArg x -> ArgArg (f x)
+ | ArgVar _ as y -> y
-let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr }
+let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
let has_no_specified_occs cl =
(cl.onhyps = None ||
- List.for_all (fun ((occs,_),_) -> occs = all_occurrences_expr)
+ List.for_all (fun ((occs,_),_) -> occs = AllOccurrences)
(Option.get cl.onhyps))
- && (cl.concl_occs = all_occurrences_expr
- || cl.concl_occs = no_occurrences_expr)
+ && (cl.concl_occs = AllOccurrences
+ || cl.concl_occs = NoOccurrences)
let merge_occurrences loc cl = function
| None ->
@@ -185,11 +188,11 @@ let merge_occurrences loc cl = function
user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
| Some (occs,p) ->
(Some p,
- if occs = all_occurrences_expr then cl
+ if occs = AllOccurrences then cl
else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs }
else match cl.onhyps with
| Some [(occs',id),l] when
- occs' = all_occurrences_expr && cl.concl_occs = no_occurrences_expr ->
+ occs' = AllOccurrences && cl.concl_occs = NoOccurrences ->
{ cl with onhyps=Some[(occs,id),l] }
| _ ->
if has_no_specified_occs cl then
@@ -205,12 +208,12 @@ GEXTEND Gram
simple_intropattern;
int_or_var:
- [ [ n = integer -> Glob_term.ArgArg n
- | id = identref -> Glob_term.ArgVar id ] ]
+ [ [ n = integer -> ArgArg n
+ | id = identref -> ArgVar id ] ]
;
nat_or_var:
- [ [ n = natural -> Glob_term.ArgArg n
- | id = identref -> Glob_term.ArgVar id ] ]
+ [ [ n = natural -> ArgArg n
+ | id = identref -> ArgVar id ] ]
;
(* An identifier or a quotation meta-variable *)
id_or_meta:
@@ -236,18 +239,18 @@ GEXTEND Gram
;
conversion:
[ [ c = constr -> (None, c)
- | c1 = constr; "with"; c2 = constr -> (Some (all_occurrences_expr,c1),c2)
+ | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2)
| c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
(Some (occs,c1), c2) ] ]
;
occs_nums:
- [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
+ [ [ 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 *)
- all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ]
+ AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ]
;
occs:
- [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr ] ]
+ [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ]
;
pattern_occ:
[ [ c = constr; nl = occs -> (nl,c) ] ]
@@ -374,7 +377,7 @@ GEXTEND Gram
| hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
{onhyps=Some hl; concl_occs=occs}
| hl=LIST0 hypident_occ SEP"," ->
- {onhyps=Some hl; concl_occs=no_occurrences_expr} ] ]
+ {onhyps=Some hl; concl_occs=NoOccurrences} ] ]
;
clause_dft_concl:
[ [ "in"; cl = in_clause -> cl
@@ -383,14 +386,14 @@ GEXTEND Gram
;
clause_dft_all:
[ [ "in"; cl = in_clause -> cl
- | -> {onhyps=None; concl_occs=all_occurrences_expr} ] ]
+ | -> {onhyps=None; concl_occs=AllOccurrences} ] ]
;
opt_clause:
[ [ "in"; cl = in_clause -> Some cl | -> None ] ]
;
concl_occ:
[ [ "*"; occs = occs -> occs
- | -> no_occurrences_expr ] ]
+ | -> NoOccurrences ] ]
;
in_hyp_list:
[ [ "in"; idl = LIST1 id_or_meta -> idl
@@ -546,9 +549,9 @@ GEXTEND Gram
TacMutualCofix (false,id,List.map mk_cofix_tac fd)
| IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacLetTac (Names.Name id,b,nowhere,true)
+ TacLetTac (Names.Name id,b,Locusops.nowhere,true)
| IDENT "pose"; b = constr; na = as_name ->
- TacLetTac (na,b,nowhere,true)
+ TacLetTac (na,b,Locusops.nowhere,true)
| IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
TacLetTac (Names.Name id,c,p,true)
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
@@ -572,9 +575,9 @@ GEXTEND Gram
| IDENT "cut"; c = constr -> TacCut c
| IDENT "generalize"; c = constr ->
- TacGeneralize [((all_occurrences_expr,c),Names.Anonymous)]
+ TacGeneralize [((AllOccurrences,c),Names.Anonymous)]
| IDENT "generalize"; c = constr; l = LIST1 constr ->
- let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in
+ let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
TacGeneralize (List.map gen_everywhere (c::l))
| IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
na = as_name;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f684b9a0d..34e0d9532 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -23,6 +23,7 @@ open Genarg
open Ppextend
open Goptions
open Declaremods
+open Misctypes
open Prim
open Constr
@@ -240,7 +241,7 @@ GEXTEND Gram
def_body:
[ [ bl = binders; ":="; red = reduce; c = lconstr ->
(match c with
- CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t)
+ CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
| _ -> DefineBody (bl, red, c, None))
| bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
DefineBody (bl, red, c, Some t)
@@ -343,7 +344,7 @@ GEXTEND Gram
(oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
| l = binders; ":="; b = lconstr -> fun id ->
match b with
- | CCast(_,b, Glob_term.CastConv (_, t)) ->
+ | CCast(_,b, (CastConv t|CastVM t)) ->
(None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
| _ ->
(None,DefExpr(id,mkCLambdaN loc l b,None)) ] ]
@@ -568,7 +569,7 @@ GEXTEND Gram
VernacContext c
| IDENT "Instance"; namesup = instance_name; ":";
- expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200";
+ expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
pri = OPT [ "|"; i = natural -> i ] ;
props = [ ":="; "{"; r = record_declaration; "}" -> Some r |
":="; c = lconstr -> Some c | -> None ] ->
@@ -714,7 +715,7 @@ GEXTEND Gram
(* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
- expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200";
+ expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
pri = OPT [ "|"; i = natural -> i ] ->
VernacInstance (true, not (use_section_locality ()),
snd namesup, (fst namesup, expl, t),
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 3cb553437..7c26ac124 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -20,6 +20,8 @@ open Libnames
open Nametab
open Detyping
open Tok
+open Misctypes
+open Decl_kinds
(* Generic xml parser without raw data *)
@@ -96,8 +98,8 @@ let inductive_of_cdata a = match global_of_cdata a with
let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
let sort_of_cdata (loc,a) = match a with
- | "Prop" -> GProp Null
- | "Set" -> GProp Pos
+ | "Prop" -> GProp
+ | "Set" -> GSet
| "Type" -> GType None
| _ -> user_err_loc (loc,"",str "sort expected.")
@@ -191,7 +193,7 @@ let rec interp_xml_constr = function
let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"CAST",al,[x1;x2]) ->
- GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
+ GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
| XmlTag (loc,"SORT",al,[]) ->
GSort (loc, get_xml_sort al)
| XmlTag (loc,s,_,_) ->
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 39fd88506..cae4b13d6 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -56,11 +56,13 @@ Lib
Goptions
Decl_kinds
Global
+Locusops
Termops
Namegen
Evd
Reductionops
Inductiveops
+Miscops
Glob_term
Detyping
Pattern
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ebcc53264..5bc6bddd9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -17,6 +17,7 @@ open Topconstr
open Tacexpr
open Libnames
open Compat
+open Misctypes
(** The parser of Coq *)
@@ -220,7 +221,7 @@ module Tactic :
val int_or_var : int or_var Gram.entry
val red_expr : raw_red_expr Gram.entry
val simple_tactic : raw_atomic_tactic_expr Gram.entry
- val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry
+ val simple_intropattern : intro_pattern_expr located Gram.entry
val tactic_arg : raw_tactic_arg Gram.entry
val tactic_expr : raw_tactic_expr Gram.entry
val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 98ed6883e..45ea77d13 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -21,6 +21,9 @@ open Pattern
open Glob_term
open Constrextern
open Termops
+open Decl_kinds
+open Misctypes
+open Locus
(*i*)
let sep_v = fun _ -> str"," ++ spc()
@@ -110,8 +113,8 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
let pr_universe = Univ.pr_uni
let pr_glob_sort = function
- | GProp Term.Null -> str "Prop"
- | GProp Term.Pos -> str "Set"
+ | GProp -> str "Prop"
+ | GSet -> str "Set"
| GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
let pr_id = pr_id
@@ -253,7 +256,7 @@ let pr_binder_among_many pr_c = function
pr_binder true pr_c (nal,k,t)
| LocalRawDef (na,c) ->
let c,topt = match c with
- | CCast(_,c, CastConv (_,t)) -> c, t
+ | CCast(_,c, (CastConv t|CastVM t)) -> c, t
| _ -> c, CHole (dummy_loc, None) in
surround (pr_lname na ++ pr_opt_type pr_c topt ++
str":=" ++ cut() ++ pr_c c)
@@ -530,13 +533,12 @@ let pr pr sep inherited a =
| CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
| CSort (_,s) -> pr_glob_sort s, latom
- | CCast (_,a,CastConv (k,b)) ->
- let s = match k with VMcast -> "<:" | DEFAULTcast | REVERTcast -> ":" in
- hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
- lcast
- | CCast (_,a,CastCoerce) ->
- hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
- lcast
+ | CCast (_,a,b) ->
+ hv 0 (pr mt (lcast,L) a ++ cut () ++
+ match b with
+ | CastConv b -> str ":" ++ pr mt (-lcast,E) b
+ | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
+ | CastCoerce -> str ":>"), lcast
| CNotation (_,"( _ )",([t],[],[])) ->
pr (fun()->str"(") (max_int,L) t ++ str")", latom
| CNotation (_,s,env) ->
@@ -581,12 +583,15 @@ let pr_cases_pattern_expr = pr_patt ltop
let pr_binders = pr_undelimited_binders spc (pr ltop)
-let pr_with_occurrences pr occs =
+let pr_with_occurrences pr (occs,c) =
match occs with
- ((false,[]),c) -> pr c
- | ((nowhere_except_in,nl),c) ->
+ | AllOccurrences -> pr c
+ | NoOccurrences -> failwith "pr_with_occurrences: no occurrences"
+ | OnlyOccurrences nl ->
hov 1 (pr c ++ spc() ++ str"at " ++
- (if nowhere_except_in then mt() else str "- ") ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+ | AllOccurrencesBut nl ->
+ hov 1 (pr c ++ spc() ++ str"at - " ++
hov 0 (prlist_with_sep spc (pr_or_var int) nl))
let pr_red_flag pr r =
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index c61d4c206..1497c90e7 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -16,7 +16,8 @@ open Topconstr
open Names
open Errors
open Util
-open Genarg
+open Misctypes
+open Locus
val extract_lam_binders :
constr_expr -> local_binder list * constr_expr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 513034194..c50ab9fcd 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -20,6 +20,9 @@ open Pattern
open Ppextend
open Ppconstr
open Printer
+open Misctypes
+open Locus
+open Decl_kinds
let pr_global x = Nametab.pr_global_env Idset.empty x
@@ -384,11 +387,11 @@ let pr_by_tactic prt = function
| tac -> spc() ++ str "by " ++ prt tac
let pr_hyp_location pr_id = function
- | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs
- | occs, Termops.InHypTypeOnly ->
+ | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+ | occs, InHypTypeOnly ->
spc () ++
pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
- | occs, Termops.InHypValueOnly ->
+ | occs, InHypValueOnly ->
spc () ++
pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
@@ -403,17 +406,17 @@ let pr_in_hyp_as pr_id = function
| Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat
let pr_clauses default_is_concl pr_id = function
- | { onhyps=Some []; concl_occs=occs }
- when occs = all_occurrences_expr & default_is_concl = Some true -> mt ()
- | { onhyps=None; concl_occs=occs }
- when occs = all_occurrences_expr & default_is_concl = Some false -> mt ()
+ | { onhyps=Some []; concl_occs=AllOccurrences }
+ when default_is_concl = Some true -> mt ()
+ | { onhyps=None; concl_occs=AllOccurrences }
+ when default_is_concl = Some false -> mt ()
| { onhyps=None; concl_occs=occs } ->
- if occs = no_occurrences_expr then pr_in (str " * |-")
+ if occs = NoOccurrences then pr_in (str " * |-")
else pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
| { onhyps=Some l; concl_occs=occs } ->
pr_in
(prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++
- (if occs = no_occurrences_expr then mt ()
+ (if occs = NoOccurrences then mt ()
else pr_with_occurrences (fun () -> str" |- *") (occs,())))
let pr_orient b = if b then mt () else str " <-"
@@ -690,7 +693,7 @@ and pr_atom1 = function
| TacGeneralizeDep c ->
hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
pr_constrarg c)
- | TacLetTac (na,c,cl,true) when cl = nowhere ->
+ | TacLetTac (na,c,cl,true) when cl = Locusops.nowhere ->
hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
| TacLetTac (na,c,cl,b) ->
hov 1 ((if b then str "set" else str "remember") ++
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index d85f1ec3f..afcc83c68 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -17,6 +17,7 @@ open Pattern
open Ppextend
open Environ
open Evd
+open Misctypes
val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index fad4e879e..5dbef1fe5 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -31,6 +31,7 @@ open Printmod
open Libnames
open Nametab
open Recordops
+open Misctypes
type object_pr = {
print_inductive : mutual_inductive -> std_ppcmds;
@@ -644,11 +645,11 @@ let print_any_name = function
"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
let print_name = function
- | Genarg.ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,ntn,sc) ->
print_any_name
(Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
ntn sc))
- | Genarg.AN ref ->
+ | AN ref ->
print_any_name (locate_any_name ref)
let print_opaque_name qid =
@@ -686,11 +687,11 @@ let print_about_any k =
hov 0 (pr_located_qualid k) ++ fnl()
let print_about = function
- | Genarg.ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,ntn,sc) ->
print_about_any
(Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
ntn sc))
- | Genarg.AN ref ->
+ | AN ref ->
print_about_any (locate_any_name ref)
(* for debug *)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 40ba7f047..b3271d141 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -16,7 +16,7 @@ open Environ
open Reductionops
open Libnames
open Nametab
-open Genarg
+open Misctypes
(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index f5225feb3..543240a82 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -17,6 +17,7 @@ open Pp
open Compat
open Pcaml
open PcamlSig
+open Misctypes
let loc = dummy_loc
let dloc = <:expr< Pp.dummy_loc >>
@@ -33,8 +34,8 @@ EXTEND
<:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ]
;
sort:
- [ [ "Set" -> GProp Pos
- | "Prop" -> GProp Null
+ [ [ "Set" -> GSet
+ | "Prop" -> GProp
| "Type" -> GType None ] ]
;
ident:
@@ -49,9 +50,9 @@ EXTEND
constr:
[ "200" RIGHTA
[ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr ->
- <:expr< Glob_term.GProd ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >>
+ <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >>
| "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr ->
- <:expr< Glob_term.GLambda ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >>
+ <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >>
| "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr ->
<:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >>
(* fix todo *)
@@ -61,7 +62,7 @@ EXTEND
<:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
| "90" RIGHTA
[ c1 = constr; "->"; c2 = SELF ->
- <:expr< Glob_term.GProd ($dloc$,Anonymous,Glob_term.Explicit,$c1$,$c2$) >> ]
+ <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ]
| "75" RIGHTA
[ "~"; c = constr ->
apply_ref <:expr< coq_not_ref >> [c] ]
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f36465207..6ef7ba1d8 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -51,18 +51,18 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
let mlexpr_of_loc loc = <:expr< $dloc$ >>
let mlexpr_of_by_notation f = function
- | Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
- | Genarg.ByNotation (loc,s,sco) ->
- <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
+ | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >>
+ | Misctypes.ByNotation (loc,s,sco) ->
+ <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
let mlexpr_of_intro_pattern = function
- | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
- | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
- | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
- | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
- | Genarg.IntroIdentifier id ->
- <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
- | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ ->
+ | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >>
+ | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
+ | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
+ | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
+ | Misctypes.IntroIdentifier id ->
+ <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
+ | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ ->
failwith "mlexpr_of_intro_pattern: TODO"
let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
@@ -72,34 +72,40 @@ let mlexpr_of_or_metaid f = function
| Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >>
let mlexpr_of_quantified_hypothesis = function
- | Glob_term.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
- | Glob_term.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
+ | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
+ | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
let mlexpr_of_or_var f = function
- | Glob_term.ArgArg x -> <:expr< Glob_term.ArgArg $f x$ >>
- | Glob_term.ArgVar id -> <:expr< Glob_term.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
+ | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
+ | Misctypes.ArgVar id -> <:expr< Misctypes.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_pair
- mlexpr_of_bool (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
+let mlexpr_of_occs = function
+ | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>
+ | Locus.AllOccurrencesBut l ->
+ <:expr< Locus.AllOccurrencesBut
+ $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
+ | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >>
+ | Locus.OnlyOccurrences l ->
+ <:expr< Locus.OnlyOccurrences
+ $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
let mlexpr_of_hyp_location = function
- | occs, Termops.InHyp ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHyp) >>
- | occs, Termops.InHypTypeOnly ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypTypeOnly) >>
- | occs, Termops.InHypValueOnly ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypValueOnly) >>
+ | occs, Locus.InHyp ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >>
+ | occs, Locus.InHypTypeOnly ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >>
+ | occs, Locus.InHypValueOnly ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >>
let mlexpr_of_clause cl =
- <:expr< {Tacexpr.onhyps=
+ <:expr< {Locus.onhyps=
$mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location)
- cl.Tacexpr.onhyps$;
- Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >>
+ cl.Locus.onhyps$;
+ Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >>
let mlexpr_of_red_flags {
Glob_term.rBeta = bb;
@@ -120,8 +126,8 @@ let mlexpr_of_explicitation = function
| Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
let mlexpr_of_binding_kind = function
- | Glob_term.Implicit -> <:expr< Glob_term.Implicit >>
- | Glob_term.Explicit -> <:expr< Glob_term.Explicit >>
+ | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >>
+ | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >>
let mlexpr_of_binder_kind = function
| Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
@@ -215,14 +221,14 @@ let rec mlexpr_of_may_eval f = function
<:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >>
let mlexpr_of_binding_kind = function
- | Glob_term.ExplicitBindings l ->
+ | Misctypes.ExplicitBindings l ->
let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
- <:expr< Glob_term.ExplicitBindings $l$ >>
- | Glob_term.ImplicitBindings l ->
+ <:expr< Misctypes.ExplicitBindings $l$ >>
+ | Misctypes.ImplicitBindings l ->
let l = mlexpr_of_list mlexpr_of_constr l in
- <:expr< Glob_term.ImplicitBindings $l$ >>
- | Glob_term.NoBindings ->
- <:expr< Glob_term.NoBindings >>
+ <:expr< Misctypes.ImplicitBindings $l$ >>
+ | Misctypes.NoBindings ->
+ <:expr< Misctypes.NoBindings >>
let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 11:35:54 +0000