aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/PULL_REQUEST_TEMPLATE.md16
-rw-r--r--dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh4
-rw-r--r--ide/ide_slave.ml4
-rw-r--r--intf/vernacexpr.ml5
-rw-r--r--lib/flags.ml10
-rw-r--r--lib/flags.mli7
-rw-r--r--lib/system.ml10
-rw-r--r--lib/system.mli2
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--plugins/ltac/extratactics.ml470
-rw-r--r--plugins/ltac/rewrite.ml5
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--printing/ppvernac.ml2
-rw-r--r--stm/stm.ml15
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--tactics/leminv.ml7
-rw-r--r--tactics/leminv.mli2
-rw-r--r--toplevel/coqinit.ml6
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqloop.ml10
-rw-r--r--toplevel/coqloop.mli4
-rw-r--r--toplevel/coqtop.ml39
-rw-r--r--toplevel/vernac.ml17
-rw-r--r--toplevel/vernac.mli4
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/vernacentries.ml19
-rw-r--r--vernac/vernacprop.ml17
-rw-r--r--vernac/vernacprop.mli2
29 files changed, 146 insertions, 151 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
new file mode 100644
index 000000000..c7437c4a4
--- /dev/null
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -0,0 +1,16 @@
+<!-- Thank you for your contribution.
+ Make sure you read the contributing guide and fill this template. -->
+
+
+<!-- Keep what applies -->
+**Kind:** documentation / bug fix / feature / performance / infrastructure.
+
+
+<!-- If this is a bug fix, make sure the bug was reported beforehand. -->
+Fixes / closes #????
+
+
+<!-- If this is a feature pull request / breaks compatibility: -->
+<!-- (Otherwise, remove these lines.) -->
+- [ ] Corresponding documentation was added / updated.
+- [ ] Entry added in [CHANGES](/CHANGES).
diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
new file mode 100644
index 000000000..c2e367038
--- /dev/null
+++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then
+ Equations_CI_BRANCH=rm-local-polymorphic-flag
+ Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+fi
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index aafc3fc59..5f40a2242 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -69,9 +69,7 @@ let ide_cmd_checks ~id (loc,ast) =
if is_known_option ast then
warn "Set this option from the IDE menu instead";
if is_navigation_vernac ast || is_undo ast then
- warn "Use IDE navigation instead";
- if is_query ast then
- warn "Query commands should not be inserted in scripts"
+ warn "Use IDE navigation instead"
(** Interpretation (cf. [Ide_intf.interp]) *)
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index a90e5501a..5106e513b 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -479,8 +479,9 @@ and vernac_argument_status = {
type vernac_control =
| VernacExpr of vernac_expr
- (* Control *)
- | VernacTime of vernac_control located
+ (* boolean is true when the `-time` batch-mode command line flag was set.
+ the flag is used to print differently in `-time` vs `Time foo` *)
+ | VernacTime of bool * vernac_control located
| VernacRedirect of string * vernac_control located
| VernacTimeout of int * vernac_control
| VernacFail of vernac_control
diff --git a/lib/flags.ml b/lib/flags.ml
index 644f66d02..ee4c0734a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -48,8 +48,6 @@ let profile = false
let ide_slave = ref false
let ideslave_coqtop_flags = ref None
-let time = ref false
-
let raw_print = ref false
let univ_print = ref false
@@ -110,14 +108,6 @@ let universe_polymorphism = ref false
let make_universe_polymorphism b = universe_polymorphism := b
let is_universe_polymorphism () = !universe_polymorphism
-let local_polymorphic_flag = ref None
-let use_polymorphic_flag () =
- match !local_polymorphic_flag with
- | Some p -> local_polymorphic_flag := None; p
- | None -> is_universe_polymorphism ()
-let make_polymorphic_flag b =
- local_polymorphic_flag := Some b
-
let polymorphic_inductive_cumulativity = ref false
let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index 000862b2c..33d281798 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,9 +35,6 @@ val profile : bool
val ide_slave : bool ref
val ideslave_coqtop_flags : string option ref
-(* -time option: every command will be wrapped with `Time` *)
-val time : bool ref
-
(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref
@@ -77,10 +74,6 @@ val is_program_mode : unit -> bool
val make_universe_polymorphism : bool -> unit
val is_universe_polymorphism : unit -> bool
-(** Local universe polymorphism flag. *)
-val make_polymorphic_flag : bool -> unit
-val use_polymorphic_flag : unit -> bool
-
(** Global polymorphic inductive cumulativity flag. *)
val make_polymorphic_inductive_cumulativity : bool -> unit
val is_polymorphic_inductive_cumulativity : unit -> bool
diff --git a/lib/system.ml b/lib/system.ml
index 2c8dbac7c..e56736eb1 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -294,18 +294,18 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
real (round (sstop -. sstart)) ++ str "s" ++
str ")"
-let with_time time f x =
+let with_time ~batch f x =
let tstart = get_time() in
- let msg = if time then "" else "Finished transaction in " in
+ let msg = if batch then "" else "Finished transaction in " in
try
let y = f x in
let tend = get_time() in
- let msg2 = if time then "" else " (successful)" in
+ let msg2 = if batch then "" else " (successful)" in
Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
y
with e ->
let tend = get_time() in
- let msg = if time then "" else "Finished failing transaction in " in
- let msg2 = if time then "" else " (failure)" in
+ let msg = if batch then "" else "Finished failing transaction in " in
+ let msg2 = if batch then "" else " (failure)" in
Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
diff --git a/lib/system.mli b/lib/system.mli
index c02bc9c8a..0c0cc9fae 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -104,4 +104,4 @@ val get_time : unit -> time
val time_difference : time -> time -> float (** in seconds *)
val fmt_time_difference : time -> time -> Pp.t
-val with_time : bool -> ('a -> 'b) -> 'a -> 'b
+val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 29bcddaf4..92e60f465 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -68,7 +68,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
GEXTEND Gram
GLOBAL: vernac_control gallina_ext noedit_mode subprf;
vernac_control: FIRST
- [ [ IDENT "Time"; c = located_vernac -> VernacTime c
+ [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c)
| IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
| IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
| IDENT "Fail"; v = vernac_control -> VernacFail v
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 982fc7cc3..cf5125757 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -25,6 +25,7 @@ open Termops
open Equality
open Misctypes
open Proofview.Notations
+open Vernacinterp
DECLARE PLUGIN "ltac_plugin"
@@ -249,11 +250,10 @@ TACTIC EXTEND rewrite_star
(**********************************************************************)
(* Hint Rewrite *)
-let add_rewrite_hint bases ort t lcsr =
+let add_rewrite_hint ~poly bases ort t lcsr =
let env = Global.env() in
let sigma = Evd.from_env env in
- let poly = Flags.use_polymorphic_flag () in
- let f ce =
+ let f ce =
let c, ctx = Constrintern.interp_constr env sigma ce in
let ctx =
let ctx = UState.context_set ctx in
@@ -270,16 +270,16 @@ let add_rewrite_hint bases ort t lcsr =
let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
-VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint
+VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
[ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
- [ add_rewrite_hint bl o None l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- [ add_rewrite_hint bl o (Some t) l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- [ add_rewrite_hint ["core"] o None l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
- [ add_rewrite_hint ["core"] o (Some t) l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ]
END
(**********************************************************************)
@@ -290,7 +290,7 @@ open EConstr
open Vars
open Coqlib
-let project_hint pri l2r r =
+let project_hint ~poly pri l2r r =
let gr = Smartlocate.global_with_alias r in
let env = Global.env() in
let sigma = Evd.from_env env in
@@ -313,30 +313,28 @@ let project_hint pri l2r r =
let id =
Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
in
- let poly = Flags.use_polymorphic_flag () in
let ctx = Evd.const_univ_entry ~poly sigma in
let c = EConstr.to_constr sigma c in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
(info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
-let add_hints_iff ?locality l2r lc n bl =
- Hints.add_hints (Locality.make_module_locality locality) bl
- (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
+let add_hints_iff ~atts l2r lc n bl =
+ let open Vernacinterp in
+ Hints.add_hints (Locality.make_module_locality atts.locality) bl
+ (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality true lc n bl;
+ add_hints_iff ~atts true lc n bl;
st
end
]
| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality true lc n ["core"];
+ add_hints_iff ~atts true lc n ["core"];
st
end
]
@@ -346,15 +344,13 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality false lc n bl;
+ add_hints_iff ~atts false lc n bl;
st
end
]
| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality false lc n ["core"];
+ add_hints_iff ~atts false lc n ["core"];
st
end
]
@@ -430,34 +426,46 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
| [ "Type" ] -> [ InType ]
END*)
-VERNAC COMMAND EXTEND DeriveInversionClear
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ]
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ]
END
-VERNAC COMMAND EXTEND DeriveInversion
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion
| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s false inv_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ]
| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ]
END
-VERNAC COMMAND EXTEND DeriveDependentInversion
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion
| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s true dinv_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ]
END
-VERNAC COMMAND EXTEND DeriveDependentInversionClear
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear
| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ]
END
(**********************************************************************)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a698b05dd..3cbb11001 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1981,8 +1981,7 @@ let add_morphism_infer glob m n =
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
- poly (ConstRef cst));
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
else
let kind = Decl_kinds.Global, poly,
@@ -1993,7 +1992,7 @@ let add_morphism_infer glob m n =
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
- glob poly (ConstRef cst));
+ glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bc9990d02..f153b6341 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -87,7 +87,6 @@ type instance = {
(* Sections where the instance should be redeclared,
None for discard, Some 0 for none. *)
is_global: int option;
- is_poly: bool;
is_impl: global_reference;
}
@@ -97,7 +96,7 @@ let instance_impl is = is.is_impl
let hint_priority is = is.is_info.Vernacexpr.hint_priority
-let new_instance cl info glob poly impl =
+let new_instance cl info glob impl =
let global =
if glob then Some (Lib.sections_depth ())
else None
@@ -107,7 +106,6 @@ let new_instance cl info glob poly impl =
{ is_class = cl.cl_impl;
is_info = info ;
is_global = global ;
- is_poly = poly;
is_impl = impl }
(*
@@ -420,7 +418,7 @@ let declare_instance info local glob =
match class_of_constr Evd.empty (EConstr.of_constr ty) with
| Some (rels, ((tc,_), args) as _cl) ->
assert (not (isVarRef glob) || local);
- add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
+ add_instance (new_instance tc info (not local) glob)
| None -> ()
let add_class cl =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 0cbe1c71c..ee28ec173 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -53,7 +53,7 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
global_reference -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 418d4a0b8..e88284fb1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1223,7 +1223,7 @@ open Decl_kinds
let return = tag_vernac v in
match v with
| VernacExpr v' -> pr_vernac_expr v' ++ sep_end v'
- | VernacTime (_,v) ->
+ | VernacTime (_,(_,v)) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
| VernacRedirect (s, (_,v)) ->
return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
diff --git a/stm/stm.ml b/stm/stm.ml
index afb6fabcb..7045df0ed 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1935,15 +1935,16 @@ end = struct (* {{{ *)
let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
{ indentation; verbose; loc; expr = e; strlen }
=
- let e, time, fail =
- let rec find ~time ~fail = function
- | VernacTime (_,e) -> find ~time:true ~fail e
- | VernacRedirect (_,(_,e)) -> find ~time ~fail e
- | VernacFail e -> find ~time ~fail:true e
- | e -> e, time, fail in find ~time:false ~fail:false e in
+ let e, time, batch, fail =
+ let rec find ~time ~batch ~fail = function
+ | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e
+ | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e
+ | VernacFail e -> find ~time ~batch ~fail:true e
+ | e -> e, time, batch, fail in
+ find ~time:false ~batch:false ~fail:false e in
let st = Vernacstate.freeze_interp_state `No in
Vernacentries.with_fail st fail (fun () ->
- (if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
+ (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
Proof_global.with_current_proof (fun _ p ->
let goals, _, _, _, _ = Proof.proof p in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1291b7642..2fa47ba43 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -195,7 +195,7 @@ let classify_vernac e =
let rec static_control_classifier ~poly = function
| VernacExpr e -> static_classifier ~poly e
| VernacTimeout (_,e) -> static_control_classifier ~poly e
- | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+ | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
static_control_classifier ~poly e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier ~poly e with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 01065868d..197b3030d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -234,10 +234,9 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let p = Evarutil.nf_evars_universes sigma invProof in
p, sigma
-let add_inversion_lemma name env sigma t sort dep inv_op =
+let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
let univs =
- let poly = Flags.use_polymorphic_flag () in
Evd.const_univ_entry ~poly sigma
in
let entry = definition_entry ~univs invProof in
@@ -247,13 +246,13 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
(* inv_op = Inv (derives de complete inv. lemma)
* inv_op = InvNoThining (derives de semi inversion lemma) *)
-let add_inversion_lemma_exn na com comsort bool tac =
+let add_inversion_lemma_exn ~poly na com comsort bool tac =
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma, c = Constrintern.interp_type_evars env sigma com in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in
try
- add_inversion_lemma na env sigma c sort bool tac
+ add_inversion_lemma ~poly na env sigma c sort bool tac
with
| UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 8745ad397..f221b1fd9 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -14,6 +14,6 @@ open Misctypes
val lemInv_clause :
quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
-val add_inversion_lemma_exn :
+val add_inversion_lemma_exn : poly:bool ->
Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
unit
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3a195c1df..176dfb3c9 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true
let load_rc = ref true
let no_load_rc () = load_rc := false
-let load_rcfile doc sid =
+let load_rcfile ~time doc sid =
if !load_rc then
try
if !rcfile_specified then
if CUnix.file_readable_p !rcfile then
- Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
else
try
@@ -43,7 +43,7 @@ let load_rcfile doc sid =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
with Not_found -> doc, sid
(*
Flags.if_verbose
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 60ed698b8..c3fd72754 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -13,7 +13,7 @@ val set_debug : unit -> unit
val set_rcfile : string -> unit
val no_load_rc : unit -> unit
-val load_rcfile : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
val push_include : string -> Names.DirPath.t -> bool -> unit
(** [push_include phys_path log_path implicit] *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 910c81381..5c1b27c33 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -300,13 +300,13 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
is caught and handled (i.e. not re-raised).
*)
-let do_vernac doc sid =
+let do_vernac ~time doc sid =
top_stderr (fnl());
if !print_emacs then top_stderr (str (top_buffer.prompt doc));
resynch_buffer top_buffer;
try
let input = (top_buffer.tokens, None) in
- Vernac.process_expr doc sid (read_sentence ~doc sid (fst input))
+ Vernac.process_expr ~time doc sid (read_sentence ~doc sid (fst input))
with
| Stm.End_of_input | CErrors.Quit ->
top_stderr (fnl ()); raise CErrors.Quit
@@ -337,13 +337,13 @@ let loop_flush_all () =
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
-let rec loop doc =
+let rec loop ~time doc =
Sys.catch_break true;
try
reset_input_buffer doc stdin top_buffer;
(* Be careful to keep this loop tail-recursive *)
let rec vernac_loop doc sid =
- let ndoc, nsid = do_vernac doc sid in
+ let ndoc, nsid = do_vernac ~time doc sid in
loop_flush_all ();
vernac_loop ndoc nsid
(* We recover the current stateid, threading from the caller is
@@ -358,4 +358,4 @@ let rec loop doc =
fnl() ++
str"Please report" ++
strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
- loop doc
+ loop ~time doc
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 46934f326..09240ec82 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,8 +32,8 @@ val coqloop_feed : Feedback.feedback -> unit
(** Parse and execute one vernac command. *)
-val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
(** Main entry point of Coq: read and execute vernac commands. *)
-val loop : Stm.doc -> Stm.doc
+val loop : time:bool -> Stm.doc -> Stm.doc
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 437b7b0ac..a3a4e20af 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -80,6 +80,7 @@ let toploop_init = ref begin fun x ->
bogus. For now we just print to the console too *)
let coqtop_init_feed = Coqloop.coqloop_feed
let drop_last_doc = ref None
+let measure_time = ref false
(* Default toplevel loop *)
let console_toploop_run doc =
@@ -89,7 +90,7 @@ let console_toploop_run doc =
Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
- let doc = Coqloop.loop doc in
+ let doc = Coqloop.loop ~time:!measure_time doc in
(* Initialise and launch the Ocaml toplevel *)
drop_last_doc := Some doc;
Coqinit.init_ocaml_path();
@@ -180,19 +181,19 @@ let load_vernacular_list = ref ([] : (string * bool) list)
let add_load_vernacular verb s =
load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
-let load_vernacular doc sid =
+let load_vernacular ~time doc sid =
List.fold_left
(fun (doc,sid) (f_in, verbosely) ->
let s = Loadpath.locate_file f_in in
if !Flags.beautify then
- Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
+ Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in
else
- Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
+ Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s)
(doc, sid) (List.rev !load_vernacular_list)
-let load_init_vernaculars doc sid =
- let doc, sid = Coqinit.load_rcfile doc sid in
- load_vernacular doc sid
+let load_init_vernaculars ~time doc sid =
+ let doc, sid = Coqinit.load_rcfile ~time doc sid in
+ load_vernacular ~time doc sid
(******************************************************************************)
(* Required Modules *)
@@ -291,7 +292,7 @@ let ensure_exists f =
compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
(* Compile a vernac file *)
-let compile ~verbosely ~f_in ~f_out =
+let compile ~time ~verbosely ~f_in ~f_out =
let check_pending_proofs () =
let pfs = Proof_global.get_all_proof_names () in
if not (CList.is_empty pfs) then
@@ -316,7 +317,7 @@ let compile ~verbosely ~f_in ~f_out =
require_libs = require_libs ()
}) in
- let doc, sid = load_init_vernaculars doc sid in
+ let doc, sid = load_init_vernaculars ~time doc sid in
let ldir = Stm.get_ldir ~doc in
Aux_file.(start_aux_file
~aux_file:(aux_file_name_for long_f_dot_vo)
@@ -324,7 +325,7 @@ let compile ~verbosely ~f_in ~f_out =
Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
let wall_clock1 = Unix.gettimeofday () in
- let doc, _ = Vernac.load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+ let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
let _doc = Stm.join ~doc in
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
@@ -351,10 +352,10 @@ let compile ~verbosely ~f_in ~f_out =
require_libs = require_libs ()
}) in
- let doc, sid = load_init_vernaculars doc sid in
+ let doc, sid = load_init_vernaculars ~time doc sid in
let ldir = Stm.get_ldir ~doc in
- let doc, _ = Vernac.load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+ let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
let doc = Stm.finish ~doc in
check_pending_proofs ();
let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
@@ -369,9 +370,9 @@ let compile ~verbosely ~f_in ~f_out =
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
Library.save_library_raw lfdv sum lib univs proofs
-let compile ~verbosely ~f_in ~f_out =
+let compile ~time ~verbosely ~f_in ~f_out =
ignore(CoqworkmgrApi.get 1);
- compile ~verbosely ~f_in ~f_out;
+ compile ~time ~verbosely ~f_in ~f_out;
CoqworkmgrApi.giveback 1
let compile_file (verbosely,f_in) =
@@ -381,9 +382,9 @@ let compile_file (verbosely,f_in) =
else
compile ~verbosely ~f_in ~f_out:None
-let compile_files doc =
+let compile_files ~time =
if !compile_list == [] then ()
- else List.iter compile_file (List.rev !compile_list)
+ else List.iter (compile_file ~time) (List.rev !compile_list)
(******************************************************************************)
(* VIO Dispatching *)
@@ -736,7 +737,7 @@ let parse_args arglist =
|"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
|"-quick" -> compilation_mode := BuildVio
|"-list-tags" -> print_tags := true
- |"-time" -> Flags.time := true
+ |"-time" -> measure_time := true
|"-type-in-type" -> set_type_in_type ()
|"-unicode" -> add_require ("Utf8_core", None, Some false)
|"-v"|"--version" -> Usage.version (exitcode ())
@@ -812,12 +813,12 @@ let init_toplevel arglist =
{ doc_type = Interactive !toplevel_name;
require_libs = require_libs ()
}) in
- Some (load_init_vernaculars doc sid)
+ Some (load_init_vernaculars ~time:!measure_time doc sid)
with any -> flush_all(); fatal_error any
(* Non interactive *)
end else begin
try
- compile_files ();
+ compile_files ~time:!measure_time;
schedule_vio_checking ();
schedule_vio_compilation ();
check_vio_tasks ();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 24d414c88..6b45a94bc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -110,16 +110,15 @@ let pr_open_cur_subgoals () =
(* Stm.End_of_input -> true *)
(* | _ -> false *)
-let rec interp_vernac ~check ~interactive doc sid (loc,com) =
+let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
let interp v =
match under_control v with
| VernacLoad (verbosely, fname) ->
let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
let fname = CUnix.make_suffix fname ".v" in
let f = Loadpath.locate_file fname in
- load_vernac ~verbosely ~check ~interactive doc sid f
+ load_vernac ~time ~verbosely ~check ~interactive doc sid f
| _ ->
-
(* 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 VtMeta can be removed
@@ -158,8 +157,8 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
try
(* The -time option is only supported from console-based
clients due to the way it prints. *)
- if !Flags.time then print_cmd_header ?loc com;
- let com = if !Flags.time then VernacTime (loc,com) else com in
+ if time then print_cmd_header ?loc com;
+ let com = if time then VernacTime(time,(loc,com)) else com in
interp com
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
@@ -173,7 +172,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
end in iraise (reraise, info)
(* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~verbosely ~check ~interactive doc sid file =
+and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
let ft_beautify, close_beautify =
if !Flags.beautify_file then
let chan_beautify = open_out (file^beautify_suffix) in
@@ -215,7 +214,7 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
Option.iter (vernac_echo ?loc) in_echo;
checknav_simple (loc, ast);
- let ndoc, nsid = Flags.silently (interp_vernac ~check ~interactive !rdoc !rsid) (loc, ast) in
+ let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in
rsid := nsid;
rdoc := ndoc
done;
@@ -242,6 +241,6 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
of a new state label). An example of state-preserving command is one coming
from the query panel of Coqide. *)
-let process_expr doc sid loc_ast =
+let process_expr ~time doc sid loc_ast =
checknav_deep loc_ast;
- interp_vernac ~interactive:true ~check:true doc sid loc_ast
+ interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 8a798a98e..b77b024fa 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,9 +12,9 @@
expected to handle and print errors in form of exceptions, however
care is taken so the state machine is left in a consistent
state. *)
-val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
+val process_expr : time:bool -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
(** [load_vernac echo sid file] Loads [file] on top of [sid], will
echo the commands if [echo] is set. Callers are expected to handle
and print errors in form of exceptions. *)
-val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
+val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6914f899b..4a2dba859 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -69,8 +69,7 @@ let existing_instance glob g info =
let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
let _, r = Term.decompose_prod_assum instance in
match class_of_constr Evd.empty (EConstr.of_constr r) with
- | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
- (*FIXME*) (Flags.use_polymorphic_flag ()) c)
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
| None -> user_err ?loc:(loc_of_reference g)
~hdr:"declare_instance"
(Pp.str "Constant does not build instances of a declared type class.")
@@ -393,8 +392,7 @@ let context poly l =
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
match class_of_constr sigma (of_constr t) with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
- poly (ConstRef cst));
+ add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
| None -> status
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index aa6121c39..ded0d97e6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2132,10 +2132,6 @@ let check_vernac_supports_polymorphism c p =
| VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
| Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
-let enforce_polymorphism = function
- | None -> Flags.is_universe_polymorphism ()
- | Some b -> Flags.make_polymorphic_flag b; b
-
(** A global default timeout, controlled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2202,6 +2198,7 @@ let with_fail st b f =
end
let interp ?(verbosely=true) ?proof ~st (loc,c) =
+ let orig_univ_poly = Flags.is_universe_polymorphism () in
let orig_program_mode = Flags.is_program_mode () in
let rec control = function
| VernacExpr v ->
@@ -2213,8 +2210,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
control v
| VernacRedirect (s, (_,v)) ->
Topfmt.with_output_to_file s control v
- | VernacTime (_,v) ->
- System.with_time !Flags.time control v;
+ | VernacTime (batch, (_loc,v)) ->
+ System.with_time ~batch control v;
and aux ?polymorphism ~atts isprogcmd = function
@@ -2241,7 +2238,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
| c ->
check_vernac_supports_locality c atts.locality;
check_vernac_supports_polymorphism c polymorphism;
- let polymorphic = enforce_polymorphism polymorphism in
+ let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
+ Flags.make_universe_polymorphism polymorphic;
Obligations.set_program_mode isprogcmd;
try
vernac_timeout begin fun () ->
@@ -2249,9 +2247,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
if verbosely
then Flags.verbosely (interp ?proof ~atts ~st) c
else Flags.silently (interp ?proof ~atts ~st) c;
+ (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
+ we should not restore the previous state of the flag... *)
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode;
- ignore (Flags.use_polymorphic_flag ())
+ if (Flags.is_universe_polymorphism() = polymorphic) then
+ Flags.make_universe_polymorphism orig_univ_poly;
end
with
| reraise when
@@ -2262,8 +2263,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
let e = CErrors.push reraise in
let e = locate_if_not_already ?loc e in
let () = restore_timeout () in
+ Flags.make_universe_polymorphism orig_univ_poly;
Flags.program_mode := orig_program_mode;
- ignore (Flags.use_polymorphic_flag ());
iraise e
in
if verbosely
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 4a01ef2ef..4fdc78dd2 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -14,14 +14,14 @@ open Vernacexpr
let rec under_control = function
| VernacExpr c -> c
| VernacRedirect (_,(_,c))
- | VernacTime (_,c)
+ | VernacTime (_,(_,c))
| VernacFail c
| VernacTimeout (_,c) -> under_control c
let rec has_Fail = function
| VernacExpr c -> false
| VernacRedirect (_,(_,c))
- | VernacTime (_,c)
+ | VernacTime (_,(_,c))
| VernacTimeout (_,c) -> has_Fail c
| VernacFail _ -> true
@@ -38,7 +38,7 @@ let is_navigation_vernac c =
is_navigation_vernac_expr (under_control c)
let rec is_deep_navigation_vernac = function
- | VernacTime (_,c) -> is_deep_navigation_vernac c
+ | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c
| VernacRedirect (_, (_,c))
| VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
| VernacExpr _ -> false
@@ -53,17 +53,6 @@ let is_debug cmd = match under_control cmd with
| VernacSetOption (["Ltac";"Debug"], _) -> true
| _ -> false
-let is_query cmd = match under_control cmd with
- | VernacChdir None
- | VernacMemOption _
- | VernacPrintOption _
- | VernacCheckMayEval _
- | VernacGlobalCheck _
- | VernacPrint _
- | VernacSearch _
- | VernacLocate _ -> true
- | _ -> false
-
let is_undo cmd = match under_control cmd with
| VernacUndo _ | VernacUndoTo _ -> true
| _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index eb7c7055a..df739f96a 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -21,6 +21,6 @@ val has_Fail : vernac_control -> bool
val is_navigation_vernac : vernac_control -> bool
val is_deep_navigation_vernac : vernac_control -> bool
val is_reset : vernac_control -> bool
-val is_query : vernac_control -> bool
val is_debug : vernac_control -> bool
val is_undo : vernac_control -> bool
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 15:00:27 +0000