summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/argextend.ml426
-rw-r--r--parsing/egrammar.ml48
-rw-r--r--parsing/g_constr.ml464
-rw-r--r--parsing/g_ltac.ml419
-rw-r--r--parsing/g_prim.ml44
-rw-r--r--parsing/g_proofs.ml417
-rw-r--r--parsing/g_tactic.ml478
-rw-r--r--parsing/g_vernac.ml4227
-rw-r--r--parsing/lexer.ml449
-rw-r--r--parsing/pcoq.ml45
-rw-r--r--parsing/pcoq.mli5
-rw-r--r--parsing/ppconstr.ml112
-rw-r--r--parsing/ppconstr.mli10
-rw-r--r--parsing/pptactic.ml59
-rw-r--r--parsing/ppvernac.ml172
-rw-r--r--parsing/prettyp.ml13
-rw-r--r--parsing/prettyp.mli4
-rw-r--r--parsing/printer.ml19
-rw-r--r--parsing/printmod.ml6
-rw-r--r--parsing/q_constr.ml44
-rw-r--r--parsing/q_coqast.ml444
-rw-r--r--parsing/search.ml17
-rw-r--r--parsing/search.mli9
-rw-r--r--parsing/vernacextend.ml45
24 files changed, 569 insertions, 447 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 57e88133..bd6be424 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: argextend.ml4 10122 2007-09-15 10:35:59Z letouzey $ *)
+(* $Id: argextend.ml4 11622 2008-11-23 08:45:56Z herbelin $ *)
open Genarg
open Q_util
@@ -25,7 +25,7 @@ let rec make_rawwit loc = function
| StringArgType -> <:expr< Genarg.rawwit_string >>
| PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
| IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
- | IdentArgType -> <:expr< Genarg.rawwit_ident >>
+ | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >>
| VarArgType -> <:expr< Genarg.rawwit_var >>
| RefArgType -> <:expr< Genarg.rawwit_ref >>
| SortArgType -> <:expr< Genarg.rawwit_sort >>
@@ -50,7 +50,7 @@ let rec make_globwit loc = function
| StringArgType -> <:expr< Genarg.globwit_string >>
| PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
| IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
- | IdentArgType -> <:expr< Genarg.globwit_ident >>
+ | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >>
| VarArgType -> <:expr< Genarg.globwit_var >>
| RefArgType -> <:expr< Genarg.globwit_ref >>
| QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
@@ -75,7 +75,7 @@ let rec make_wit loc = function
| StringArgType -> <:expr< Genarg.wit_string >>
| PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
| IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
- | IdentArgType -> <:expr< Genarg.wit_ident >>
+ | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >>
| VarArgType -> <:expr< Genarg.wit_var >>
| RefArgType -> <:expr< Genarg.wit_ref >>
| QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
@@ -163,16 +163,27 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
end
>>
-let declare_vernac_argument loc s cl =
+let declare_vernac_argument loc s pr cl =
let se = mlexpr_of_string s in
+ let wit = <:expr< $lid:"wit_"^s$ >> in
let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
+ let globwit = <:expr< $lid:"globwit_"^s$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+ let pr_rules = match pr with
+ | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
+ | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
<:str_item<
declare
- value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x;
+ value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
+ ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
+ $lid:"rawwit_"^s$) = Genarg.create_arg $se$;
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None
[(None, None, $rules$)];
+ Pptactic.declare_extra_genarg_pprule
+ ($rawwit$, $pr_rules$)
+ ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer")
+ ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer");
end
>>
@@ -202,11 +213,12 @@ EXTEND
failwith "Argument entry names must be lowercase";
declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l
| "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+ pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
OPT "|"; l = LIST1 argrule SEP "|";
"END" ->
if String.capitalize s = s then
failwith "Argument entry names must be lowercase";
- declare_vernac_argument loc s l ] ]
+ declare_vernac_argument loc s pr l ] ]
;
argtype:
[ "2"
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 825d1af0..43836dbb 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: egrammar.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
open Pp
open Util
@@ -52,58 +52,56 @@ type prod_item =
| NonTerm of constr_production_entry *
(Names.identifier * constr_production_entry) option
-type 'a action_env = (identifier * 'a) list
+type 'a action_env = 'a list * 'a list list
let make_constr_action
(f : loc -> constr_expr action_env -> constr_expr) pil =
- let rec make (env : constr_expr action_env) = function
+ let rec make (env,envlist as fullenv : constr_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gramext.action (fun loc -> f loc fullenv)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gramext.action (fun _ -> make fullenv tl)
| Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
- Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
+ Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
- Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
+ Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
- make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+ make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bigint.bigint) ->
- make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
+ make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| Some (p, ETConstrList _) :: tl ->
- Gramext.action (fun (v:constr_expr list) ->
- let dummyid = Ident (dummy_loc,id_of_string "_") in
- make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
+ Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
| Some (p, ETPattern) :: tl ->
failwith "Unexpected entry of type cases pattern" in
- make [] (List.rev pil)
+ make ([],[]) (List.rev pil)
let make_cases_pattern_action
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
- let rec make (env : cases_pattern_expr action_env) = function
+ let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gramext.action (fun loc -> f loc fullenv)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gramext.action (fun _ -> make fullenv tl)
| Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
- Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl)
+ Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
Gramext.action (fun (v:reference) ->
- make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
+ make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
- make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
+ make
+ (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bigint.bigint) ->
- make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
+ make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| Some (p, ETConstrList _) :: tl ->
Gramext.action (fun (v:cases_pattern_expr list) ->
- let dummyid = Ident (dummy_loc,id_of_string "_") in
- make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
+ make (env, v :: envlist) tl)
| Some (p, (ETPattern | ETOther _)) :: tl ->
failwith "Unexpected entry of type cases pattern or other" in
- make [] (List.rev pil)
+ make ([],[]) (List.rev pil)
let make_constr_prod_item univ assoc from forpat = function
| Term tok -> (Gramext.Stoken tok, None)
@@ -133,11 +131,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt =
let extend_constr_notation (n,assoc,ntn,rule) =
(* Add the notation in constr *)
- let mkact loc env = CNotation (loc,ntn,List.map snd env) in
+ let mkact loc env = CNotation (loc,ntn,env) in
let e = get_constr_entry false (ETConstr (n,())) in
extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
(* Add the notation in cases_pattern *)
- let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
+ let mkact loc env = CPatNotation (loc,ntn,env) in
let e = get_constr_entry true (ETConstr (n,())) in
extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
true rule
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b93fdadd..cdce13e6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_constr.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: g_constr.ml4 11709 2008-12-20 11:42:15Z msozeau $ *)
open Pcoq
open Constr
@@ -24,7 +24,8 @@ open Util
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
"end"; "as"; "let"; "if"; "then"; "else"; "return";
- "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
+ "Prop"; "Set"; "Type"; ".("; "_"; "..";
+ "`{"; "`("; "{|"; "|}" ]
let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
@@ -41,6 +42,11 @@ let loc_of_binder_let = function
| LocalRawDef ((loc,_),_)::_ -> loc
| _ -> dummy_loc
+let binders_of_lidents l =
+ List.map (fun (loc, id) ->
+ LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
+ CHole (loc, Some (Evd.BinderType (Name id))))) l
+
let rec index_and_rec_order_of_annot loc bl ann =
match names_of_local_assums bl,ann with
| [loc,Name id], (None, r) -> Some (loc, id), r
@@ -124,12 +130,24 @@ let ident_colon =
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
+let ident_with =
+ Gram.Entry.of_parser "ident_with"
+ (fun strm ->
+ match Stream.npeek 1 strm with
+ | [("IDENT",s)] ->
+ (match Stream.npeek 2 strm with
+ | [_; ("", "with")] ->
+ Stream.junk strm; Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure)
+ | _ -> raise Stream.Failure)
+
let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
constr_pattern lconstr_pattern Constr.ident
- binder binder_let binders_let
+ binder binder_let binders_let record_declaration
binders_let_fixannot typeclass_constraint pattern appl_arg;
Constr.ident:
[ [ id = Prim.ident -> id
@@ -202,8 +220,14 @@ GEXTEND Gram
| "("; c = operconstr LEVEL "200"; ")" ->
(match c with
CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CNotation(loc,"( _ )",[c])
- | _ -> c) ] ]
+ CNotation(loc,"( _ )",([c],[]))
+ | _ -> c)
+ | "{|"; c = record_declaration; "|}" -> c
+ | "`{"; c = operconstr LEVEL "200"; "}" ->
+ CGeneralization (loc, Implicit, None, c)
+ | "`("; c = operconstr LEVEL "200"; ")" ->
+ CGeneralization (loc, Explicit, None, c)
+ ] ]
;
forall:
[ [ "forall" -> ()
@@ -215,6 +239,16 @@ GEXTEND Gram
| IDENT "λ" -> ()
] ]
;
+ record_declaration:
+ [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
+(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
+(* CRecord (loc, Some c, fs) *)
+ ] ]
+ ;
+ record_field_declaration:
+ [ [ id = identref; params = LIST0 identref; ":="; c = lconstr ->
+ (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
+ ;
binder_constr:
[ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
mkCProdN loc bl c
@@ -337,7 +371,7 @@ GEXTEND Gram
| "("; p = pattern LEVEL "200"; ")" ->
(match p with
CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CPatNotation(loc,"( _ )",[p])
+ CPatNotation(loc,"( _ )",([p],[]))
| _ -> p)
| n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
| s = string -> CPatPrim (loc, String s) ] ]
@@ -398,12 +432,10 @@ GEXTEND Gram
[LocalRawAssum ([id],Default Implicit,c)]
| "{"; id=name; idl=LIST1 name; "}" ->
List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
- | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc
- | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
- | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
+ | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+ | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
] ]
;
binder:
@@ -413,13 +445,13 @@ GEXTEND Gram
] ]
;
typeclass_constraint:
- [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
- | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+ [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
+ | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
id, expl, c
- | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+ | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
(loc, Name iid), expl, c
| c = operconstr LEVEL "200" ->
- (loc, Anonymous), Implicit, c
+ (loc, Anonymous), false, c
] ]
;
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index dbd81e7f..316bf8e1 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_ltac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: g_ltac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *)
open Pp
open Util
@@ -165,11 +165,24 @@ GEXTEND Gram
match_pattern:
[ [ IDENT "context"; oid = OPT Constr.ident;
"["; pc = Constr.lconstr_pattern; "]" ->
- Subterm (oid, pc)
+ Subterm (false,oid, pc)
+ | IDENT "appcontext"; oid = OPT Constr.ident;
+ "["; pc = Constr.lconstr_pattern; "]" ->
+ Subterm (true,oid, pc)
| pc = Constr.lconstr_pattern -> Term pc ] ]
;
match_hyps:
- [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ]
+ [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp)
+ | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt)
+ | na = name; ":="; mpv = match_pattern ->
+ let t, ty =
+ match mpv with
+ | Term t -> (match t with
+ | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty)
+ | _ -> mpv, None)
+ | _ -> mpv, None
+ in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty)
+ ] ]
;
match_context_rule:
[ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 1e738384..76225d77 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(*i $Id: g_prim.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: g_prim.ml4 11525 2008-10-30 22:18:54Z amahboub $ i*)
open Pcoq
open Names
@@ -45,7 +45,7 @@ GEXTEND Gram
[ [ s = IDENT -> id_of_string s ] ]
;
pattern_ident:
- [ [ s = PATTERNIDENT -> id_of_string s ] ]
+ [ [ LEFTQMARK; id = ident -> id ] ]
;
pattern_identref:
[ [ id = pattern_ident -> (loc, id) ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 05878e97..655bb267 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_proofs.ml4 10628 2008-03-06 14:56:08Z msozeau $ *)
+(* $Id: g_proofs.ml4 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pcoq
@@ -90,9 +90,12 @@ GEXTEND Gram
| IDENT "Go"; IDENT "next" -> VernacGo GoNext
| IDENT "Guarded" -> VernacCheckGuard
(* Hints for Auto and EAuto *)
- | IDENT "Hint"; local = locality; h = hint;
+ | IDENT "Create"; IDENT "HintDb" ;
+ id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
+ VernacCreateHintDb (use_locality (), id, b)
+ | IDENT "Hint"; local = obsolete_locality; h = hint;
dbnames = opt_hintbases ->
- VernacHints (local,dbnames, h)
+ VernacHints (enforce_locality_of local,dbnames, h)
(*This entry is not commented, only for debug*)
@@ -101,16 +104,18 @@ GEXTEND Gram
[Genarg.in_gen Genarg.rawwit_constr c])
] ];
- locality:
+ obsolete_locality:
[ [ IDENT "Local" -> true | -> false ] ]
;
hint:
[ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] ->
- HintsResolve (List.map (fun x -> (n, x)) lc)
+ HintsResolve (List.map (fun x -> (n, true, x)) lc)
| IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+ | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
+ | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
| IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
| IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
- | IDENT "Extern"; n = natural; c = constr_pattern ; "=>";
+ | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
tac = tactic ->
HintsExtern (n,c,tac)
| IDENT "Destruct";
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 49f00d40..7bebf6db 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_tactic.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: g_tactic.ml4 11741 2009-01-03 14:34:39Z herbelin $ *)
open Pp
open Pcoq
@@ -18,6 +18,7 @@ open Rawterm
open Genarg
open Topconstr
open Libnames
+open Termops
let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
@@ -215,7 +216,8 @@ GEXTEND Gram
;
smart_global:
[ [ c = global -> AN c
- | s = ne_string -> ByNotation (loc,s) ] ]
+ | s = ne_string; sc = OPT ["%"; key = IDENT -> key ] ->
+ ByNotation (loc,s,sc) ] ]
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
@@ -255,6 +257,11 @@ GEXTEND Gram
| "?" -> loc, IntroAnonymous
| id = ident -> loc, IntroIdentifier id ] ]
;
+ intropattern_modifier:
+ [ [ IDENT "_eqn";
+ id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
+ -> id ] ]
+ ;
simple_intropattern:
[ [ pat = disjunctive_intropattern -> pat
| pat = naming_intropattern -> pat
@@ -362,10 +369,14 @@ GEXTEND Gram
[ [ "*"; occs = occs -> occs
| -> no_occurrences_expr ] ]
;
- simple_clause:
+ in_hyp_list:
[ [ "in"; idl = LIST1 id_or_meta -> idl
| -> [] ] ]
;
+ in_hyp_as:
+ [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
+ | -> None ] ]
+ ;
orient:
[ [ "->" -> true
| "<-" -> false
@@ -404,18 +415,17 @@ GEXTEND Gram
eliminator:
[ [ "using"; el = constr_with_bindings -> el ] ]
;
- with_names:
- [ [ "as"; ipat = simple_intropattern -> ipat
- | -> dummy_loc,IntroAnonymous ] ]
+ as_ipat:
+ [ [ "as"; ipat = simple_intropattern -> Some ipat
+ | -> None ] ]
;
with_inversion_names:
- [ [ "as"; ipat = disjunctive_intropattern -> Some ipat
+ [ [ "as"; ipat = simple_intropattern -> Some ipat
| -> None ] ]
;
with_induction_names:
- [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern
+ [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier
-> (eq,Some ipat)
- | "as"; eq = naming_intropattern -> (Some eq,None)
| -> (None,None) ] ]
;
as_name:
@@ -433,19 +443,10 @@ GEXTEND Gram
[ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
;
rewriter :
- [ [
- (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally
- produce a pattern_ident *)
- c = pattern_ident ->
- let c = (CRef (Ident (loc,c)), NoBindings) in
- (RepeatStar, c)
- | n = natural; c = pattern_ident ->
- let c = (CRef (Ident (loc,c)), NoBindings) in
- (UpTo n, c)
- | "!"; c = constr_with_bindings -> (RepeatPlus,c)
- | "?"; c = constr_with_bindings -> (RepeatStar,c)
+ [ [ "!"; c = constr_with_bindings -> (RepeatPlus,c)
+ | ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c)
| n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
- | n = natural; "?"; c = constr_with_bindings -> (UpTo n,c)
+ | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings -> (UpTo n,c)
| n = natural; c = constr_with_bindings -> (Precisely n,c)
| c = constr_with_bindings -> (Precisely 1, c)
] ]
@@ -480,13 +481,14 @@ GEXTEND Gram
| IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
| IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
- | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," ->
- TacApply (true,false,cl)
- | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," ->
- TacApply (true,true,cl)
- | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","
- -> TacApply (false,false,cl)
- | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> TacApply (false,true,cl)
+ | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+ inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
+ | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ",";
+ inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp)
+ | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+ inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp)
+ | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP",";
+ inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp)
| IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
TacElim (false,cl,el)
| IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
@@ -518,15 +520,15 @@ GEXTEND Gram
(* Begin compatibility *)
| IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
c = lconstr; ")" ->
- TacAssert (None,(loc,IntroIdentifier id),c)
+ TacAssert (None,Some (loc,IntroIdentifier id),c)
| IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAssert (Some tac,(loc,IntroIdentifier id),c)
+ TacAssert (Some tac,Some (loc,IntroIdentifier id),c)
(* End compatibility *)
- | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
+ | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
TacAssert (Some tac,ipat,c)
- | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = with_names ->
+ | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
TacAssert (None,ipat,c)
| IDENT "cut"; c = constr -> TacCut c
@@ -587,8 +589,8 @@ GEXTEND Gram
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
| IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
| IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
- | IDENT "move"; dep = [IDENT "dependent" -> true | -> false];
- hfrom = id_or_meta; hto = move_location -> TacMove (dep,hfrom,hto)
+ | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
+ TacMove (true,hfrom,hto)
| IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
| IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
@@ -627,18 +629,18 @@ GEXTEND Gram
TacInversion (DepInversion (k,co,ids),hyp)
| IDENT "simple"; IDENT "inversion";
hyp = quantified_hypothesis; ids = with_inversion_names;
- cl = simple_clause ->
+ cl = in_hyp_list ->
TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
| IDENT "inversion";
hyp = quantified_hypothesis; ids = with_inversion_names;
- cl = simple_clause ->
+ cl = in_hyp_list ->
TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
| IDENT "inversion_clear";
hyp = quantified_hypothesis; ids = with_inversion_names;
- cl = simple_clause ->
+ cl = in_hyp_list ->
TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
| IDENT "inversion"; hyp = quantified_hypothesis;
- "using"; c = constr; cl = simple_clause ->
+ "using"; c = constr; cl = in_hyp_list ->
TacInversion (InversionUsing (c,cl), hyp)
(* Conversion *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 87c11164..f960492e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_vernac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: g_vernac.ml4 11809 2009-01-20 11:39:55Z aspiwack $ *)
open Pp
@@ -46,7 +46,9 @@ let noedit_mode = Gram.Entry.create "vernac:noedit_command"
let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
let thm_token = Gram.Entry.create "vernac:thm_token"
let def_body = Gram.Entry.create "vernac:def_body"
+let decl_notation = Gram.Entry.create "vernac:decl_notation"
let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
+let record_field = Gram.Entry.create "vernac:record_field"
let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
let get_command_entry () =
@@ -62,7 +64,13 @@ let default_command_entry =
let no_hook _ _ = ()
GEXTEND Gram
GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
- vernac:
+ vernac: FIRST
+ [ [ IDENT "Time"; locality; v = vernac_aux ->
+ check_locality (); VernacTime v
+ | locality; v = vernac_aux ->
+ check_locality (); v ] ]
+ ;
+ vernac_aux:
(* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
(* "." is still in the stream and discard_to_dot works correctly *)
[ [ g = gallina; "." -> g
@@ -72,12 +80,14 @@ GEXTEND Gram
| "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
] ]
;
- vernac: FIRST
- [ [ IDENT "Time"; v = vernac -> VernacTime v ] ]
- ;
- vernac: LAST
+ vernac_aux: LAST
[ [ prfcom = default_command_entry -> prfcom ] ]
;
+ locality:
+ [ [ IDENT "Local" -> locality_flag := Some true
+ | IDENT "Global" -> locality_flag := Some false
+ | -> locality_flag := None ] ]
+ ;
noedit_mode:
[ [ c = subgoal_command -> c None] ]
;
@@ -104,7 +114,6 @@ GEXTEND Gram
;
END
-
let test_plurial_form = function
| [(_,([_],_))] ->
Flags.if_verbose warning
@@ -119,7 +128,7 @@ let no_coercion loc (c,x) =
(* Gallina declarations *)
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
- typeclass_context typeclass_constraint;
+ typeclass_context typeclass_constraint record_field decl_notation;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
@@ -142,6 +151,8 @@ GEXTEND Gram
(* Gallina inductive declarations *)
| f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
+ let (k,f) = f in
+ let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
VernacInductive (f,indl)
| IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
VernacFixpoint (recs,true)
@@ -158,16 +169,12 @@ GEXTEND Gram
gallina_ext:
[ [ b = record_token; oc = opt_coercion; name = identref;
ps = binders_let;
- s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ];
- ":="; cstr = OPT identref; "{";
- fs = LIST0 record_field SEP ";"; "}" ->
- VernacRecord (b,(oc,name),ps,s,cstr,fs)
-(* Non port ?
- | f = finite_token; s = csort; id = identref;
- indpar = LIST0 simple_binder; ":="; lc = constructor_list ->
- VernacInductive (f,[id,None,indpar,s,lc])
-*)
- ] ]
+ s = OPT [ ":"; s = lconstr -> s ];
+ cfs = [ ":="; l = constructor_list_or_record_decl -> l
+ | -> RecordDecl (None, []) ] ->
+ let (recf,indf) = b in
+ VernacInductive (indf,[((oc,name),ps,s,recf,cfs),None])
+ ] ]
;
typeclass_context:
[ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l
@@ -189,9 +196,8 @@ GEXTEND Gram
no_hook, (Local, Flags.boxed_definitions(), Definition)
| IDENT "Example" ->
no_hook, (Global, Flags.boxed_definitions(), Example)
- | IDENT "SubClass" -> Class.add_subclass_hook, (Global, false, SubClass)
- | IDENT "Local"; IDENT "SubClass" ->
- Class.add_subclass_hook, (Local, false, SubClass) ] ]
+ | IDENT "SubClass" ->
+ Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ]
;
assumption_token:
[ [ "Hypothesis" -> (Local, Logical)
@@ -210,11 +216,13 @@ GEXTEND Gram
[ ["Inline" -> true | -> false] ]
;
finite_token:
- [ [ "Inductive" -> true
- | "CoInductive" -> false ] ]
+ [ [ "Inductive" -> (Inductive_kw,Finite)
+ | "CoInductive" -> (CoInductive,CoFinite) ] ]
;
record_token:
- [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
+ [ [ IDENT "Record" -> (Record,BiFinite)
+ | IDENT "Structure" -> (Structure,BiFinite)
+ | IDENT "Class" -> (Class true,BiFinite) ] ]
;
(* Simple definitions *)
def_body:
@@ -237,15 +245,20 @@ GEXTEND Gram
;
(* Inductives and records *)
inductive_definition:
- [ [ id = identref; indpar = binders_let;
- c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
- ":="; lc = constructor_list; ntn = decl_notation ->
- ((id,indpar,c,lc),ntn) ] ]
- ;
- constructor_list:
- [ [ "|"; l = LIST1 constructor SEP "|" -> l
- | l = LIST1 constructor SEP "|" -> l
- | -> [] ] ]
+ [ [ id = identref; oc = opt_coercion; indpar = binders_let;
+ c = OPT [ ":"; c = lconstr -> c ];
+ ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
+ (((oc,id),indpar,c,lc),ntn) ] ]
+ ;
+ constructor_list_or_record_decl:
+ [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
+ | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
+ Constructors ((c id)::l)
+ | id = identref ; c = constructor_type -> Constructors [ c id ]
+ | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+ RecordDecl (Some cstr,fs)
+ | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+ | -> Constructors [] ] ]
;
(*
csort:
@@ -316,6 +329,9 @@ GEXTEND Gram
*)
(* ... with coercions *)
record_field:
+ [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
+ ;
+ record_binder:
[ [ id = name -> (false,AssumExpr(id,CHole (loc, None)))
| id = name; oc = of_type_with_opt_coercion; t = lconstr ->
(oc,AssumExpr (id,t))
@@ -336,12 +352,19 @@ GEXTEND Gram
[ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
(oc,(idl,c)) ] ]
;
+
+ constructor_type:
+ [[ l = binders_let;
+ t= [ coe = of_type_with_opt_coercion; c = lconstr ->
+ fun l id -> (coe,(id,mkCProdN loc l c))
+ | ->
+ fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ]
+ -> t l
+ ]]
+;
+
constructor:
- [ [ id = identref; l = binders_let;
- coe = of_type_with_opt_coercion; c = lconstr ->
- (coe,(id,mkCProdN loc l c))
- | id = identref; l = binders_let ->
- (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
+ [ [ id = identref; c=constructor_type -> c id ] ]
;
of_type_with_opt_coercion:
[ [ ":>" -> true
@@ -440,15 +463,12 @@ GEXTEND Gram
gallina_ext:
[ [ (* Transparent and Opaque *)
IDENT "Transparent"; l = LIST1 global ->
- VernacSetOpacity (true,[Conv_oracle.transparent,l])
+ VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l])
| IDENT "Opaque"; l = LIST1 global ->
- VernacSetOpacity (true,[Conv_oracle.Opaque, l])
+ VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l])
| IDENT "Strategy"; l =
LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
- VernacSetOpacity (false,l)
- | IDENT "Local"; IDENT "Strategy"; l =
- LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
- VernacSetOpacity (true,l)
+ VernacSetOpacity (use_locality (),l)
(* Canonical structure *)
| IDENT "Canonical"; IDENT "Structure"; qid = global ->
VernacCanonical qid
@@ -461,43 +481,31 @@ GEXTEND Gram
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = coerce_global_to_id qid in
- VernacDefinition ((Global,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+ VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
| IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
let s = coerce_global_to_id qid in
- VernacDefinition ((Local,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+ VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacIdentityCoercion (Local, f, s, t)
+ VernacIdentityCoercion (enforce_locality_exp (), f, s, t)
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacIdentityCoercion (Global, f, s, t)
+ VernacIdentityCoercion (use_locality_exp (), f, s, t)
| IDENT "Coercion"; IDENT "Local"; qid = global; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacCoercion (Local, qid, s, t)
+ VernacCoercion (enforce_locality_exp (), qid, s, t)
| IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
t = class_rawexpr ->
- VernacCoercion (Global, qid, s, t)
-
- (* Type classes, new syntax without artificial sup. *)
- | IDENT "Class"; qid = identref; pars = binders_let;
- s = [ ":"; c = sort -> Some (loc, c) | -> None ];
- props = typeclass_field_types ->
- VernacClass (qid, pars, s, [], props)
-
- (* Type classes *)
- | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
- qid = identref; pars = binders_let;
- s = [ ":"; c = sort -> Some (loc, c) | -> None ];
- props = typeclass_field_types ->
- VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
+ VernacCoercion (use_locality_exp (), qid, s, t)
| IDENT "Context"; c = binders_let ->
VernacContext c
- | global = [ IDENT "Global" -> true | -> false ];
- IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
+ | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
+ pri = OPT [ "|"; i = natural -> i ] ;
+ props = [ ":="; "{"; r = record_declaration; "}" -> r |
+ ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
let sup =
match sup with
None -> []
@@ -507,17 +515,15 @@ GEXTEND Gram
let (loc, id) = name in
(loc, Name id)
in
- VernacInstance (global, sup, (n, expl, t), props, pri)
+ VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri)
| IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
(* Implicit *)
- | IDENT "Implicit"; IDENT "Arguments";
- local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ];
- qid = global;
+ | IDENT "Implicit"; IDENT "Arguments"; qid = global;
pos = OPT [ "["; l = LIST0 implicit_name; "]" ->
List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
- VernacDeclareImplicits (local,qid,pos)
+ VernacDeclareImplicits (use_section_locality (),qid,pos)
| IDENT "Implicit"; ["Type" | IDENT "Types"];
idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
@@ -528,20 +534,6 @@ GEXTEND Gram
| "["; "!"; id = ident; "]" -> (id,true,true)
| "["; id = ident; "]" -> (id,true, false) ] ]
;
- typeclass_field_type:
- [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ]
- ;
- typeclass_field_def:
- [ [ id = identref; params = LIST0 identref; ":="; t = lconstr -> id, params, t ] ]
- ;
- typeclass_field_types:
- [ [ ":="; l = LIST1 typeclass_field_type SEP ";" -> l
- | -> [] ] ]
- ;
- typeclass_field_defs:
- [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l
- | -> [] ] ]
- ;
strategy_level:
[ [ IDENT "expand" -> Conv_oracle.Expand
| IDENT "opaque" -> Conv_oracle.Opaque
@@ -615,9 +607,15 @@ GEXTEND Gram
| IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
VernacSearch (SearchRewrite c, l)
| IDENT "SearchAbout";
- sl = [ "["; l = LIST1 [ r = global -> SearchRef r
- | s = ne_string -> SearchString s ]; "]" -> l
- | qid = global -> [SearchRef qid] ];
+ sl = [ "[";
+ l = LIST1 [
+ b = positive_search_mark; s = ne_string; sc = OPT scope
+ -> b, SearchString (s,sc)
+ | b = positive_search_mark; p = constr_pattern
+ -> b, SearchSubPattern p
+ ]; "]" -> l
+ | p = constr_pattern -> [true,SearchSubPattern p]
+ | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ];
l = in_or_out_modules ->
VernacSearch (SearchAbout sl, l)
@@ -672,7 +670,7 @@ GEXTEND Gram
| IDENT "Grammar"; ent = IDENT ->
(* This should be in "syntax" section but is here for factorization*)
PrintGrammar ent
- | IDENT "LoadPath" -> PrintLoadPath
+ | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir
| IDENT "Modules" ->
error "Print Modules is obsolete; use Print Libraries instead"
| IDENT "Libraries" -> PrintModules
@@ -697,7 +695,6 @@ GEXTEND Gram
| IDENT "Hint"; "*" -> PrintHintDb
| IDENT "HintDb"; s = IDENT -> PrintHintDbName s
| "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
- | IDENT "Setoids" -> PrintSetoids
| IDENT "Scopes" -> PrintScopes
| IDENT "Scope"; s = IDENT -> PrintScope s
| IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
@@ -743,6 +740,12 @@ GEXTEND Gram
| s = STRING -> CommentString s
| n = natural -> CommentInt n ] ]
;
+ positive_search_mark:
+ [ [ "-" -> false | -> true ] ]
+ ;
+ scope:
+ [ [ "%"; key = IDENT -> key ] ]
+ ;
END;
GEXTEND Gram
@@ -776,16 +779,16 @@ GEXTEND Gram
;;
(* Grammar extensions *)
-
+
GEXTEND Gram
GLOBAL: syntax;
syntax:
- [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT ->
- VernacOpenCloseScope (local,true,sc)
+ [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
+ VernacOpenCloseScope (enforce_locality_of local,true,sc)
- | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT ->
- VernacOpenCloseScope (local,false,sc)
+ | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
+ VernacOpenCloseScope (enforce_locality_of local,false,sc)
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
VernacDelimiters (sc,key)
@@ -793,44 +796,44 @@ GEXTEND Gram
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
- | IDENT "Arguments"; IDENT "Scope"; local = non_globality; qid = global;
- "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl)
+ | IDENT "Arguments"; IDENT "Scope"; qid = global;
+ "["; scl = LIST0 opt_scope; "]" ->
+ VernacArgumentsScope (use_non_locality (),qid,scl)
- | IDENT "Infix"; local = locality;
+ | IDENT "Infix"; local = obsolete_locality;
op = ne_string; ":="; p = global;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
- VernacInfix (local,(op,modl),p,sc)
- | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident;
- ":="; c = constr;
+ VernacInfix (enforce_locality_of local,(op,modl),p,sc)
+ | IDENT "Notation"; local = obsolete_locality; id = identref;
+ idl = LIST0 ident; ":="; c = constr;
b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
- VernacSyntacticDefinition (id,(idl,c),local,b)
- | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
+ VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b)
+ | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":=";
+ c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
- VernacNotation (local,c,(s,modl),sc)
+ VernacNotation (enforce_locality_of local,c,(s,modl),sc)
| IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
pil = LIST1 production_item; ":="; t = Tactic.tactic
-> VernacTacticNotation (n,pil,t)
- | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string;
+ | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
+ s = ne_string;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
- -> VernacSyntaxExtension (local,(s,l))
+ -> VernacSyntaxExtension (enforce_locality_of local,(s,l))
(* "Print" "Grammar" should be here but is in "command" entry in order
to factorize with other "Print"-based vernac entries *)
] ]
;
+ obsolete_locality:
+ [ [ IDENT "Local" -> true | -> false ] ]
+ ;
tactic_level:
[ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
;
- locality:
- [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ]
- ;
- non_globality:
- [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
- ;
level:
[ [ IDENT "level"; n = natural -> NumLevel n
| IDENT "next"; IDENT "level" -> NextLevel ] ]
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 1b0c24da..2633386f 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lexer.ml4 11238 2008-07-19 09:34:03Z herbelin $ i*)
+(*i $Id: lexer.ml4 11786 2009-01-14 13:07:34Z herbelin $ i*)
(*i camlp4use: "pr_o.cmo" i*)
@@ -175,7 +175,7 @@ let add_keyword str =
(* Adding a new token (keyword or special token). *)
let add_token (con, str) = match con with
| "" -> add_keyword str
- | "METAIDENT" | "PATTERNIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
+ | "METAIDENT" | "LEFTQMARK" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
-> ()
| _ ->
raise (Token.Error ("\
@@ -237,7 +237,7 @@ let rec string bp len = parser
let xml_output_comment = ref (fun _ -> ())
let set_xml_output_comment f = xml_output_comment := f
-(* Utilities for comment translation *)
+(* Utilities for comments in beautify *)
let comment_begin = ref None
let comm_loc bp = if !comment_begin=None then comment_begin := Some bp
@@ -280,7 +280,7 @@ let comment_stop ep =
if !Flags.xml_export && Buffer.length current > 0 &&
(!between_com || not(null_comment current_s)) then
!xml_output_comment current_s;
- (if Flags.do_translate() && Buffer.length current > 0 &&
+ (if Flags.do_beautify() && Buffer.length current > 0 &&
(!between_com || not(null_comment current_s)) then
let bp = match !comment_begin with
Some bp -> bp
@@ -315,7 +315,7 @@ let rec comment bp = parser bp2
| [< '')' >] -> push_string "*)";
| [< s >] -> real_push_char '*'; comment bp s >] -> ()
| [< ''"'; s >] ->
- if Flags.do_translate() then (push_string"\"";comm_string bp2 s)
+ if Flags.do_beautify() then (push_string"\"";comm_string bp2 s)
else ignore (string bp2 0 s);
comment bp s
| [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
@@ -372,31 +372,50 @@ let process_chars bp c cs =
| Some t -> (("", t), (bp, ep))
| None -> err (bp, ep) Undefined_token
-(* Parse what follows a dot/question mark *)
+let parse_after_dollar bp =
+ parser
+ | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ->
+ ("METAIDENT", get_buff len)
+ | [< s >] ->
+ match lookup_utf8 s with
+ | Utf8Token (UnicodeLetter, n) ->
+ ("METAIDENT", get_buff (ident_tail (nstore n 0 s) s))
+ | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '$' s)
+
+(* Parse what follows a dot *)
let parse_after_dot bp c =
- let constructor = if c = '?' then "PATTERNIDENT" else "FIELD" in
parser
| [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ->
- (constructor, get_buff len)
+ ("FIELD", get_buff len)
| [< s >] ->
match lookup_utf8 s with
| Utf8Token (UnicodeLetter, n) ->
- (constructor, get_buff (ident_tail (nstore n 0 s) s))
+ ("FIELD", get_buff (ident_tail (nstore n 0 s) s))
| AsciiChar | Utf8Token _ | EmptyStream ->
fst (process_chars bp c s)
+(* Parse what follows a question mark *)
+let parse_after_qmark bp s =
+ match Stream.peek s with
+ |Some ('a'..'z' | 'A'..'Z' | '_') -> ("LEFTQMARK", "")
+ |None -> ("","?")
+ | _ ->
+ match lookup_utf8 s with
+ | Utf8Token (UnicodeLetter, _) -> ("LEFTQMARK", "")
+ | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '?' s)
+
(* Parse a token in a char stream *)
let rec next_token = parser bp
| [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
comm_loc bp; push_char c; next_token s
- | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c);
- len = ident_tail (store 0 c) >] ep ->
- comment_stop bp;
- (("METAIDENT", get_buff len), (bp,ep))
- | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep ->
+ | [< ''$'; t = parse_after_dollar bp >] ep ->
+ comment_stop bp; (t, (ep, bp))
+ | [< ''.' as c; t = parse_after_dot bp c >] ep ->
comment_stop bp;
- if Flags.do_translate() & t=("",".") then between_com := true;
+ if Flags.do_beautify() & t=("",".") then between_com := true;
(t, (bp,ep))
+ | [< ''?'; s >] ep ->
+ let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
| [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
len = ident_tail (store 0 c) >] ep ->
let id = get_buff len in
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2e55b656..d0a9c3d8 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
-(*i $Id: pcoq.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: pcoq.ml4 11784 2009-01-14 11:36:32Z herbelin $ i*)
open Pp
open Util
@@ -407,7 +407,7 @@ module Prim =
let name = Gram.Entry.create "Prim.name"
let identref = Gram.Entry.create "Prim.identref"
- let pattern_ident = Gram.Entry.create "pattern_ident"
+ let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident"
let pattern_identref = Gram.Entry.create "pattern_identref"
(* A synonym of ident - maybe ident will be located one day *)
@@ -445,6 +445,7 @@ module Constr =
let binders_let = Gram.Entry.create "constr:binders_let"
let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
+ let record_declaration = Gram.Entry.create "constr:record_declaration"
let appl_arg = Gram.Entry.create "constr:appl_arg"
end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 525727ce..0a4b349f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: pcoq.mli 11784 2009-01-14 11:36:32Z herbelin $ i*)
open Util
open Names
@@ -166,7 +166,8 @@ module Constr :
val binder_let : local_binder list Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
- val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
+ val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
+ val record_declaration : constr_expr Gram.Entry.e
val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
end
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 5f6ffe87..d5357d86 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: ppconstr.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
(*i*)
open Util
@@ -62,42 +62,46 @@ let prec_of_prim_token = function
| Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
| String _ -> latom
-let env_assoc_value v env =
- try List.nth env (v-1)
- with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
-
-let decode_constrlist_value = function
- | CAppExpl (_,_,l) -> l
- | CApp (_,_,l) -> List.map fst l
- | _ -> anomaly "Ill-formed list argument of notation"
-
-let decode_patlist_value = function
- | CPatCstr (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
open Notation
-let rec print_hunk n decode pr env = function
- | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
- | UnpListMetaVar (e,prec,sl) ->
- prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
- (pr (n,prec)) (decode (env_assoc_value e env))
- | UnpTerminal s -> str s
- | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
- | UnpCut cut -> ppcmd_of_cut cut
-
-let pr_notation_gen decode pr s env =
+let print_hunks n pr (env,envlist) unp =
+ let env = ref env and envlist = ref envlist in
+ let pop r = let a = List.hd !r in r := List.tl !r; a in
+ let rec aux = function
+ | [] -> mt ()
+ | UnpMetaVar (_,prec) :: l ->
+ let c = pop env in pr (n,prec) c ++ aux l
+ | UnpListMetaVar (_,prec,sl) :: l ->
+ let cl = pop envlist in
+ let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+ let pp2 = aux l in
+ pp1 ++ pp2
+ | UnpTerminal s :: l -> str s ++ aux l
+ | UnpBox (b,sub) :: l ->
+ (* Keep order: side-effects *)
+ let pp1 = ppcmd_of_box b (aux sub) in
+ let pp2 = aux l in
+ pp1 ++ pp2
+ | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
+ aux unp
+
+let pr_notation pr s env =
let unpl, level = find_notation_printing_rule s in
- prlist (print_hunk level decode pr env) unpl, level
-
-let pr_notation = pr_notation_gen decode_constrlist_value
-let pr_patnotation = pr_notation_gen decode_patlist_value
+ print_hunks level pr env unpl, level
let pr_delimiters key strm =
strm ++ str ("%"^key)
+let pr_generalization bk ak c =
+ let hd, tl =
+ match bk with
+ | Implicit -> "{", "}"
+ | Explicit -> "(", ")"
+ in (* TODO: syntax Abstraction Kind *)
+ str "`" ++ str hd ++ c ++ str tl
+
let pr_com_at n =
- if Flags.do_translate() && n <> 0 then comment n
+ if Flags.do_beautify() && n <> 0 then comment n
else mt()
let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
@@ -179,9 +183,9 @@ let rec pr_patt sep inh p =
| CPatAtom (_,Some r) -> pr_reference r, latom
| CPatOr (_,pl) ->
hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
- | CPatNotation (_,"( _ )",[p]) ->
+ | CPatNotation (_,"( _ )",([p],[])) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
- | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
+ | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
| CPatPrim (_,p) -> pr_prim_token p, latom
| CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
in
@@ -209,17 +213,23 @@ let begin_of_binders = function
| b::_ -> begin_of_binder b
| _ -> 0
-let surround_binder k p =
+let surround_impl k p =
match k with
- Default Explicit -> hov 1 (str"(" ++ p ++ str")")
- | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
- | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
+ | Explicit -> str"(" ++ p ++ str")"
+ | Implicit -> str"{" ++ p ++ str"}"
+let surround_binder k p =
+ match k with
+ | Default b -> hov 1 (surround_impl b p)
+ | Generalized (b, b', t) ->
+ hov 1 (surround_impl b' (surround_impl b p))
+
let surround_implicit k p =
match k with
- Default Explicit -> p
- | Default Implicit -> (str"{" ++ p ++ str"}")
- | TypeClass _ -> (str"[" ++ p ++ str"]")
+ | Default Explicit -> p
+ | Default Implicit -> (str"{" ++ p ++ str"}")
+ | Generalized (b, b', t) ->
+ surround_impl b' (surround_impl b p)
let pr_binder many pr (nal,k,t) =
match t with
@@ -542,6 +552,17 @@ let rec pr sep inherited a =
else
p, lproj
| CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
+ | CRecord (_,w,l) ->
+ let beg =
+ match w with
+ | None -> spc ()
+ | Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
+ in
+ hv 0 (str"{" ++ beg ++
+ prlist_with_sep (fun () -> spc () ++ str";" ++ spc ())
+ (fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c)
+ l), latom
+
| CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
hv 0 (
str "let '" ++
@@ -592,9 +613,10 @@ let rec pr sep inherited a =
| CCast (_,a,CastCoerce) ->
hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
lcast
- | CNotation (_,"( _ )",[t]) ->
+ | CNotation (_,"( _ )",([t],[])) ->
pr (fun()->str"(") (max_int,L) t ++ str")", latom
| CNotation (_,s,env) -> pr_notation (pr mt) s env
+ | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
| CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
| CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
| CDynamic _ -> str "<dynamic>", latom
@@ -644,15 +666,15 @@ let rec strip_context n iscast t =
type term_pr = {
pr_constr_expr : constr_expr -> std_ppcmds;
pr_lconstr_expr : constr_expr -> std_ppcmds;
- pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds;
- pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+ pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
}
let default_term_pr = {
pr_constr_expr = pr lsimple;
pr_lconstr_expr = pr ltop;
- pr_pattern_expr = pr lsimple;
- pr_lpattern_expr = pr ltop
+ pr_constr_pattern_expr = pr lsimple;
+ pr_lconstr_pattern_expr = pr ltop
}
let term_pr = ref default_term_pr
@@ -661,8 +683,8 @@ let set_term_pr = (:=) term_pr
let pr_constr_expr c = !term_pr.pr_constr_expr c
let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c
-let pr_pattern_expr c = !term_pr.pr_pattern_expr c
-let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c
+let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c
+let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
let pr_cases_pattern_expr = pr_patt ltop
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 8047e968..0d0c8f56 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppconstr.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: ppconstr.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
open Pp
open Environ
@@ -66,8 +66,8 @@ val pr_may_eval :
val pr_rawsort : rawsort -> std_ppcmds
val pr_binders : local_binder list -> std_ppcmds
-val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
-val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
val pr_constr_expr : constr_expr -> std_ppcmds
val pr_lconstr_expr : constr_expr -> std_ppcmds
val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
@@ -75,8 +75,8 @@ val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
type term_pr = {
pr_constr_expr : constr_expr -> std_ppcmds;
pr_lconstr_expr : constr_expr -> std_ppcmds;
- pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds;
- pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+ pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
}
val set_term_pr : term_pr -> unit
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6a7ae9bc..3b433498 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Names
@@ -21,6 +21,7 @@ open Pattern
open Ppextend
open Ppconstr
open Printer
+open Termops
let pr_global x = Nametab.pr_global_env Idset.empty x
@@ -79,7 +80,7 @@ let pr_and_short_name pr (c,_) = pr c
let pr_or_by_notation f = function
| AN v -> f v
- | ByNotation (_,s) -> str s
+ | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_located pr (loc,x) = pr x
@@ -122,10 +123,6 @@ let pr_with_constr prc = function
| None -> mt ()
| Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
-let pr_with_names = function
- | None -> mt ()
- | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
-
let rec pr_message_token prid = function
| MsgString s -> qs s
| MsgInt n -> int n
@@ -140,6 +137,8 @@ let out_bindings = function
| ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l)
| NoBindings -> NoBindings
+let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
+
let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
| BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
@@ -148,7 +147,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
| StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
| PreIdentArgType -> str (out_gen rawwit_pre_ident x)
| IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
- | IdentArgType -> pr_id (out_gen rawwit_ident x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x)
| VarArgType -> pr_located pr_id (out_gen rawwit_var x)
| RefArgType -> prref (out_gen rawwit_ref x)
| SortArgType -> pr_rawsort (out_gen rawwit_sort x)
@@ -179,7 +178,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
x)
| ExtraArgType s ->
try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> str " [no printer for " ++ str s ++ str "] "
+ with Not_found -> str "[no printer for " ++ str s ++ str "]"
let rec pr_glob_generic prc prlc prtac x =
@@ -190,7 +189,7 @@ let rec pr_glob_generic prc prlc prtac x =
| StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
| PreIdentArgType -> str (out_gen globwit_pre_ident x)
| IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
- | IdentArgType -> pr_id (out_gen globwit_ident x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x)
| VarArgType -> pr_located pr_id (out_gen globwit_var x)
| RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
| SortArgType -> pr_rawsort (out_gen globwit_sort x)
@@ -224,7 +223,7 @@ let rec pr_glob_generic prc prlc prtac x =
x)
| ExtraArgType s ->
try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> str "[no printer for " ++ str s ++ str "] "
+ with Not_found -> str "[no printer for " ++ str s ++ str "]"
open Closure
@@ -236,7 +235,7 @@ let rec pr_generic prc prlc prtac x =
| StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
| PreIdentArgType -> str (out_gen wit_pre_ident x)
| IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
- | IdentArgType -> pr_id (out_gen wit_ident x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen wit_ident x)
| VarArgType -> pr_id (out_gen wit_var x)
| RefArgType -> pr_global (out_gen wit_ref x)
| SortArgType -> pr_sort (out_gen wit_sort x)
@@ -326,9 +325,6 @@ let pr_evaluable_reference_env env = function
| EvalConstRef sp ->
Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp)
-let pr_inductive env ind =
- Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind)
-
let pr_quantified_hypothesis = function
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
@@ -376,9 +372,9 @@ let pr_with_inversion_names = function
| None -> mt ()
| Some ipat -> pr_as_intro_pattern ipat
-let pr_with_names = function
- | _,IntroAnonymous -> mt ()
- | ipat -> pr_as_intro_pattern ipat
+let pr_as_ipat = function
+ | None -> mt ()
+ | Some ipat -> pr_as_intro_pattern ipat
let pr_as_name = function
| Anonymous -> mt ()
@@ -397,7 +393,7 @@ let pr_assertion _prlc prc ipat c = match ipat with
spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
*)
| ipat ->
- spc() ++ prc c ++ pr_with_names ipat
+ spc() ++ prc c ++ pr_as_ipat ipat
let pr_assumption prlc prc ipat c = match ipat with
(* Use this "optimisation" or use only the general case ?
@@ -405,7 +401,7 @@ let pr_assumption prlc prc ipat c = match ipat with
spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
*)
| ipat ->
- spc() ++ prc c ++ pr_with_names ipat
+ spc() ++ prc c ++ pr_as_ipat ipat
let pr_by_tactic prt = function
| TacId [] -> mt ()
@@ -426,6 +422,10 @@ let pr_simple_clause pr_id = function
| [] -> mt ()
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+let pr_in_hyp_as pr_id = function
+ | None -> mt ()
+ | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat
+
let pr_clauses pr_id = function
| { onhyps=None; concl_occs=occs } ->
if occs = no_occurrences_expr then pr_in (str " * |-")
@@ -468,12 +468,16 @@ let pr_lazy lz = if lz then str "lazy" else mt ()
let pr_match_pattern pr_pat = function
| Term a -> pr_pat a
- | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
- | Subterm (Some id,a) ->
- str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+ | Subterm (b,None,a) -> (if b then str"appcontext [" else str "context [") ++ pr_pat a ++ str "]"
+ | Subterm (b,Some id,a) ->
+ (if b then str"appcontext " else str "context ") ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-let pr_match_hyps pr_pat (Hyp (nal,mp)) =
- pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+let pr_match_hyps pr_pat = function
+ | Hyp (nal,mp) ->
+ pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+ | Def (nal,mv,mp) ->
+ pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
+ ++ str ":" ++ pr_match_pattern pr_pat mp
let pr_match_rule m pr pr_pat = function
| Pat ([],mp,t) when m ->
@@ -695,10 +699,11 @@ and pr_atom1 = function
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
| TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
| TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
- | TacApply (a,ev,cb) ->
+ | TacApply (a,ev,cb,inhyp) ->
hov 1 ((if a then mt() else str "simple ") ++
str (with_evars ev "apply") ++ spc () ++
- prlist_with_sep pr_coma pr_with_bindings cb)
+ prlist_with_sep pr_coma pr_with_bindings cb ++
+ pr_in_hyp_as pr_ident inhyp)
| TacElim (ev,cb,cbo) ->
hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
pr_opt pr_eliminator cbo)
@@ -1019,7 +1024,7 @@ let rec raw_printers =
(pr_raw_tactic_level,
drop_env pr_constr_expr,
drop_env pr_lconstr_expr,
- pr_lpattern_expr,
+ pr_lconstr_pattern_expr,
drop_env (pr_or_by_notation pr_reference),
drop_env (pr_or_by_notation pr_reference),
pr_reference,
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 67cd6f72..78c63ca2 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: ppvernac.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
open Pp
open Names
@@ -133,9 +133,11 @@ let pr_in_out_modules = function
| SearchOutside [] -> mt()
| SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l
-let pr_search_about = function
- | SearchRef r -> pr_reference r
- | SearchString s -> qs s
+let pr_search_about (b,c) =
+ (if b then str "-" else mt()) ++
+ match c with
+ | SearchSubPattern p -> pr_constr_pattern_expr p
+ | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a b pr_p = match a with
| SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b
@@ -144,7 +146,7 @@ let pr_search a b pr_p = match a with
| SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
let pr_locality local = if local then str "Local " else str ""
-let pr_non_globality local = if local then str "" else str "Global "
+let pr_non_locality local = if local then str "" else str "Global "
let pr_explanation (e,b,f) =
let a = match e with
@@ -192,18 +194,22 @@ let pr_hints local db h pr_c pr_pat =
match h with
| HintsResolve l ->
str "Resolve " ++ prlist_with_sep sep
- (fun (pri, c) -> pr_c c ++
+ (fun (pri, _, c) -> pr_c c ++
match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
l
| HintsImmediate l ->
str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
| HintsUnfold l ->
str "Unfold " ++ prlist_with_sep sep pr_reference l
+ | HintsTransparency (l, b) ->
+ str (if b then "Transparent " else "Opaque ") ++ prlist_with_sep sep
+ pr_reference l
| HintsConstructors c ->
str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
- | HintsExtern (n,c,tac) ->
- str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++
- spc() ++ pr_raw_tactic tac
+ | HintsExtern (n,c,tac) ->
+ let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+ str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
+ spc() ++ pr_raw_tactic tac
| HintsDestruct(name,i,loc,c,tac) ->
str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++
hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++
@@ -325,7 +331,7 @@ let pr_assumption_token many = function
str (if many then "Parameters" else "Parameter")
| (Global,Conjectural) -> str"Conjecture"
| (Local,Conjectural) ->
- anomaly "Don't know how to translate a local conjecture"
+ anomaly "Don't know how to beautify a local conjecture"
let pr_params pr_c (xl,(c,t)) =
hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -402,9 +408,27 @@ let make_pr_vernac pr_constr pr_lconstr =
let pr_constrarg c = spc () ++ pr_constr c in
let pr_lconstrarg c = spc () ++ pr_lconstr c in
let pr_intarg n = spc () ++ int n in
-let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
-let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l
- ++ sep ++ pr_constrarg c in
+(* let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in *)
+let pr_record_field (x, ntn) =
+ let prx = match x with
+ | (oc,AssumExpr (id,t)) ->
+ hov 1 (pr_lname id ++
+ (if oc then str" :>" else str" :") ++ spc() ++
+ pr_lconstr_expr t)
+ | (oc,DefExpr(id,b,opt)) -> (match opt with
+ | Some t ->
+ hov 1 (pr_lname id ++
+ (if oc then str" :>" else str" :") ++ spc() ++
+ pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+ | None ->
+ hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+ pr_lconstr b)) in
+ prx ++ pr_decl_notation pr_constr ntn
+in
+let pr_record_decl b c fs =
+ pr_opt pr_lident c ++ str"{" ++
+ hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+in
let rec pr_vernac = function
@@ -480,7 +504,7 @@ let rec pr_vernac = function
| VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
| None -> str"_"
| Some sc -> str sc in
- str"Arguments Scope" ++ spc() ++ pr_non_globality local ++ pr_reference q
+ str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ pr_reference q
++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
| VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
hov 0 (hov 0 (str"Infix " ++ pr_locality local
@@ -533,11 +557,11 @@ let rec pr_vernac = function
| VernacStartTheoremProof (ki,l,_,_) ->
let pr_statement head (id,(bl,c)) =
hov 0
- (head ++ spc () ++ pr_opt pr_lident id ++ spc() ++
+ (head ++ pr_opt pr_lident id ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
str":" ++ pr_spc_lconstr c) in
hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
- prlist (pr_statement (str "with ")) (List.tl l))
+ prlist (pr_statement (spc () ++ str "with")) (List.tl l))
| VernacEndProof Admitted -> str"Admitted"
| VernacEndProof (Proved (opac,o)) -> (match o with
@@ -558,22 +582,31 @@ let rec pr_vernac = function
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
pr_spc_lconstr c) in
- let pr_constructor_list l = match l with
- | [] -> mt()
- | _ ->
+ let pr_constructor_list b l = match l with
+ | Constructors [] -> mt()
+ | Constructors l ->
pr_com_at (begin_of_inductive l) ++
fnl() ++
str (if List.length l = 1 then " " else " | ") ++
- prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
- let pr_oneind key ((id,indpar,s,lc),ntn) =
- hov 0 (
- str key ++ spc() ++
- pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++
- spc() ++ pr_lconstr_expr s ++
- str" :=") ++ pr_constructor_list lc ++
- pr_decl_notation pr_constr ntn in
-
- hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
+ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
+ | RecordDecl (c,fs) ->
+ spc() ++
+ pr_record_decl b c fs in
+ let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+ let kw =
+ str (match k with Record -> "Record" | Structure -> "Structure"
+ | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+ | Class b -> if b then "Definitional Class" else "Class")
+ in
+ hov 0 (
+ kw ++ spc() ++
+ (if coe then str" > " else str" ") ++ pr_lident id ++
+ pr_and_type_binders_arg indpar ++ spc() ++
+ Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+ str" :=") ++ pr_constructor_list k lc ++
+ pr_decl_notation pr_constr ntn
+ in
+ hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
++
(prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
@@ -585,7 +618,7 @@ let rec pr_vernac = function
let pr_onerec = function
| ((loc,id),(n,ro),bl,type_,def),ntn ->
let (bl',def,type_) =
- if Flags.do_translate() then extract_def_binders def type_
+ if Flags.do_beautify() then extract_def_binders def type_
else ([],def,type_) in
let bl = bl @ bl' in
let ids = List.flatten (List.map name_of_binder bl) in
@@ -617,7 +650,7 @@ let rec pr_vernac = function
| VernacCoFixpoint (corecs,b) ->
let pr_onecorec (((loc,id),bl,c,def),ntn) =
let (bl',def,c) =
- if Flags.do_translate() then extract_def_binders def c
+ if Flags.do_beautify() then extract_def_binders def c
else ([],def,c) in
let bl = bl @ bl' in
pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -638,30 +671,6 @@ let rec pr_vernac = function
(* Gallina extensions *)
- | VernacRecord (b,(oc,name),ps,s,c,fs) ->
- let pr_record_field = function
- | (oc,AssumExpr (id,t)) ->
- hov 1 (pr_lname id ++
- (if oc then str" :>" else str" :") ++ spc() ++
- pr_lconstr_expr t)
- | (oc,DefExpr(id,b,opt)) -> (match opt with
- | Some t ->
- hov 1 (pr_lname id ++
- (if oc then str" :>" else str" :") ++ spc() ++
- pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
- | None ->
- hov 1 (pr_lname id ++ str" :=" ++ spc() ++
- pr_lconstr b)) in
- hov 2
- (str (if b then "Record" else "Structure") ++
- (if oc then str" > " else str" ") ++ pr_lident name ++
- pr_and_type_binders_arg ps ++ str" :" ++ spc() ++
- pr_lconstr_expr s ++ str" := " ++
- (match c with
- | None -> mt()
- | Some sc -> pr_lident sc) ++
- spc() ++ str"{" ++
- hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
| VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
| VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
| VernacRequire (exp,spe,l) -> hov 2
@@ -688,28 +697,17 @@ let rec pr_vernac = function
str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++
spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
spc() ++ pr_class_rawexpr c2)
-
-
- | VernacClass (id, par, ar, sup, props) ->
- hov 1 (
- str"Class" ++ spc () ++ pr_lident id ++
-(* prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ *)
- pr_and_type_binders_arg par ++
- (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++
- spc () ++ str"where" ++ spc () ++
- prlist_with_sep (fun () -> str";" ++ spc())
- (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
| VernacInstance (glob, sup, (instid, bk, cl), props, pri) ->
hov 1 (
- pr_non_globality (not glob) ++
+ pr_non_locality (not glob) ++
str"Instance" ++ spc () ++
pr_and_type_binders_arg sup ++
str"=>" ++ spc () ++
(match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
pr_constr_expr cl ++ spc () ++
- spc () ++ str"where" ++ spc () ++
- prlist_with_sep (fun () -> str";" ++ spc()) (pr_instance_def (spc () ++ str":=" ++ spc())) props)
+ spc () ++ str":=" ++ spc () ++
+ pr_constr_expr props)
| VernacContext l ->
hov 1 (
@@ -806,8 +804,10 @@ let rec pr_vernac = function
hov 1
((str "Ltac ") ++
prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
+ | VernacCreateHintDb (local,dbname,b) ->
+ hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
| VernacHints (local,dbnames,h) ->
- pr_hints local dbnames h pr_constr pr_pattern_expr
+ pr_hints local dbnames h pr_constr pr_constr_pattern_expr
| VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
hov 2
(str"Notation " ++ pr_locality local ++ pr_lident id ++
@@ -816,7 +816,7 @@ let rec pr_vernac = function
| VernacDeclareImplicits (local,q,None) ->
hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
| VernacDeclareImplicits (local,q,Some imps) ->
- hov 1 (str"Implicit Arguments " ++ pr_non_globality local ++
+ hov 1 (str"Implicit Arguments " ++ pr_non_locality local ++
spc() ++ pr_reference q ++ spc() ++
str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
| VernacReserve (idl,c) ->
@@ -824,11 +824,11 @@ let rec pr_vernac = function
str (if List.length idl > 1 then "s " else " ") ++
prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++
pr_lconstr c)
- | VernacSetOpacity(true,[k,l]) when k=Conv_oracle.transparent ->
- hov 1 (str"Transparent" ++
+ | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
+ hov 1 (str"Transparent" ++ pr_non_locality b ++
spc() ++ prlist_with_sep sep pr_reference l)
- | VernacSetOpacity(true,[Conv_oracle.Opaque,l]) ->
- hov 1 (str"Opaque" ++
+ | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
+ hov 1 (str"Opaque" ++ pr_non_locality b ++
spc() ++ prlist_with_sep sep pr_reference l)
| VernacSetOpacity (local,l) ->
let pr_lev = function
@@ -866,7 +866,7 @@ let rec pr_vernac = function
str"Print Section" ++ spc() ++ Libnames.pr_reference s
| PrintGrammar ent ->
str"Print Grammar" ++ spc() ++ str ent
- | PrintLoadPath -> str"Print LoadPath"
+ | PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir
| PrintModules -> str"Print Modules"
| PrintMLLoadPath -> str"Print ML Path"
| PrintMLModules -> str"Print ML Modules"
@@ -890,7 +890,6 @@ let rec pr_vernac = function
| PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid
| PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid
| PrintInspect n -> str"Inspect" ++ spc() ++ int n
- | PrintSetoids -> str"Print Setoids"
| PrintScopes -> str"Print Scopes"
| PrintScope s -> str"Print Scope" ++ spc() ++ str s
| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s
@@ -900,7 +899,7 @@ let rec pr_vernac = function
term *)
| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
in pr_printable p
- | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr
+ | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
| VernacLocate loc ->
let pr_locate =function
| LocateTerm qid -> pr_reference qid
@@ -931,19 +930,16 @@ and pr_extend s cl =
let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
let start,rl,cl =
match rl with
- | Egrammar.TacTerm s :: rl -> str s, rl, cl
- | Egrammar.TacNonTerm _ :: rl ->
- (* Will put an unnecessary extra space in front *)
- pr_gen (Global.env()) (List.hd cl), rl, List.tl cl
- | [] -> anomaly "Empty entry" in
+ | Egrammar.TacTerm s :: rl -> str s, rl, cl
+ | Egrammar.TacNonTerm _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
+ | [] -> anomaly "Empty entry" in
let (pp,_) =
List.fold_left
(fun (strm,args) pi ->
- match pi with
- Egrammar.TacNonTerm _ ->
- (strm ++ pr_gen (Global.env()) (List.hd args),
- List.tl args)
- | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
+ let pp,args = match pi with
+ | Egrammar.TacNonTerm _ -> (pr_arg (List.hd args), List.tl args)
+ | Egrammar.TacTerm s -> (str s, args) in
+ (strm ++ spc() ++ pp), args)
(start,cl) rl in
hov 1 pp
with Not_found ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4811c443..5543a31c 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
* on May-June 2006 for implementation of abstraction of pretty-printing of objects.
*)
-(* $Id: prettyp.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
+(* $Id: prettyp.ml 11622 2008-11-23 08:45:56Z herbelin $ *)
open Pp
open Util
@@ -349,10 +349,10 @@ let pr_record (sp,tyi) =
str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
str ":= " ++ pr_id cstrnames.(0)) ++
brk(1,2) ++
- hv 2 (str "{ " ++
- prlist_with_sep (fun () -> str "; " ++ brk(1,0))
+ hv 2 (str "{" ++
+ prlist_with_sep (fun () -> str ";" ++ brk(1,0))
(fun (id,b,c) ->
- pr_id id ++ str (if b then " : " else " := ") ++
+ str " " ++ pr_id id ++ str (if b then " : " else " := ") ++
pr_lconstr_env envpar c) fields) ++ str" }")
let gallina_print_inductive sp =
@@ -784,6 +784,11 @@ let pr_instance env i =
(* lighter *)
print_ref false (ConstRef (instance_impl i))
+let print_all_instances () =
+ let env = Global.env () in
+ let inst = all_instances () in
+ prlist_with_sep fnl (pr_instance env) inst
+
let print_instances r =
let env = Global.env () in
let inst = instances r in
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index a487ef62..ec2228c7 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: prettyp.mli 10697 2008-03-19 17:58:43Z msozeau $ i*)
+(*i $Id: prettyp.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Pp
@@ -61,7 +61,7 @@ val print_canonical_projections : unit -> std_ppcmds
(* Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> std_ppcmds
val print_instances : global_reference -> std_ppcmds
-
+val print_all_instances : unit -> std_ppcmds
val inspect : int -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index b126cc9c..10034dd9 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: printer.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
open Pp
open Util
@@ -90,14 +90,14 @@ let pr_cases_pattern t =
pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
let pr_lconstr_pattern_env env c =
- pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c)
+ pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
let pr_constr_pattern_env env c =
- pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c)
+ pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
let pr_lconstr_pattern t =
- pr_lconstr_expr (extern_constr_pattern empty_names_context t)
+ pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t)
let pr_constr_pattern t =
- pr_constr_expr (extern_constr_pattern empty_names_context t)
+ pr_constr_pattern_expr (extern_constr_pattern empty_names_context t)
let pr_sort s = pr_rawsort (extern_sort s)
@@ -162,9 +162,9 @@ let pr_rel_decl env (na,c,typ) =
(* Prints a signature, all declarations on the same line if possible *)
let pr_named_context_of env =
- hv 0 (fold_named_context
- (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
- env ~init:(mt ()))
+ let make_decl_list env d pps = pr_var_decl env d :: pps in
+ let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
+ hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
let pr_named_context env ne_context =
hv 0 (Sign.fold_named_context
@@ -475,6 +475,9 @@ let pr_prim_rule = function
(str (if withdep then "dependent " else "") ++
str"move " ++ pr_id id1 ++ pr_move_location pr_id id2)
+ | Order ord ->
+ (str"order " ++ prlist_with_sep pr_spc pr_id ord)
+
| Rename (id1,id2) ->
(str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index be73f573..596ce6b2 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -90,7 +90,7 @@ and print_modtype locals mty =
let s = (String.concat "." (List.map string_of_id idl)) in
hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
- | SEBwith(seb,With_module_body(idl,mp,_))->
+ | SEBwith(seb,With_module_body(idl,mp,_,_))->
let s =(String.concat "." (List.map string_of_id idl)) in
hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
@@ -102,7 +102,7 @@ and print_sig locals msid sign =
| SFBconst {const_opaque=true} -> str "Parameter "
| SFBmind _ -> str "Inductive "
| SFBmodule _ -> str "Module "
- | SFBalias (mp,_) -> str "Module "
+ | SFBalias (mp,_,_) -> str "Module "
| SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
in
prlist_with_sep spc print_spec sign
@@ -114,7 +114,7 @@ and print_struct locals msid struc =
| SFBconst {const_body=None} -> str "Parameter "
| SFBmind _ -> str "Inductive "
| SFBmodule _ -> str "Module "
- | SFBalias (mp,_) -> str "Module "
+ | SFBalias (mp,_,_) -> str "Module "
| SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
in
prlist_with_sep spc print_body struc
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 72d81051..37817389 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: q_constr.ml4 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: q_constr.ml4 11576 2008-11-10 19:13:15Z msozeau $ *)
open Rawterm
open Term
@@ -75,7 +75,7 @@ EXTEND
| "0"
[ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
| id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
- | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >>
+ | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >>
| "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
| "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a4cfe27a..aeee632c 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
-(* $Id: q_coqast.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: q_coqast.ml4 11735 2009-01-02 17:22:31Z herbelin $ *)
open Util
open Names
@@ -68,7 +68,8 @@ 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) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
+ | Genarg.ByNotation (loc,s,sco) ->
+ <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
let mlexpr_of_intro_pattern = function
| Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
@@ -102,12 +103,12 @@ let mlexpr_of_occs =
let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
let mlexpr_of_hyp_location = function
- | occs, Tacexpr.InHyp ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >>
- | occs, Tacexpr.InHypTypeOnly ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >>
- | occs, Tacexpr.InHypValueOnly ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >>
+ | 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) >>
let mlexpr_of_clause cl =
<:expr< {Tacexpr.onhyps=
@@ -139,7 +140,9 @@ let mlexpr_of_binding_kind = function
let mlexpr_of_binder_kind = function
| Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
- | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >>
+ | Topconstr.Generalized (b,b',b'') ->
+ <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$
+ $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
let rec mlexpr_of_constr = function
| Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
@@ -158,9 +161,11 @@ let rec mlexpr_of_constr = function
| Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
| Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
| Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
- | Topconstr.CNotation(_,ntn,l) ->
+ | Topconstr.CNotation(_,ntn,subst) ->
<:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
- $mlexpr_of_list mlexpr_of_constr l$ >>
+ $mlexpr_of_pair
+ (mlexpr_of_list mlexpr_of_constr)
+ (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >>
| Topconstr.CPatVar (loc,n) ->
<:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
| _ -> failwith "mlexpr_of_constr: TODO"
@@ -196,7 +201,7 @@ let rec mlexpr_of_argtype loc = function
| Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
| Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
| Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
- | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
+ | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
| Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
@@ -264,13 +269,16 @@ let mlexpr_of_entry_type = function
let mlexpr_of_match_pattern = function
| Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >>
- | Tacexpr.Subterm (ido,t) ->
- <:expr< Tacexpr.Subterm $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
+ | Tacexpr.Subterm (b,ido,t) ->
+ <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
let mlexpr_of_match_context_hyps = function
| Tacexpr.Hyp (id,l) ->
let f = mlexpr_of_located mlexpr_of_name in
<:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >>
+ | Tacexpr.Def (id,v,l) ->
+ let f = mlexpr_of_located mlexpr_of_name in
+ <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >>
let mlexpr_of_match_rule f = function
| Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >>
@@ -300,8 +308,8 @@ let rec mlexpr_of_atomic_tactic = function
<:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
| Tacexpr.TacVmCastNoCheck c ->
<:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
- | Tacexpr.TacApply (b,false,cb) ->
- <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >>
+ | Tacexpr.TacApply (b,false,cb,None) ->
+ <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
| Tacexpr.TacElim (false,cb,cbo) ->
let cb = mlexpr_of_constr_with_binding cb in
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
@@ -337,7 +345,7 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacCut c ->
<:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
| Tacexpr.TacAssert (t,ipat,c) ->
- let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in
+ let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
<:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
$mlexpr_of_constr c$ >>
| Tacexpr.TacGeneralize cl ->
@@ -480,6 +488,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
| Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
| Tacexpr.TacArg t ->
<:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >>
+ | Tacexpr.TacComplete t ->
+ <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >>
| _ -> failwith "Quotation of tactic expressions: TODO"
and mlexpr_of_tactic_arg = function
diff --git a/parsing/search.ml b/parsing/search.ml
index c6ff4c04..8b1551b6 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: search.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: search.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
open Pp
open Util
@@ -165,15 +165,6 @@ let raw_search_rewrite extra_filter display_function pattern =
(pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c))
&& extra_filter s a c)
display_function gref_eq
-(*
- ;
- filtered_search
- (fun s a c ->
- ((pattern_filter (mk_rewrite_pattern1 gref_eqT pattern) s a c) ||
- (pattern_filter (mk_rewrite_pattern2 gref_eqT pattern) s a c))
- && extra_filter s a c)
- display_function gref_eqT
-*)
let text_pattern_search extra_filter =
raw_pattern_search extra_filter plain_display
@@ -204,17 +195,17 @@ let gen_filtered_search filter_function display_function =
let name_of_reference ref = string_of_id (id_of_global ref)
type glob_search_about_item =
- | GlobSearchRef of global_reference
+ | GlobSearchSubPattern of constr_pattern
| GlobSearchString of string
let search_about_item (itemref,typ) = function
- | GlobSearchRef ref -> Termops.occur_term (constr_of_global ref) typ
+ | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
| GlobSearchString s -> string_string_contains (name_of_reference itemref) s
let raw_search_about filter_modules display_function l =
let filter ref' env typ =
filter_modules ref' env typ &&
- List.for_all (search_about_item (ref',typ)) l &&
+ List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l &&
not (string_string_contains (name_of_reference ref') "_subproof")
in
gen_filtered_search filter display_function
diff --git a/parsing/search.mli b/parsing/search.mli
index 8ee708bc..7d12d26f 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: search.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: search.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
open Pp
open Names
@@ -19,13 +19,14 @@ open Nametab
(*s Search facilities. *)
type glob_search_about_item =
- | GlobSearchRef of global_reference
+ | GlobSearchSubPattern of constr_pattern
| GlobSearchString of string
val search_by_head : global_reference -> dir_path list * bool -> unit
val search_rewrite : constr_pattern -> dir_path list * bool -> unit
val search_pattern : constr_pattern -> dir_path list * bool -> unit
-val search_about : glob_search_about_item list -> dir_path list * bool -> unit
+val search_about :
+ (bool * glob_search_about_item) list -> dir_path list * bool -> unit
(* The filtering function that is by standard search facilities.
It can be passed as argument to the raw search functions.
@@ -46,4 +47,4 @@ val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
(global_reference -> env -> constr -> unit) -> constr_pattern -> unit
val raw_search_about : (global_reference -> env -> constr -> bool) ->
(global_reference -> env -> constr -> unit) ->
- glob_search_about_item list -> unit
+ (bool * glob_search_about_item) list -> unit
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 08feb17a..a7b27e21 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: vernacextend.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: vernacextend.ml4 11622 2008-11-23 08:45:56Z herbelin $ *)
open Util
open Genarg
@@ -118,6 +118,9 @@ EXTEND
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let t, g = Q_util.interp_entry_name loc e "" in
VernacNonTerm (loc, t, g, Some s)
+ | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+ let t, g = Q_util.interp_entry_name loc e sep in
+ VernacNonTerm (loc, t, g, Some s)
| s = STRING ->
VernacTerm s
] ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 07:57:57 +0000