aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/build/windows/makecoq_mingw.sh2
-rw-r--r--dev/top_printers.ml4
-rw-r--r--grammar/argextend.mlp12
-rw-r--r--grammar/q_util.mli2
-rw-r--r--grammar/q_util.mlp2
-rw-r--r--grammar/tacextend.mlp17
-rw-r--r--grammar/vernacextend.mlp16
-rw-r--r--parsing/egramml.ml4
-rw-r--r--parsing/egramml.mli2
-rw-r--r--plugins/.dir-locals.el4
-rw-r--r--plugins/ltac/extraargs.ml420
-rw-r--r--plugins/ltac/extraargs.mli4
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_ltac.ml48
-rw-r--r--plugins/ltac/g_tactic.ml413
-rw-r--r--plugins/ltac/pptactic.ml7
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacentries.ml14
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--test-suite/Makefile5
-rw-r--r--test-suite/success/ltac.v7
-rw-r--r--toplevel/coqtop.ml3
-rw-r--r--toplevel/vernac.ml23
-rw-r--r--vernac/obligations.ml12
24 files changed, 129 insertions, 58 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 52b158871b..98e80c7652 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1082,7 +1082,7 @@ function make_coq {
copq_coq_gtk
copy_coq_license
- # make clean seems to br broken for 8.5pl2
+ # make clean seems to be broken for 8.5pl2
# 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
# 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
# make clean
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f8498c4023..ce6d5dff05 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -510,7 +510,7 @@ let _ =
extend_vernac_command_grammar ("PrintConstr", 0) None
[GramTerminal "PrintConstr";
GramNonTerminal
- (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+ (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
let _ =
try
@@ -526,7 +526,7 @@ let _ =
extend_vernac_command_grammar ("PrintPureConstr", 0) None
[GramTerminal "PrintPureConstr";
GramNonTerminal
- (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+ (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
(* Setting printer of unbound global reference *)
open Names
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index d00ee4e5d2..5cfcc6fd22 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -40,7 +40,8 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
let make_act loc act pil =
let rec make = function
| [] -> <:expr< (fun loc -> $act$) >>
- | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
+ | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
+ | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
| ExtTerminal _ :: tl ->
<:expr< (fun _ -> $make tl$) >> in
make (List.rev pil)
@@ -63,7 +64,7 @@ let is_ident x = function
| _ -> false
let make_extend loc s cl wit = match cl with
-| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act ->
+| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
(** Special handling of identity arguments by not redeclaring an entry *)
<:str_item<
value $lid:s$ =
@@ -246,10 +247,13 @@ EXTEND
genarg:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING -> ExtTerminal s
] ]
;
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 5b3eb32027..0b3def058f 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -23,7 +23,7 @@ type user_symbol =
type extend_token =
| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 8b930cf360..87262e1c8e 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -25,7 +25,7 @@ type user_symbol =
type extend_token =
| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
let mlexpr_of_list f l =
List.fold_right
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index b14fba9758..3057ee58ca 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -31,19 +31,19 @@ let mlexpr_of_ident id =
let rec make_patt = function
| [] -> <:patt< [] >>
- | ExtNonTerminal (_, p) :: l ->
+ | ExtNonTerminal (_, Some p) :: l ->
<:patt< [ $lid:p$ :: $make_patt l$ ] >>
| _::l -> make_patt l
let rec make_let raw e = function
| [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
- | ExtNonTerminal (g, p) :: l ->
+ | ExtNonTerminal (g, Some p) :: l ->
let t = type_of_user_symbol g in
let loc = MLast.loc_of_expr e in
let e = make_let raw e l in
let v =
if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
- else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
+ else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
<:expr< let $lid:p$ = $v$ in $e$ >>
| _::l -> make_let raw e l
@@ -75,7 +75,7 @@ let rec mlexpr_of_symbol = function
let make_prod_item = function
| ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
| ExtNonTerminal (g, id) ->
- <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
+ <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_option mlexpr_of_ident id$ >>
let mlexpr_of_clause cl =
mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
@@ -87,7 +87,7 @@ let is_constr_gram = function
| _ -> false
let make_var = function
- | ExtNonTerminal (_, p) -> Some p
+ | ExtNonTerminal (_, p) -> p
| _ -> assert false
let declare_tactic loc tacname ~level classification clause = match clause with
@@ -158,10 +158,13 @@ EXTEND
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING ->
let () = if s = "" then failwith "Empty terminal." in
ExtTerminal s
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 436a7f0d98..7c99b52e85 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -27,7 +27,7 @@ type rule = {
let rec make_let e = function
| [] -> e
- | ExtNonTerminal (g, p) :: l ->
+ | ExtNonTerminal (g, Some p) :: l ->
let t = type_of_user_symbol g in
let loc = MLast.loc_of_expr e in
let e = make_let e l in
@@ -42,7 +42,7 @@ let make_clause { r_patt = pt; r_branch = e; } =
(* To avoid warnings *)
let mk_ignore c pt =
let fold accu = function
- | ExtNonTerminal (_, p) -> p :: accu
+ | ExtNonTerminal (_, Some p) -> p :: accu
| _ -> accu
in
let names = List.fold_left fold [] pt in
@@ -101,10 +101,11 @@ let make_fun_classifiers loc s c l =
let make_prod_item = function
| ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
- | ExtNonTerminal (g, id) ->
+ | ExtNonTerminal (g, ido) ->
let nt = type_of_user_symbol g in
let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
- <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
+ let typ = match ido with None -> None | Some _ -> Some nt in
+ <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_option (make_rawwit loc) typ$
$mlexpr_of_prod_entry_key base g$ >>
let mlexpr_of_clause cl =
@@ -178,10 +179,13 @@ EXTEND
args:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING ->
ExtTerminal s
] ]
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 97a3e89a59..984957589f 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+ Loc.t * 'a raw_abstract_argument_type option * ('s, 'a) symbol -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
@@ -38,7 +38,7 @@ let rec ty_rule_of_gram = function
AnyTyRule r
| GramNonTerminal (_, t, tok) :: rem ->
let AnyTyRule rem = ty_rule_of_gram rem in
- let inj = Some (fun obj -> Genarg.in_gen t obj) in
+ let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
let r = TyNext (rem, tok, inj) in
AnyTyRule r
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 1ad9472007..29baaf052b 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -15,7 +15,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+ | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type option *
('s, 'a) Extend.symbol -> 's grammar_prod_item
val extend_vernac_command_grammar :
diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el
new file mode 100644
index 0000000000..4e8830f6c1
--- /dev/null
+++ b/plugins/.dir-locals.el
@@ -0,0 +1,4 @@
+((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
+ buffer-file-name ".dir-locals.el")))
+ (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq"))
+ (setq-local coq-prog-name (expand-file-name "../bin/coqtop")))))))
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432c..ec3a49df49 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause
| [ in_clause'(cl) ] -> [ cl ]
END
+let local_test_lpar_id_colon =
+ let err () = raise Stream.Failure in
+ Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+ (fun strm ->
+ match Util.stream_nth 0 strm with
+ | Tok.KEYWORD "(" ->
+ (match Util.stream_nth 1 strm with
+ | Tok.IDENT _ ->
+ (match Util.stream_nth 2 strm with
+ | Tok.KEYWORD ":" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
+let pr_lpar_id_colon _ _ _ _ = mt ()
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
+| [ local_test_lpar_id_colon(x) ] -> [ () ]
+END
+
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
let pr_r_nat_field natf =
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfadd..9b41675120 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
(int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
raw_tactic_expr option -> Pp.std_ppcmds
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
(** Spiwack: Primitive for retroknowledge registration *)
val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e6ccaf84a..bd48614dbc 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -463,7 +463,7 @@ open Evar_tactics
(* TODO: add support for some test similar to g_constr.name_colon so that
expressions like "evar (list A)" do not raise a syntax error *)
TACTIC EXTEND evar
- [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+ [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
END
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c23..d717ed0a53 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -460,7 +460,9 @@ END
let pr_ltac_production_item = function
| Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, (arg, sep), id) ->
+| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg
+| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false
+| Tacentries.TacNonTerm (_, (arg, sep), Some id) ->
let sep = match sep with
| None -> mt ()
| Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -470,7 +472,9 @@ let pr_ltac_production_item = function
VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
| [ string(s) ] -> [ Tacentries.TacTerm s ]
| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
- [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ]
+ [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ]
+| [ ident(nt) ] ->
+ [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ]
END
VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af5..e33c25cf88 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq =
| _ -> err ())
(* idem for (x:t) *)
-let test_lpar_id_colon =
- Gram.Entry.of_parser "lpar_id_colon"
- (fun strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ ->
- (match stream_nth 2 strm with
- | KEYWORD ":" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+open Extraargs
(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b73b66e56f..a619575591 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
@@ -264,8 +264,9 @@ type 'a extra_genarg_printer =
let rec pack prods args = match prods, args with
| [], [] -> []
| TacTerm s :: prods, args -> TacTerm s :: pack prods args
- | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
- TacNonTerm (loc, (symb, arg), id) :: pack prods args
+ | TacNonTerm (_, _, None) :: prods, args -> pack prods args
+ | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args ->
+ TacNonTerm (loc, (symb, arg), ido) :: pack prods args
| _ -> raise Not_found
in
let prods = pack pp.pptac_prods l in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 729338fb9a..433f342c4f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 32750383b8..91262f6fd6 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -21,7 +21,7 @@ open Nameops
type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type raw_argument = string * string option
type argument = Genarg.ArgT.any Extend.user_symbol
@@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
in
let map = function
| TacTerm s -> GramTerminal s
- | TacNonTerm (loc, s, _) ->
+ | TacNonTerm (loc, s, ido) ->
let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
- GramNonTerminal (loc, typ, e)
+ GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e)
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
@@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry =
let interp_prod_item = function
| TacTerm s -> TacTerm s
- | TacNonTerm (loc, (nt, sep), id) ->
+ | TacNonTerm (loc, (nt, sep), ido) ->
let symbol = parse_user_entry nt sep in
let interp s = function
| None ->
@@ -220,7 +220,7 @@ let interp_prod_item = function
end
in
let symbol = interp_entry_name interp symbol in
- TacNonTerm (loc, symbol, id)
+ TacNonTerm (loc, symbol, ido)
let make_fresh_key =
let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
let cons_production_parameter = function
| TacTerm _ -> None
-| TacNonTerm (_, _, id) -> Some id
+| TacNonTerm (_, _, ido) -> ido
let add_glob_tactic_notation local ~level prods forml ids tac =
let parule = {
@@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
let open Tacexpr in
let get_id = function
| TacTerm s -> None
- | TacNonTerm (_, _, id) -> Some id
+ | TacNonTerm (_, _, ido) -> ido
in
let ids = List.map_filter get_id prods in
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 0695044736..dac62dad33 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type raw_argument = string * string option
(** An argument type as provided in Tactic notations, i.e. a string like
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 39ef05269f..afaa48463b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -408,6 +408,11 @@ modules/%.vo: modules/%.v
misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
+misc/universes.log: misc/universes/all_stdlib.v
+
+misc/universes/all_stdlib.v:
+ cd .. && $(MAKE) test-suite/$@
+
$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
@echo "TEST $<"
$(HIDE){ \
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index d7ec092d76..1d35f1ef6c 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -330,3 +330,10 @@ Fail match goal with
end
end.
Abort.
+
+(* Test evar syntax *)
+
+Goal True.
+evar (0=0).
+Abort.
+
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8f50bfb3d8..41d370ea57 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -641,6 +641,9 @@ let init_toplevel arglist =
init_library_roots ();
load_vernac_obj ();
require ();
+ (* XXX: This is incorrect in batch mode, as we will initialize
+ the STM before having done Declaremods.start_library, thus
+ state 1 is invalid. This bug was present in 8.5/8.6. *)
Stm.init ();
let sid = load_rcfile (Stm.get_current_state ()) in
(* XXX: We ignore this for now, but should be threaded to the toplevels *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index eaf685b184..deb2cc1e3f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -126,6 +126,16 @@ let rec interp_vernac sid (loc,com) =
let f = Loadpath.locate_file fname in
load_vernac verbosely sid f
| v ->
+
+ (* XXX: We need to run this before add as the classification is
+ highly dynamic and depends on the structure of the
+ document. Hopefully this is fixed when VtBack can be removed
+ and Undo etc... are just interpreted regularly. *)
+ let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
+ | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+ | _ -> false
+ in
+
let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
(* Main STM interaction *)
@@ -139,11 +149,12 @@ let rec interp_vernac sid (loc,com) =
if check_proof then Stm.finish ();
(* We could use a more refined criteria that depends on the
- vernac. For now we imitate the old approach. *)
- let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
- not (Proof_global.there_are_pending_proofs ()) in
+ vernac. For now we imitate the old approach and rely on the
+ classification. *)
+ let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+ is_proof_step && Proof_global.there_are_pending_proofs () in
- if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+ if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
nsid
in
try
@@ -153,7 +164,9 @@ let rec interp_vernac sid (loc,com) =
let com = if !Flags.time then VernacTime (loc,com) else com in
interp com
with reraise ->
- ignore(Stm.edit_at sid);
+ (* XXX: In non-interactive mode edit_at seems to do very weird
+ things, so we better avoid it while we investigate *)
+ if not !Flags.batch_mode then ignore(Stm.edit_at sid);
let (reraise, info) = CErrors.push reraise in
let loc' = Option.default Loc.ghost (Loc.get_loc info) in
if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5233fab151..24cb9c886e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -631,6 +631,16 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+let it_mkLambda_or_LetIn_or_clean t ctx =
+ let open Context.Rel.Declaration in
+ let fold t decl =
+ if is_local_assum decl then mkLambda_or_LetIn decl t
+ else
+ if noccurn 1 t then subst1 mkProp t
+ else mkLambda_or_LetIn decl t
+ in
+ Context.Rel.fold_inside fold ctx ~init:t
+
let declare_obligation prg obl body ty uctx =
let body = prg.prg_reduce body in
let ty = Option.map prg.prg_reduce ty in
@@ -664,7 +674,7 @@ let declare_obligation prg obl body ty uctx =
if poly then
Some (DefinedObl constant)
else
- Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
+ Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
notations obls impls kind reduce hook =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:14:33 +0000