aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egrammar.ml5
-rw-r--r--parsing/egrammar.mli2
-rw-r--r--parsing/g_decl_mode.ml4252
-rw-r--r--parsing/g_proofs.ml44
-rw-r--r--parsing/g_vernac.ml455
-rw-r--r--parsing/grammar.mllib1
-rw-r--r--parsing/highparsing.mllib1
-rw-r--r--parsing/parsing.mllib1
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--parsing/ppdecl_proof.ml190
-rw-r--r--parsing/ppdecl_proof.mli2
-rw-r--r--parsing/ppvernac.ml13
-rw-r--r--parsing/printer.ml79
-rw-r--r--parsing/printer.mli8
-rw-r--r--parsing/tactic_printer.ml89
-rw-r--r--parsing/tactic_printer.mli1
-rw-r--r--parsing/vernacextend.ml420
18 files changed, 120 insertions, 606 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 023ec0f3c..b5ee1ae60 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -222,12 +222,13 @@ let extend_tactic_grammar s gl =
let vernac_exts = ref []
let get_extend_vernac_grammars () = !vernac_exts
-let extend_vernac_command_grammar s gl =
+let extend_vernac_command_grammar s nt gl =
+ let nt = Option.default Vernac_.command nt in
vernac_exts := (s,gl) :: !vernac_exts;
let univ = get_univ "vernac" in
let mkact loc l = VernacExtend (s,List.map snd l) in
let rules = List.map (make_rule univ mkact make_prod_item) gl in
- Gram.extend Vernac_.command None [(None, None, List.rev rules)]
+ Gram.extend nt None [(None, None, List.rev rules)]
(**********************************************************************)
(** Grammar declaration for Tactic Notation (Coq level) *)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 1228b40cf..a45ea9549 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -59,7 +59,7 @@ val extend_tactic_grammar :
string -> grammar_prod_item list list -> unit
val extend_vernac_command_grammar :
- string -> grammar_prod_item list list -> unit
+ string -> vernac_expr Gram.Entry.e option -> grammar_prod_item list list -> unit
val get_extend_vernac_grammars :
unit -> (string * grammar_prod_item list list) list
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
deleted file mode 100644
index e73e54e7f..000000000
--- a/parsing/g_decl_mode.ml4
+++ /dev/null
@@ -1,252 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
-(* $Id$ *)
-
-
-open Decl_expr
-open Names
-open Term
-open Genarg
-open Pcoq
-
-open Pcoq.Constr
-open Pcoq.Tactic
-open Pcoq.Vernac_
-
-let none_is_empty = function
- None -> []
- | Some l -> l
-
-GEXTEND Gram
-GLOBAL: proof_instr;
- thesis :
- [[ "thesis" -> Plain
- | "thesis"; "for"; i=ident -> (For i)
- ]];
- statement :
- [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
- | i=ident -> {st_label=Anonymous;
- st_it=Topconstr.CRef (Libnames.Ident (loc, i))}
- | c=constr -> {st_label=Anonymous;st_it=c}
- ]];
- constr_or_thesis :
- [[ t=thesis -> Thesis t ] |
- [ c=constr -> This c
- ]];
- statement_or_thesis :
- [
- [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ]
- |
- [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
- | i=ident -> {st_label=Anonymous;
- st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))}
- | c=constr -> {st_label=Anonymous;st_it=This c}
- ]
- ];
- justification_items :
- [[ -> Some []
- | "by"; l=LIST1 constr SEP "," -> Some l
- | "by"; "*" -> None ]]
- ;
- justification_method :
- [[ -> None
- | "using"; tac = tactic -> Some tac ]]
- ;
- simple_cut_or_thesis :
- [[ ls = statement_or_thesis;
- j = justification_items;
- taco = justification_method
- -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
- ;
- simple_cut :
- [[ ls = statement;
- j = justification_items;
- taco = justification_method
- -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
- ;
- elim_type:
- [[ IDENT "induction" -> ET_Induction
- | IDENT "cases" -> ET_Case_analysis ]]
- ;
- block_type :
- [[ IDENT "claim" -> B_claim
- | IDENT "focus" -> B_focus
- | IDENT "proof" -> B_proof
- | et=elim_type -> B_elim et ]]
- ;
- elim_obj:
- [[ IDENT "on"; c=constr -> Real c
- | IDENT "of"; c=simple_cut -> Virtual c ]]
- ;
- elim_step:
- [[ IDENT "consider" ;
- h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
- | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)
- | IDENT "suffices"; ls=suff_clause;
- j = justification_items;
- taco = justification_method
- -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]]
- ;
- rew_step :
- [[ "~=" ; c=simple_cut -> (Rhs,c)
- | "=~" ; c=simple_cut -> (Lhs,c)]]
- ;
- cut_step:
- [[ "then"; tt=elim_step -> Pthen tt
- | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c)
- | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c))
- | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c)
- | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c)
- | tt=elim_step -> tt
- | tt=rew_step -> let s,c=tt in Prew (s,c);
- | IDENT "have"; c=simple_cut_or_thesis -> Pcut c;
- | IDENT "claim"; c=statement -> Pclaim c;
- | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c;
- | "end"; bt = block_type -> Pend bt;
- | IDENT "escape" -> Pescape ]]
- ;
- (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*)
- loc_id:
- [[ id=ident -> fun x -> (loc,(id,x)) ]];
- hyp:
- [[ id=loc_id -> id None ;
- | id=loc_id ; ":" ; c=constr -> id (Some c)]]
- ;
- consider_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=consider_vars -> (Hvar name) :: v
- | name=hyp;
- IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h
- ]]
- ;
- consider_hyps:
- [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h
- | st=statement; IDENT "and";
- IDENT "consider" ; v=consider_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]]
- ;
- assume_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=assume_vars -> (Hvar name) :: v
- | name=hyp;
- IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h
- ]]
- ;
- assume_hyps:
- [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h
- | st=statement; IDENT "and";
- IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]]
- ;
- assume_clause:
- [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v
- | h=assume_hyps -> h ]]
- ;
- suff_vars:
- [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
- [Hvar name],c
- | name=hyp; ","; v=suff_vars ->
- let (q,c) = v in ((Hvar name) :: q),c
- | name=hyp;
- IDENT "such"; IDENT "that"; h=suff_hyps ->
- let (q,c) = h in ((Hvar name) :: q),c
- ]];
- suff_hyps:
- [[ st=statement; IDENT "and"; h=suff_hyps ->
- let (q,c) = h in (Hprop st::q),c
- | st=statement; IDENT "and";
- IDENT "to" ; IDENT "have" ; v=suff_vars ->
- let (q,c) = v in (Hprop st::q),c
- | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
- [Hprop st],c
- ]]
- ;
- suff_clause:
- [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v
- | h=suff_hyps -> h ]]
- ;
- let_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=let_vars -> (Hvar name) :: v
- | name=hyp; IDENT "be";
- IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h
- ]]
- ;
- let_hyps:
- [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h
- | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]];
- given_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=given_vars -> (Hvar name) :: v
- | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h
- ]]
- ;
- given_hyps:
- [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h
- | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]];
- suppose_vars:
- [[name=hyp -> [Hvar name]
- |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v
- |name=hyp; OPT[IDENT "be"];
- IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h
- ]]
- ;
- suppose_hyps:
- [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h
- | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have";
- v=suppose_vars -> Hprop st::v
- | st=statement_or_thesis -> [Hprop st]
- ]]
- ;
- suppose_clause:
- [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v;
- | h=suppose_hyps -> h ]]
- ;
- intro_step:
- [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
- | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
- po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ;
- ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] ->
- Pcase (none_is_empty po,c,none_is_empty ho)
- | "let" ; v=let_vars -> Plet v
- | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses
- | IDENT "assume"; h=assume_clause -> Passume h
- | IDENT "given"; h=given_vars -> Pgiven h
- | IDENT "define"; id=ident; args=LIST0 hyp;
- "as"; body=constr -> Pdefine(id,args,body)
- | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ)
- | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ)
- ]]
- ;
- emphasis :
- [[ -> 0
- | "*" -> 1
- | "**" -> 2
- | "***" -> 3
- ]]
- ;
- bare_proof_instr:
- [[ c = cut_step -> c ;
- | i = intro_step -> i ]]
- ;
- proof_instr :
- [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]]
- ;
-END;;
-
-
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 39e577b88..27ad1e964 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -40,6 +40,7 @@ GEXTEND Gram
[ [ IDENT "Goal"; c = lconstr -> VernacGoal c
| IDENT "Proof" -> VernacProof (Tacexpr.TacId [])
| IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
+ | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Abort" -> VernacAbort None
| IDENT "Abort"; IDENT "All" -> VernacAbortAll
| IDENT "Abort"; id = identref -> VernacAbort (Some id)
@@ -66,6 +67,9 @@ GEXTEND Gram
| IDENT "Focus" -> VernacFocus None
| IDENT "Focus"; n = natural -> VernacFocus (Some n)
| IDENT "Unfocus" -> VernacUnfocus
+ | IDENT "BeginSubproof" -> VernacSubproof None
+ | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n)
+ | IDENT "EndSubproof" -> VernacEndSubproof
| IDENT "Show" -> VernacShow (ShowGoal None)
| IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n))
| IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 008a6ac51..db683b9a9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -19,7 +19,6 @@ open Topconstr
open Extend
open Vernacexpr
open Pcoq
-open Decl_mode
open Tactic
open Decl_kinds
open Genarg
@@ -40,7 +39,6 @@ let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
let check_command = Gram.Entry.create "vernac:check_command"
let tactic_mode = Gram.Entry.create "vernac:tactic_command"
-let proof_mode = Gram.Entry.create "vernac:proof_command"
let noedit_mode = Gram.Entry.create "vernac:noedit_command"
let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
@@ -50,13 +48,23 @@ 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 subgoal_command = Gram.Entry.create "proof_mode:subgoal_command"
let instance_name = Gram.Entry.create "vernac:instance_name"
-let get_command_entry () =
- match Decl_mode.get_current_mode () with
- Mode_proof -> proof_mode
- | Mode_tactic -> tactic_mode
- | Mode_none -> noedit_mode
+let command_entry = ref noedit_mode
+let set_command_entry e = command_entry := e
+let get_command_entry () = !command_entry
+
+
+(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
+ proof editing and changes nothing else). Then sets it as the default proof mode. *)
+let set_tactic_mode () = set_command_entry tactic_mode
+let set_noedit_mode () = set_command_entry noedit_mode
+let _ = Proof_global.register_proof_mode {Proof_global.
+ name = "Classic" ;
+ set = set_tactic_mode ;
+ reset = set_noedit_mode
+ }
let default_command_entry =
Gram.Entry.of_parser "command_entry"
@@ -64,7 +72,7 @@ let default_command_entry =
let no_hook _ _ = ()
GEXTEND Gram
- GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
+ GLOBAL: vernac gallina_ext tactic_mode noedit_mode subgoal_command;
vernac: FIRST
[ [ IDENT "Time"; v = vernac -> VernacTime v
| IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
@@ -89,25 +97,25 @@ GEXTEND Gram
| -> locality_flag := None ] ]
;
noedit_mode:
- [ [ c = subgoal_command -> c None] ]
+ [ [ c = subgoal_command -> c None None] ]
;
tactic_mode:
[ [ gln = OPT[n=natural; ":" -> n];
- tac = subgoal_command -> tac gln ] ]
+ tac = subgoal_command -> tac gln None
+ | b = bullet; tac = subgoal_command -> tac None (Some b)] ]
+ ;
+ bullet:
+ [ [ "-" -> Dash
+ | "*" -> Star
+ | "+" -> Plus ] ]
;
- subgoal_command:
- [ [ c = check_command; "." -> c
+ subgoal_command:
+ [ [ c = check_command; "." -> fun g _ -> c g
| tac = Tactic.tactic;
use_dft_tac = [ "." -> false | "..." -> true ] ->
- (fun g ->
- let g = match g with Some gl -> gl | _ -> 1 in
- VernacSolve(g,tac,use_dft_tac)) ] ]
- ;
- proof_mode:
- [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ]
- ;
- proof_mode: LAST
- [ [ c=subgoal_command -> c (Some 1) ] ]
+ (fun g b ->
+ let g = Option.default 1 g in
+ VernacSolve(g,b,tac,use_dft_tac)) ] ]
;
located_vernac:
[ [ v = vernac -> loc, v ] ]
@@ -713,10 +721,7 @@ GEXTEND Gram
| IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
-> VernacRemoveOption ([table;field], v)
| IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
- VernacRemoveOption ([table], v)
-
- | IDENT "proof" -> VernacDeclProof
- | "return" -> VernacReturn ]]
+ VernacRemoveOption ([table], v) ]]
;
check_command: (* TODO: rapprocher Eval et Check *)
[ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 248a8ad9a..483538da6 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -14,6 +14,7 @@ Hashcons
Predicate
Rtree
Option
+Store
Names
Univ
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 3eb27abbb..eed6caea3 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -4,4 +4,3 @@ G_prim
G_proofs
G_tactic
G_ltac
-G_decl_mode
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index c0c1817d1..84a08d549 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -6,7 +6,6 @@ G_xml
Ppconstr
Printer
Pptactic
-Ppdecl_proof
Tactic_printer
Printmod
Prettyp
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 7120f72d2..de15d8a7c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -373,8 +373,6 @@ module Vernac_ =
let command = gec_vernac "command"
let syntax = gec_vernac "syntax_command"
let vernac = gec_vernac "Vernac.vernac"
- let proof_instr = Gram.Entry.create "proofmode:instr"
-
let vernac_eoi = eoi_entry vernac
(* Main vernac entry *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ed370a995..7ed05ed5c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -247,7 +247,6 @@ module Vernac_ :
val syntax : vernac_expr Gram.Entry.e
val vernac : vernac_expr Gram.Entry.e
val vernac_eoi : vernac_expr Gram.Entry.e
- val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e
end
(* The main entry: reads an optional vernac command *)
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
deleted file mode 100644
index 40c712cdf..000000000
--- a/parsing/ppdecl_proof.ml
+++ /dev/null
@@ -1,190 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Util
-open Pp
-open Decl_expr
-open Names
-open Nameops
-
-let pr_constr = Printer.pr_constr_env
-let pr_tac = Pptactic.pr_glob_tactic
-let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
-
-let pr_label = function
- Anonymous -> mt ()
- | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
-
-let pr_justification_items env = function
- Some [] -> mt ()
- | Some (_::_ as l) ->
- spc () ++ str "by" ++ spc () ++
- prlist_with_sep (fun () -> str ",") (pr_constr env) l
- | None -> spc () ++ str "by *"
-
-let pr_justification_method env = function
- None -> mt ()
- | Some tac ->
- spc () ++ str "using" ++ spc () ++ pr_tac env tac
-
-let pr_statement pr_it env st =
- pr_label st.st_label ++ pr_it env st.st_it
-
-let pr_or_thesis pr_this env = function
- Thesis Plain -> str "thesis"
- | Thesis (For id) ->
- str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
- | This c -> pr_this env c
-
-let pr_cut pr_it env c =
- hov 1 (pr_it env c.cut_stat) ++
- pr_justification_items env c.cut_by ++
- pr_justification_method env c.cut_using
-
-let type_or_thesis = function
- Thesis _ -> Term.mkProp
- | This c -> c
-
-let _I x = x
-
-let rec print_hyps pconstr gtyp env sep _be _have hyps =
- let pr_sep = if sep then str "and" ++ spc () else mt () in
- match hyps with
- (Hvar _ ::_) as rest ->
- spc () ++ pr_sep ++ str _have ++
- print_vars pconstr gtyp env false _be _have rest
- | Hprop st :: rest ->
- begin
- let nenv =
- match st.st_label with
- Anonymous -> env
- | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
- spc() ++ pr_sep ++ pr_statement pconstr env st ++
- print_hyps pconstr gtyp nenv true _be _have rest
- end
- | [] -> mt ()
-
-and print_vars pconstr gtyp env sep _be _have vars =
- match vars with
- Hvar st :: rest ->
- begin
- let nenv =
- match st.st_label with
- Anonymous -> anomaly "anonymous variable"
- | Name id -> Environ.push_named (id,None,st.st_it) env in
- let pr_sep = if sep then pr_coma () else mt () in
- spc() ++ pr_sep ++
- pr_statement pr_constr env st ++
- print_vars pconstr gtyp nenv true _be _have rest
- end
- | (Hprop _ :: _) as rest ->
- let _st = if _be then
- str "be such that"
- else
- str "such that" in
- spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest
- | [] -> mt ()
-
-let pr_suffices_clause env (hyps,c) =
- print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
- str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
-
-let pr_elim_type = function
- ET_Case_analysis -> str "cases"
- | ET_Induction -> str "induction"
-
-let pr_casee env =function
- Real c -> str "on" ++ spc () ++ pr_constr env c
- | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
-
-let pr_side = function
- Lhs -> str "=~"
- | Rhs -> str "~="
-
-let rec pr_bare_proof_instr _then _thus env = function
- | Pescape -> str "escape"
- | Pthen i -> pr_bare_proof_instr true _thus env i
- | Pthus i -> pr_bare_proof_instr _then true env i
- | Phence i -> pr_bare_proof_instr true true env i
- | Pcut c ->
- begin
- match _then,_thus with
- false,false -> str "have" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
- | false,true -> str "thus" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
- | true,false -> str "then" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
- | true,true -> str "hence" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
- end
- | Psuffices c ->
- str "suffices" ++ pr_cut pr_suffices_clause env c
- | Prew (sid,c) ->
- (if _thus then str "thus" else str " ") ++ spc () ++
- pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
- | Passume hyps ->
- str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
- | Plet hyps ->
- str "let" ++ print_vars pr_constr _I env false true "let" hyps
- | Pclaim st ->
- str "claim" ++ spc () ++ pr_statement pr_constr env st
- | Pfocus st ->
- str "focus on" ++ spc () ++ pr_statement pr_constr env st
- | Pconsider (id,hyps) ->
- str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
- ++ spc () ++ str "from " ++ pr_constr env id
- | Pgiven hyps ->
- str "given" ++ print_vars pr_constr _I env false false "given" hyps
- | Ptake witl ->
- str "take" ++ spc () ++
- prlist_with_sep pr_coma (pr_constr env) witl
- | Pdefine (id,args,body) ->
- str "define" ++ spc () ++ pr_id id ++ spc () ++
- prlist_with_sep spc
- (fun st -> str "(" ++
- pr_statement pr_constr env st ++ str ")") args ++ spc () ++
- str "as" ++ (pr_constr env body)
- | Pcast (id,typ) ->
- str "reconsider" ++ spc () ++
- pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
- str "as" ++ spc () ++ (pr_constr env typ)
- | Psuppose hyps ->
- str "suppose" ++
- print_hyps pr_constr _I env false false "we have" hyps
- | Pcase (params,pat,hyps) ->
- str "suppose it is" ++ spc () ++ pr_pat pat ++
- (if params = [] then mt () else
- (spc () ++ str "with" ++ spc () ++
- prlist_with_sep spc
- (fun st -> str "(" ++
- pr_statement pr_constr env st ++ str ")") params ++ spc ()))
- ++
- (if hyps = [] then mt () else
- (spc () ++ str "and" ++
- print_hyps (pr_or_thesis pr_constr) type_or_thesis
- env false false "we have" hyps))
- | Pper (et,c) ->
- str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
- pr_casee env c
- | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
- | _ -> anomaly "unprintable instruction"
-
-let pr_emph = function
- 0 -> str " "
- | 1 -> str "* "
- | 2 -> str "** "
- | 3 -> str "*** "
- | _ -> anomaly "unknown emphasis"
-
-let pr_proof_instr env instr =
- pr_emph instr.emph ++ spc () ++
- pr_bare_proof_instr false false env instr.instr
-
diff --git a/parsing/ppdecl_proof.mli b/parsing/ppdecl_proof.mli
deleted file mode 100644
index fd6fb6637..000000000
--- a/parsing/ppdecl_proof.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-
-val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9ebf77adb..dc61aaa26 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -774,23 +774,16 @@ let rec pr_vernac = function
hov 2 (str"Include " ++
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
(* Solving *)
- | VernacSolve (i,tac,deftac) ->
+ | VernacSolve (i,b,tac,deftac) ->
(if i = 1 then mt() else int i ++ str ": ") ++
+ (match b with None -> mt () | Some Dash -> str"-" | Some Star -> str"*" | Some Plus -> str"+") ++
pr_raw_tactic tac
- ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
+ ++ (try if deftac then str ".." else mt ()
with UserError _|Stdpp.Exc_located _ -> mt())
| VernacSolveExistential (i,c) ->
str"Existential " ++ int i ++ pr_lconstrarg c
- (* MMode *)
-
- | VernacProofInstr instr -> anomaly "Not implemented"
- | VernacDeclProof -> str "proof"
- | VernacReturn -> str "return"
-
- (* /MMode *)
-
(* Auxiliary file and library management *)
| VernacRequireFrom (exp,spe,f) -> hov 2
(str"Require" ++ spc() ++ pr_require_token exp ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d9dced791..cd07c4e15 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -22,13 +22,14 @@ open Libnames
open Nametab
open Evd
open Proof_type
-open Decl_mode
open Refiner
open Pfedit
open Ppconstr
open Constrextern
open Tacexpr
+open Store.Field
+
let emacs_str s alts =
match !Flags.print_emacs, !Flags.print_emacs_safechar with
| true, true -> alts
@@ -265,18 +266,13 @@ let pr_subgoal_metas metas env=
hv 0 (prlist_with_sep mt pr_one metas)
(* display complete goal *)
-let default_pr_goal g =
- let env = evar_unfiltered_env g in
+let default_pr_goal gs =
+ let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
+ let env = Goal.V82.unfiltered_env sigma g in
let preamb,thesis,penv,pc =
- if g.evar_extra = None then
- mt (), mt (),
- pr_context_of env,
- pr_ltype_env_at_top env g.evar_concl
- else
- (str " *** Declarative Mode ***" ++ fnl ()++fnl ()),
- (str "thesis := " ++ fnl ()),
- pr_context_of env,
- pr_ltype_env_at_top env g.evar_concl
+ mt (), mt (),
+ pr_context_of env,
+ pr_ltype_env_at_top env (Goal.V82.concl sigma g)
in
preamb ++
str" " ++ hv 0 (penv ++ fnl () ++
@@ -285,9 +281,10 @@ let default_pr_goal g =
thesis ++ str " " ++ pc) ++ fnl ()
(* display the conclusion of a goal *)
-let pr_concl n g =
- let env = evar_env g in
- let pc = pr_ltype_env_at_top env g.evar_concl in
+let pr_concl n sigma g =
+ let (g,sigma) = Goal.V82.nf_evar sigma g in
+ let env = Goal.V82.env sigma g in
+ let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in
str (emacs_str (String.make 1 (Char.chr 253)) "") ++
str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc
@@ -313,12 +310,12 @@ let rec pr_evars_int i = function
str (string_of_existential ev) ++ str " : " ++ pegl)) ++
fnl () ++ pei
-let default_pr_subgoal n =
+let default_pr_subgoal n sigma =
let rec prrec p = function
| [] -> error "No such goal."
| g::rest ->
if p = 1 then
- let pg = default_pr_goal g in
+ let pg = default_pr_goal { sigma=sigma ; it=g } in
v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
else
prrec (p-1) rest
@@ -343,17 +340,17 @@ let default_pr_subgoals close_cmd sigma = function
str "variables:" ++ fnl () ++ (hov 0 pei))
end
| [g] ->
- let pg = default_pr_goal g in
+ let pg = default_pr_goal { it = g ; sigma = sigma } in
v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
| g1::rest ->
let rec pr_rec n = function
| [] -> (mt ())
| g::rest ->
- let pc = pr_concl n g in
+ let pc = pr_concl n sigma g in
let prest = pr_rec (n+1) rest in
(cut () ++ pc ++ prest)
in
- let pg1 = default_pr_goal g1 in
+ let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
let prest = pr_rec 2 rest in
v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
++ pg1 ++ prest ++ fnl ())
@@ -365,8 +362,8 @@ let default_pr_subgoals close_cmd sigma = function
type printer_pr = {
pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
- pr_subgoal : int -> goal list -> std_ppcmds;
- pr_goal : goal -> std_ppcmds;
+ pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal : goal sigma -> std_ppcmds;
}
let default_printer_pr = {
@@ -387,25 +384,29 @@ let pr_goal x = !printer_pr.pr_goal x
(**********************************************************************)
let pr_open_subgoals () =
- let pfts = get_pftreestate () in
- let gls = fst (frontier (proof_of_pftreestate pfts)) in
- match focus() with
- | 0 ->
- let sigma = (top_goal_of_pftreestate pfts).sigma in
- let close_cmd = Decl_mode.get_end_command pfts in
- pr_subgoals close_cmd sigma gls
- | n ->
- assert (n > List.length gls);
- if List.length gls < 2 then
- pr_subgoal n gls
- else
- (* LEM TODO: this way of saying how many subgoals has to be abstracted out*)
- v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
- pr_subgoal n gls)
+ let p = Proof_global.give_me_the_proof () in
+ let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
+ begin match goals with
+ | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+ begin match bgoals with
+ | [] -> pr_subgoals None sigma goals
+ | _ -> pr_subgoals None bsigma bgoals ++ fnl () ++ fnl () ++
+ str"This subproof is complete, but there are still unfocused goals:"
+ (* spiwack: to stay compatible with the proof general and coqide,
+ I use print the message after the goal. It would be better to have
+ something like:
+ str"This subproof is complete, but there are still unfocused goals:"
+ ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals
+ instead. But it doesn't quite work.
+ *)
+ end
+ | _ -> pr_subgoals None sigma goals
+ end
let pr_nth_open_subgoal n =
- let pf = proof_of_pftreestate (get_pftreestate ()) in
- pr_subgoal n (fst (frontier pf))
+ let pf = get_pftreestate () in
+ let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+ pr_subgoal n sigma gls
(* Elementary tactics *)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 1797eaf22..2c1586abf 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -101,9 +101,9 @@ val pr_transparent_state : transparent_state -> std_ppcmds
(* Proofs *)
-val pr_goal : goal -> std_ppcmds
+val pr_goal : goal sigma -> std_ppcmds
val pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds
-val pr_subgoal : int -> goal list -> std_ppcmds
+val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds
val pr_open_subgoals : unit -> std_ppcmds
val pr_nth_open_subgoal : int -> std_ppcmds
@@ -130,8 +130,8 @@ val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
type printer_pr = {
pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
- pr_subgoal : int -> goal list -> std_ppcmds;
- pr_goal : goal -> std_ppcmds;
+ pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal : goal sigma -> std_ppcmds;
};;
val set_printer_pr : printer_pr -> unit
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index c09b3431e..bf554acf6 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -14,8 +14,6 @@ open Sign
open Evd
open Tacexpr
open Proof_type
-open Proof_trees
-open Decl_expr
open Logic
open Printer
@@ -26,16 +24,12 @@ let pr_tactic = function
| t ->
Pptactic.pr_tactic (Global.env()) t
-let pr_proof_instr instr =
- Ppdecl_proof.pr_proof_instr (Global.env()) instr
-
let pr_rule = function
| Prim r -> hov 0 (pr_prim_rule r)
| Nested(cmpd,_) ->
begin
match cmpd with
| Tactic (texp,_) -> hov 0 (pr_tactic texp)
- | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
end
| Daimon -> str "<Daimon>"
| Decl_proof _ -> str "proof"
@@ -62,33 +56,23 @@ let pr_rule_dot_fnl = function
exception Different
-(* We remove from the var context of env what is already in osign *)
-let thin_sign osign sign =
- Sign.fold_named_context
- (fun (id,c,ty as d) sign ->
- try
- if Sign.lookup_named id osign = (id,c,ty) then sign
- else raise Different
- with Not_found | Different -> Environ.push_named_context_val d sign)
- sign ~init:Environ.empty_named_context_val
-
-let rec print_proof _sigma osign pf =
- let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
- let hyps' = thin_sign osign hyps in
+let rec print_proof sigma osign pf =
+ (* spiwack: [osign] is currently ignored, not sure if this function is even used. *)
+ let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in
match pf.ref with
| None ->
- hov 0 (pr_goal {pf.goal with evar_hyps=hyps'})
+ hov 0 (pr_goal {sigma = sigma; it=pf.goal })
| Some(r,spfl) ->
hov 0
- (hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++
+ (hov 0 (pr_goal {sigma = sigma; it=pf.goal }) ++
spc () ++ str" BY " ++
hov 0 (pr_rule r) ++ fnl () ++
str" " ++
- hov 0 (prlist_with_sep pr_fnl (print_proof _sigma hyps) spfl))
+ hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl))
-let pr_change gl =
+let pr_change sigma gl =
str"change " ++
- pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
+ pr_lconstr_env (Goal.V82.env sigma gl) (Goal.V82.concl sigma gl) ++ str"."
let print_decl_script tac_printer ?(nochange=true) sigma pf =
let rec print_prf pf =
@@ -97,36 +81,10 @@ let print_decl_script tac_printer ?(nochange=true) sigma pf =
(if nochange then
(str"<Your Proof Text here>")
else
- pr_change pf.goal)
+ pr_change sigma pf.goal)
++ fnl ()
| Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
| Some (Prim Change_evars,[subpf]) -> print_prf subpf
- | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
- begin
- match instr.instr,subprfs with
- Pescape,[{ref=Some(_,subsubprfs)}] ->
- hov 7
- (pr_rule_dot_fnl rule ++
- prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
- if opened then mt () else str "return."
- | Pclaim _,[body;cont] ->
- hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
- (if opened then mt () else str "end claim." ++ fnl ()) ++
- print_prf cont
- | Pfocus _,[body;cont] ->
- hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++
- fnl () ++
- (if opened then mt () else str "end focus." ++ fnl ()) ++
- print_prf cont
- | (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
- hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
- print_prf cont
- | _,[next] ->
- pr_rule_dot_fnl rule ++ print_prf next
- | _,[] ->
- pr_rule_dot rule
- | _,_ -> anomaly "unknown branching instruction"
- end
| _ -> anomaly "Not Applicable" in
print_prf pf
@@ -137,12 +95,12 @@ let print_script ?(nochange=true) sigma pf =
(if nochange then
(str"<Your Tactic Text here>")
else
- pr_change pf.goal)
+ pr_change sigma pf.goal)
++ fnl ()
| Some(Decl_proof opened,script) ->
assert (List.length script = 1);
begin
- if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())
+ if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())
end ++
begin
hov 0 (str "proof." ++ fnl () ++
@@ -153,10 +111,10 @@ let print_script ?(nochange=true) sigma pf =
if opened then mt () else (str "end proof." ++ fnl ())
end
| Some(Daimon,spfl) ->
- ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+ ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
prlist_with_sep pr_fnl print_prf spfl )
| Some(rule,spfl) ->
- ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+ ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
pr_rule_dot_fnl rule ++
prlist_with_sep pr_fnl print_prf spfl ) in
print_prf pf
@@ -168,13 +126,12 @@ let print_treescript ?(nochange=true) sigma pf =
match pf.ref with
| None ->
if nochange then
- if pf.goal.evar_extra=None then str"<Your Tactic Text here>"
- else str"<Your Proof Text here>"
- else pr_change pf.goal
+ str"<Your Proof Text here>"
+ else pr_change sigma pf.goal
| Some(Decl_proof opened,script) ->
assert (List.length script = 1);
begin
- if nochange then mt () else pr_change pf.goal ++ fnl ()
+ if nochange then mt () else pr_change sigma pf.goal ++ fnl ()
end ++
hov 0
begin str "proof." ++ fnl () ++
@@ -184,16 +141,16 @@ let print_treescript ?(nochange=true) sigma pf =
if opened then mt () else (str "end proof." ++ fnl ())
end
| Some(Daimon,spfl) ->
- (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
+ (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl
| Some(r,spfl) ->
let indent = if List.length spfl >= 2 then 1 else 0 in
- (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
+ (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
in hov 0 (print_prf pf)
let rec print_info_script sigma osign pf =
- let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+ let sign = Goal.V82.hyps sigma pf.goal in
match pf.ref with
| None -> (mt ())
| Some(r,spfl) ->
@@ -214,12 +171,4 @@ let rec print_info_script sigma osign pf =
let format_print_info_script sigma osign pf =
hov 0 (print_info_script sigma osign pf)
-let print_subscript sigma sign pf =
- if is_tactic_proof pf then
- format_print_info_script sigma sign (subproof_of_proof pf)
- else
- format_print_info_script sigma sign pf
-
-let _ = Refiner.set_info_printer print_subscript
-let _ = Refiner.set_proof_printer print_proof
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index d46f19c64..96cbeb9a8 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -21,7 +21,6 @@ open Proof_type
val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
val pr_rule : rule -> std_ppcmds
val pr_tactic : tactic_expr -> std_ppcmds
-val pr_proof_instr : Decl_expr.proof_instr -> Pp.std_ppcmds
val print_script :
?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
val print_treescript :
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index e8a3094b9..e1997b878 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -48,9 +48,10 @@ let make_clauses s l =
let mlexpr_of_clause =
mlexpr_of_list
- (fun (a,b,c) -> mlexpr_of_list make_prod_item (GramTerminal a::b))
+ (fun (a,b,c) -> mlexpr_of_list make_prod_item
+ (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b))
-let declare_command loc s cl =
+let declare_command loc s nt cl =
let gl = mlexpr_of_clause cl in
let icl = make_clauses s cl in
<:str_item<
@@ -59,7 +60,7 @@ let declare_command loc s cl =
open Extrawit;
try Vernacinterp.vinterp_add $mlexpr_of_string s$ (fun [ $list:icl$ ])
with e -> Pp.pp (Cerrors.explain_exn e);
- Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $gl$;
+ Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$;
end
>>
@@ -71,13 +72,22 @@ EXTEND
[ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT;
OPT "|"; l = LIST1 rule SEP "|";
"END" ->
- declare_command loc s l ] ]
+ declare_command loc s <:expr<None>> l
+ | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT;
+ OPT "|"; l = LIST1 rule SEP "|";
+ "END" ->
+ declare_command loc s <:expr<Some $lid:nt$>> l ] ]
;
+ (* spiwack: comment-by-guessing: it seems that the isolated string (which
+ otherwise could have been another argument) is not passed to the
+ VernacExtend interpreter function to discriminate between the clauses. *)
rule:
[ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
->
if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty.");
- (s,l,<:expr< fun () -> $e$ >>)
+ (Some s,l,<:expr< fun () -> $e$ >>)
+ | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
+ (None,l,<:expr< fun () -> $e$ >>)
] ]
;
args:
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 11:27:19 +0000