diff options
40 files changed, 592 insertions, 175 deletions
@@ -41,6 +41,12 @@ Tactics Heap, which performs a major garbage collection and heap compaction in the OCaml run-time system. +Focusing + +- Focusing bracket `{` now supports single-numbered goal selector, + e.g. `2: {` will focus on the second sub-goal. As usual, unfocus + with `}` once the sub-goal is fully solved. + Vernacular Commands - The deprecated Coercion Local, Open Local Scope, Notation Local syntax @@ -240,19 +240,6 @@ package "stm" ( ) -package "ltac" ( - - description = "Coq LTAC Plugin" - version = "8.7" - - requires = "coq.stm" - directory = "plugins/ltac" - - archive(byte) = "ltac_plugin.cmo" - archive(native) = "ltac_plugin.cmx" - -) - package "toplevel" ( description = "Coq Toplevel" @@ -293,3 +280,300 @@ package "ide" ( archive(native) = "ide.cmxa" ) + +package "plugins" ( + + description = "Coq built-in plugins" + version = "8.7" + + directory = "plugins" + + package "ltac" ( + + description = "Coq LTAC Plugin" + version = "8.7" + + requires = "coq.stm" + directory = "ltac" + + archive(byte) = "ltac_plugin.cmo" + archive(native) = "ltac_plugin.cmx" + + ) + + package "tauto" ( + + description = "Coq tauto plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "ltac" + + archive(byte) = "tauto_plugin.cmo" + archive(native) = "tauto_plugin.cmx" + ) + + package "omega" ( + + description = "Coq omega plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "omega" + + archive(byte) = "omega_plugin.cmo" + archive(native) = "omega_plugin.cmx" + ) + + package "romega" ( + + description = "Coq romega plugin" + version = "8.7" + + requires = "coq.plugins.omega" + directory = "romega" + + archive(byte) = "romega_plugin.cmo" + archive(native) = "romega_plugin.cmx" + ) + + package "micromega" ( + + description = "Coq micromega plugin" + version = "8.7" + + requires = "num,coq.plugins.ltac" + directory = "micromega" + + archive(byte) = "micromega_plugin.cmo" + archive(native) = "micromega_plugin.cmx" + ) + + package "quote" ( + + description = "Coq quote plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "quote" + + archive(byte) = "quote_plugin.cmo" + archive(native) = "quote_plugin.cmx" + ) + + package "newring" ( + + description = "Coq newring plugin" + version = "8.7" + + requires = "coq.plugins.quote" + directory = "setoid_ring" + + archive(byte) = "newring_plugin.cmo" + archive(native) = "newring_plugin.cmx" + ) + + package "fourier" ( + + description = "Coq fourier plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "fourier" + + archive(byte) = "fourier_plugin.cmo" + archive(native) = "fourier_plugin.cmx" + ) + + package "extraction" ( + + description = "Coq extraction plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "extraction" + + archive(byte) = "extraction_plugin.cmo" + archive(native) = "extraction_plugin.cmx" + ) + + package "cc" ( + + description = "Coq cc plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "cc" + + archive(byte) = "cc_plugin.cmo" + archive(native) = "cc_plugin.cmx" + ) + + package "ground" ( + + description = "Coq ground plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "firstorder" + + archive(byte) = "ground_plugin.cmo" + archive(native) = "ground_plugin.cmx" + ) + + package "rtauto" ( + + description = "Coq rtauto plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "rtauto" + + archive(byte) = "rtauto_plugin.cmo" + archive(native) = "rtauto_plugin.cmx" + ) + + package "btauto" ( + + description = "Coq btauto plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "btauto" + + archive(byte) = "btauto_plugin.cmo" + archive(native) = "btauto_plugin.cmx" + ) + + package "recdef" ( + + description = "Coq recdef plugin" + version = "8.7" + + requires = "coq.plugins.extraction" + directory = "funind" + + archive(byte) = "recdef_plugin.cmo" + archive(native) = "recdef_plugin.cmx" + ) + + package "nsatz" ( + + description = "Coq nsatz plugin" + version = "8.7" + + requires = "num,coq.plugins.ltac" + directory = "nsatz" + + archive(byte) = "nsatz_plugin.cmo" + archive(native) = "nsatz_plugin.cmx" + ) + + package "natsyntax" ( + + description = "Coq natsyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "nat_syntax_plugin.cmo" + archive(native) = "nat_syntax_plugin.cmx" + ) + + package "zsyntax" ( + + description = "Coq zsyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "z_syntax_plugin.cmo" + archive(native) = "z_syntax_plugin.cmx" + ) + + package "rsyntax" ( + + description = "Coq rsyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "r_syntax_plugin.cmo" + archive(native) = "r_syntax_plugin.cmx" + ) + + package "int31syntax" ( + + description = "Coq int31syntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "int31_syntax_plugin.cmo" + archive(native) = "int31_syntax_plugin.cmx" + ) + + package "asciisyntax" ( + + description = "Coq asciisyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "ascii_syntax_plugin.cmo" + archive(native) = "ascii_syntax_plugin.cmx" + ) + + package "stringsyntax" ( + + description = "Coq stringsyntax plugin" + version = "8.7" + + requires = "coq.plugins.asciisyntax" + directory = "syntax" + + archive(byte) = "string_syntax_plugin.cmo" + archive(native) = "string_syntax_plugin.cmx" + ) + + package "derive" ( + + description = "Coq derive plugin" + version = "8.7" + + requires = "" + directory = "derive" + + archive(byte) = "derive_plugin.cmo" + archive(native) = "derive_plugin.cmx" + ) + + package "ssrmatching" ( + + description = "Coq ssrmatching plugin" + version = "8.7" + + requires = "coq.plugins.ltac" + directory = "ssrmatching" + + archive(byte) = "ssrmatching_plugin.cmo" + archive(native) = "ssrmatching_plugin.cmx" + ) + + package "ssreflect" ( + + description = "Coq ssreflect plugin" + version = "8.7" + + requires = "coq.plugins.ssrmatching" + directory = "ssr" + + archive(byte) = "ssreflect_plugin.cmo" + archive(native) = "ssreflect_plugin.cmx" + ) +) diff --git a/Makefile.checker b/Makefile.checker index 8334b6a2a..0e429fe86 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -77,9 +77,8 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \ - if grep -q "$$v" checker/values.ml; \ - then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi + $(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml" >&2; false; fi .PHONY: md5chk diff --git a/checker/cic.mli b/checker/cic.mli index 4a0e706aa..95dd18f5f 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -170,6 +170,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet type engagement = set_predicativity +(** {6 Conversion oracle} *) + +type level = Expand | Level of int | Opaque + +type oracle = { + var_opacity : level Id.Map.t; + cst_opacity : level Cmap.t; + var_trstate : Id.Pred.t; + cst_trstate : Cpred.t; +} + (** {6 Representation of constants (Definition/Axiom) } *) @@ -219,6 +230,7 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : oracle; (** Unfolding strategies for conversion *) } type constant_body = { diff --git a/checker/closure.ml b/checker/closure.ml index 3a56bba01..98f8c4a82 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -822,6 +822,7 @@ type clos_infos = fconstr infos let infos_env x = x.i_env let infos_flags x = x.i_flags +let oracle_of_infos x = x.i_env.env_conv_oracle let create_clos_infos flgs env = create (fun _ -> inject) flgs env diff --git a/checker/closure.mli b/checker/closure.mli index 02d8b22fa..ce8c64e30 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -147,6 +147,8 @@ type clos_infos val create_clos_infos : reds -> env -> clos_infos val infos_env : clos_infos -> env val infos_flags : clos_infos -> reds +val oracle_of_infos : clos_infos -> oracle + (* Reduction function *) diff --git a/checker/environ.ml b/checker/environ.ml index 9db0d60e8..3830cd0dc 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -21,7 +21,15 @@ type env = { env_globals : globals; env_rel_context : rel_context; env_stratification : stratification; - env_imports : Cic.vodigest MPmap.t } + env_imports : Cic.vodigest MPmap.t; + env_conv_oracle : oracle; } + +let empty_oracle = { + var_opacity = Id.Map.empty; + cst_opacity = Cmap.empty; + var_trstate = Id.Pred.empty; + cst_trstate = Cpred.empty; +} let empty_env = { env_globals = @@ -34,7 +42,8 @@ let empty_env = { env_stratification = { env_universes = Univ.initial_universes; env_engagement = PredicativeSet }; - env_imports = MPmap.empty } + env_imports = MPmap.empty; + env_conv_oracle = empty_oracle } let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes @@ -51,6 +60,8 @@ let set_engagement (impr_set as c) env = { env with env_stratification = { env.env_stratification with env_engagement = c } } +let set_oracle env oracle = { env with env_conv_oracle = oracle } + (* Digests *) let add_digest env dp digest = diff --git a/checker/environ.mli b/checker/environ.mli index 6bda838f8..ba62ed519 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -18,6 +18,7 @@ type env = { env_rel_context : rel_context; env_stratification : stratification; env_imports : Cic.vodigest MPmap.t; + env_conv_oracle : Cic.oracle; } val empty_env : env @@ -25,6 +26,10 @@ val empty_env : env val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env +(** Oracle *) + +val set_oracle : env -> Cic.oracle -> env + (* Digests *) val add_digest : env -> DirPath.t -> Cic.vodigest -> env val lookup_digest : env -> DirPath.t -> Cic.vodigest diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 22c843812..bb0db8cfe 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -586,6 +586,8 @@ let check_inductive env kn mib = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in let env = Environ.push_context ind_ctx env in + (** Locally set the oracle for further typechecking *) + let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) @@ -593,13 +595,13 @@ let check_inductive env kn mib = user_err Pp.(str "not the right number of packets"); (* check mind_params_ctxt *) let params = mib.mind_params_ctxt in - let _ = check_ctxt env params in + let _ = check_ctxt env0 params in (* check mind_nparams *) if rel_context_nhyps params <> mib.mind_nparams then user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) - let env_ar = typecheck_arity env params mib.mind_packets in + let env_ar = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; (* check the inferred subtyping relation *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 4357a690e..7685863ea 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,6 +26,9 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); + (** Locally set the oracle for further typechecking *) + let oracle = env.env_conv_oracle in + let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with @@ -53,8 +56,12 @@ let check_constant_declaration env kn cb = conv_leq envty j ty) | None -> () in - if constant_is_polymorphic cb then add_constant kn cb env - else add_constant kn cb env' + let env = + if constant_is_polymorphic cb then add_constant kn cb env + else add_constant kn cb env' + in + (** Reset the value of the oracle *) + Environ.set_oracle env oracle (** {6 Checking modules } *) diff --git a/checker/reduction.ml b/checker/reduction.ml index 9b8eac04c..d4b258f58 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -276,11 +276,29 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false -let oracle_order fl1 fl2 = - match fl1,fl2 with - ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false - | _, ConstKey _ -> true - | _ -> false +let default_level = Level 0 + +let get_strategy { var_opacity; cst_opacity } = function + | VarKey id -> + (try Names.Id.Map.find id var_opacity + with Not_found -> default_level) + | ConstKey (c, _) -> + (try Names.Cmap.find c cst_opacity + with Not_found -> default_level) + | RelKey _ -> Expand + +let oracle_order infos l2r k1 k2 = + let o = Closure.oracle_of_infos infos in + match get_strategy o k1, get_strategy o k2 with + | Expand, Expand -> l2r + | Expand, (Opaque | Level _) -> true + | (Opaque | Level _), Expand -> false + | Opaque, Opaque -> l2r + | Level _, Opaque -> true + | Opaque, Level _ -> false + | Level n1, Level n2 -> + if Int.equal n1 n2 then l2r + else n1 < n2 let unfold_projection infos p c = let pb = lookup_projection p (infos_env infos) in @@ -339,7 +357,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = with NotConvertible -> (* else the oracle tells which constant is to be expanded *) let (app1,app2) = - if oracle_order fl1 fl2 then + if oracle_order infos false fl1 fl2 then match unfold_reference infos fl1 with | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) | None -> diff --git a/checker/values.ml b/checker/values.ml index 4698227ff..313067cb6 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli +MD5 483493b20fe91cc1bea4350a2db2f82d checker/cic.mli *) @@ -70,6 +70,8 @@ let v_map vk vd = let v_hset v = v_map Int (v_set v) let v_hmap vk vd = v_map Int (v_map vk vd) +let v_pred v = v_pair v_bool (v_set v) + (* lib/future *) let v_computation f = Annot ("Future.computation", @@ -199,6 +201,17 @@ let v_lazy_constr = let v_impredicative_set = v_enum "impr-set" 2 let v_engagement = v_impredicative_set +let v_conv_level = + v_sum "conv_level" 2 [|[|Int|]|] + +let v_oracle = + v_tuple "oracle" [| + v_map v_id v_conv_level; + v_hmap v_cst v_conv_level; + v_pred v_id; + v_pred v_cst; + |] + let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -213,7 +226,7 @@ let v_projbody = v_constr|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/configure.ml b/configure.ml index 67197e670..b5de5e3e1 100644 --- a/configure.ml +++ b/configure.ml @@ -863,13 +863,6 @@ let strip = if strip = "" then "strip" else strip end -(** * md5sum command *) - -let md5sum = - select_command "Don’t know how to compute MD5 checksums…" [ - "md5sum", [], [ "--version" ]; - "md5", ["-q"], [ "-s" ; "''" ]; - ] (** * Documentation : do we have latex, hevea, ... *) @@ -1248,8 +1241,6 @@ let write_makefile f = pr "# Unix systems and profiling: true\n"; pr "# Unix systems and no profiling: strip\n"; pr "STRIP=%s\n\n" strip; - pr "#the command md5sum\n"; - pr "MD5SUM=%s\n\n" md5sum; pr "# LablGTK\n"; pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes; pr "# CoqIde (no/byte/opt)\n"; diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 3850c05fd..3cbccab44 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,7 +17,7 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ -I $CAMLP4LIB -I +threads \ -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ + -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 3d4c885b3..6b24fdde7 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -320,10 +320,19 @@ Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or {\tt \}} to unfocus it or focus the next one. +\begin{Variants} + +\item {\tt {\num}: \{}\\ +This focuses on the $\num^{th}$ subgoal to prove. + +\end{Variants} + \begin{ErrMsgs} \item \errindex{This proof is focused, but cannot be unfocused this way} You are trying to use {\tt \}} but the current subproof has not been fully solved. +\item \errindex{No such goal} +\item \errindex{Brackets only support the single numbered goal selector} \item see also error message about bullets below. \end{ErrMsgs} diff --git a/engine/uState.ml b/engine/uState.ml index 6f2b3c4b2..4b650c9c9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -201,14 +201,18 @@ let process_universe_constraints ctx cstrs = | None -> user_err Pp.(str "Algebraic universe on the right") | Some r' -> if Univ.Level.is_small r' then - let levels = Univ.Universe.levels l in - let fold l' local = - let l = Univ.Universe.make l' in - if Univ.Level.is_small l' || is_local l' then - equalize_variables false l l' r r' local - else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) - in - Univ.LSet.fold fold levels local + if not (Univ.Universe.is_levels l) + then + raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + else + let levels = Univ.Universe.levels l in + let fold l' local = + let l = Univ.Universe.make l' in + if Univ.Level.is_small l' || is_local l' then + equalize_variables false l l' r r' local + else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + in + Univ.LSet.fold fold levels local else Univ.enforce_leq l r local end diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 8bfd937e3..a7e9003db 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -17,7 +17,9 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) -let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+ +let number = [ '0'-'9' ]+ + +let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ let dot_sep = '.' (space | eof) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5106e513b..8bd2da2f1 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -314,7 +314,16 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) -type vernac_expr = +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string Loc.located option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = | VernacLoad of verbose_flag * string (* Syntax *) @@ -451,7 +460,7 @@ type vernac_expr = | VernacUnfocus | VernacUnfocused | VernacBullet of bullet - | VernacSubproof of int option + | VernacSubproof of goal_selector option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard @@ -463,22 +472,13 @@ type vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list - (* Flags *) - | VernacProgram of vernac_expr - | VernacPolymorphic of bool * vernac_expr - | VernacLocal of bool * vernac_expr - -and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit - -and vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string Loc.located option; - implicit_status : vernac_implicit_status; -} +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool type vernac_control = - | VernacExpr of vernac_expr + | VernacExpr of vernac_flag list * vernac_expr (* 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 diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7f4b85fd0..5b9e1a141 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -74,6 +74,7 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d8768a0fc..9eed9efcb 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -15,9 +15,10 @@ module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) -let safe_flags = { +let safe_flags oracle = { check_guarded = true; check_universes = true; + conv_oracle = oracle; } (** {6 Arities } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 198831848..0eed11f49 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -67,7 +67,7 @@ val inductive_is_cumulative : mutual_inductive_body -> bool (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) -val safe_flags : typing_flags +val safe_flags : Conv_oracle.oracle -> typing_flags (** {6 Hash-consing} *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 1afab453a..3c86129fe 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -37,8 +37,10 @@ type env = Pre_env.env let pre_env env = env let env_of_pre_env env = env -let oracle env = env.env_conv_oracle -let set_oracle env o = { env with env_conv_oracle = o } +let oracle env = env.env_typing_flags.conv_oracle +let set_oracle env o = + let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in + { env with env_typing_flags } let empty_named_context_val = empty_named_context_val diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index c5254b453..4ef89f8c0 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -75,7 +75,6 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; - env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; } @@ -98,8 +97,7 @@ let empty_env = { env_stratification = { env_universes = UGraph.initial_universes; env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags; - env_conv_oracle = Conv_oracle.empty; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; indirect_pterms = Opaqueproof.empty_opaquetab } diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 054ae1743..fef530c87 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -53,7 +53,6 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; - env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; } diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 92e60f465..d498bda34 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -72,36 +72,36 @@ GEXTEND Gram | 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 - | v = vernac -> VernacExpr(v) ] + | (f, v) = vernac -> VernacExpr(f, v) ] ] ; vernac: - [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) - | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) + [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v) + | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v) | v = vernac_poly -> v ] ] ; vernac_poly: - [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) - | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v) + | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v) | v = vernac_aux -> v ] ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> VernacProgram g - | IDENT "Program"; g = gallina_ext; "." -> VernacProgram g - | g = gallina; "." -> g - | g = gallina_ext; "." -> g - | c = command; "." -> c - | c = syntax; "." -> c - | c = subprf -> c + [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g) + | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g) + | g = gallina; "." -> ([], g) + | g = gallina_ext; "." -> ([], g) + | c = command; "." -> ([], c) + | c = syntax; "." -> ([], c) + | c = subprf -> ([], c) ] ] ; vernac_aux: LAST - [ [ prfcom = command_entry -> prfcom ] ] + [ [ prfcom = command_entry -> ([], prfcom) ] ] ; noedit_mode: [ [ c = query_command -> c None] ] @@ -621,11 +621,9 @@ GEXTEND Gram VernacCanonical (AN qid) | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> VernacCanonical (ByNotation ntn) - | IDENT "Canonical"; IDENT "Structure"; qid = global; - d = def_body -> + | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacLocal(false, - VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d)) + VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 2fd6f53c4..4b828a702 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b4e17c5d1..0b929b8ca 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ebf6e450b..cc7ce339b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -327,7 +327,8 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g + | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 4f530a0ae..c0479dd24 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -551,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d ))) + ((Loc.tag s),None), d) ]]; END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1..96e39e89a 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -91,7 +91,7 @@ open Decl_kinds let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." @@ -535,17 +535,25 @@ open Decl_kinds | SsFwdClose e -> "("^aux e^")*" in Pp.str (aux e) - let rec pr_vernac_expr v = + let pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in + try + let rl = Egramml.get_extend_vernac_rule s in + let rec aux rl cl = + match rl, cl with + | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl + | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | [], [] -> [] + | _ -> assert false in + hov 1 (pr_sequence identity (aux rl cl)) + with Not_found -> + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + + let pr_vernac_expr v = let return = tag_vernac v in match v with - | VernacPolymorphic (poly, v) -> - let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac_expr v) - | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_expr v) - | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_expr v) - | VernacLoad (f,s) -> return ( keyword "Load" @@ -1199,30 +1207,25 @@ open Decl_kinds | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") - and pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in - try - let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = - match rl, cl with - | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl - | [], [] -> [] - | _ -> assert false in - hov 1 (pr_sequence identity (aux rl cl)) - with Not_found -> - hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") +let pr_vernac_flag = + function + | VernacPolymorphic true -> keyword "Polymorphic" + | VernacPolymorphic false -> keyword "Monomorphic" + | VernacProgram -> keyword "Program" + | VernacLocal local -> pr_locality local let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v' + | VernacExpr (f, v') -> + List.fold_right + (fun f a -> pr_vernac_flag f ++ spc() ++ a) + f + (pr_vernac_expr v' ++ sep_end v') | VernacTime (_,(_,v)) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, (_,v)) -> diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b5b9a01..bebc4d5d5 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -96,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b))) + recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) } | `Not -> `Leaks @@ -125,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof) + recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) } | `Not -> `Leaks diff --git a/stm/stm.ml b/stm/stm.ml index 7045df0ed..5f4fe6565 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1498,7 +1498,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1646,7 +1646,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> @@ -2177,7 +2177,7 @@ let collect_proof keep cur hd brkind id = (try let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in - v.expr <- VernacExpr(VernacProof(t, Some hint)); + v.expr <- VernacExpr([], VernacProof(t, Some hint)); `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2872,10 +2872,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let rec opacity_of_produced_term = function + let opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity - | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2fa47ba43..99b56d484 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -49,17 +49,13 @@ let declare_vernac_classifier classifiers := !classifiers @ [s,f] let classify_vernac e = - let rec static_classifier ~poly e = match e with + let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | ( VernacSetOption (l,_) | VernacUnsetOption l) when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> VtSideff [], VtNow - (* Nested vernac exprs *) - | VernacProgram e -> static_classifier ~poly e - | VernacLocal (_,e) -> static_classifier ~poly e - | VernacPolymorphic (b, e) -> static_classifier ~poly:b e (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater @@ -193,7 +189,13 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function - | VernacExpr e -> static_classifier ~poly e + | VernacExpr (f, e) -> + let poly = List.fold_left (fun poly f -> + match f with + | VernacPolymorphic b -> b + | (VernacProgram | VernacLocal _) -> poly + ) poly f in + static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) -> static_control_classifier ~poly e diff --git a/test-suite/bugs/closed/6297.v b/test-suite/bugs/closed/6297.v new file mode 100644 index 000000000..a28607058 --- /dev/null +++ b/test-suite/bugs/closed/6297.v @@ -0,0 +1,8 @@ +Set Printing Universes. + +(* Error: Anomaly "Uncaught exception "Anomaly: Incorrect universe Set + declared for inductive type, inferred level is max(Prop, Set+1)."." + Please report at http://coq.inria.fr/bugs/. *) +Fail Record LTS: Set := + lts { St: Set; + init: St }. diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v new file mode 100644 index 000000000..ed035f521 --- /dev/null +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -0,0 +1,16 @@ +Goal forall A B, B \/ A -> A \/ B. +Proof. + intros * [HB | HA]. + 2: { + left. + exact HA. + Fail right. (* No such goal. Try unfocusing with "}". *) + } + Fail 2: { (* Non-existent goal. *) + idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *) + 1:{ (* Syntactic test: no space before bracket. *) + right. + exact HB. +Fail Qed. + } +Qed. diff --git a/tools/md5sum.ml b/tools/md5sum.ml new file mode 100644 index 000000000..2fdcacc83 --- /dev/null +++ b/tools/md5sum.ml @@ -0,0 +1,24 @@ +let get_content file = + let ic = open_in_bin file in + let buf = Buffer.create 2048 in + let rec fill () = + match input_char ic with + | '\r' -> fill () (* NOTE: handles the case on Windows where the + git checkout has included return characters. + See: https://github.com/coq/coq/pull/6305 *) + | c -> Buffer.add_char buf c; fill () + | exception End_of_file -> close_in ic; Buffer.contents buf + in + fill () + +let () = + match Sys.argv with + | [|_; file|] -> + let content = get_content file in + let md5 = Digest.to_hex (Digest.string content) in + print_string (md5 ^ " " ^ file) + | _ -> + prerr_endline "Error: This program needs exactly one parameter."; + prerr_endline "Usage: ocaml md5sum.ml <FILE>"; + prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r."; + exit 1 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ded0d97e6..3358951f4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1846,11 +1846,8 @@ let vernac_unfocused () = user_err Pp.(str "The proof is not fully unfocused.") -(* BeginSubproof / EndSubproof. - BeginSubproof (vernac_subproof) focuses on the first goal, or the goal - given as argument. - EndSubproof (vernac_end_subproof) unfocuses from a BeginSubproof, provided - that the proof of the goal has been completed. +(* "{" focuses on the first goal, "n: {" focuses on the n-th goal + "}" unfocuses, provided that the proof of the goal has been completed. *) let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind @@ -1859,7 +1856,9 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some n -> Proof.focus subproof_cond () n p) + | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | _ -> user_err ~hdr:"bracket_selector" + (str "Brackets only support the single numbered goal selector.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> @@ -1959,11 +1958,6 @@ let interp ?proof ~atts ~st c = (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - (* Handled elsewhere *) - | VernacProgram _ - | VernacPolymorphic _ - | VernacLocal _ -> assert false - (* Syntax *) | VernacSyntaxExtension (infix, sl) -> vernac_syntax_extension atts infix sl @@ -2200,10 +2194,30 @@ let with_fail st b f = 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 flags f atts = + List.fold_left + (fun (polymorphism, atts) f -> + match f with + | VernacProgram when not atts.program -> + (polymorphism, { atts with program = true }) + | VernacProgram -> + user_err Pp.(str "Program mode specified twice") + | VernacPolymorphic b when polymorphism = None -> + (Some b, atts) + | VernacPolymorphic _ -> + user_err Pp.(str "Polymorphism specified twice") + | VernacLocal b when Option.is_empty atts.locality -> + (polymorphism, { atts with locality = Some b }) + | VernacLocal _ -> + user_err Pp.(str "Locality specified twice") + ) + (None, atts) + f + in let rec control = function - | VernacExpr v -> - let atts = { loc; locality = None; polymorphic = false; } in - aux ~atts orig_program_mode v + | VernacExpr (f, v) -> + let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> current_timeout := Some n; @@ -2213,25 +2227,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacTime (batch, (_loc,v)) -> System.with_time ~batch control v; - and aux ?polymorphism ~atts isprogcmd = function - - | VernacProgram c when not isprogcmd -> - aux ?polymorphism ~atts true c - - | VernacProgram _ -> - user_err Pp.(str "Program mode specified twice") - - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ~polymorphism:b ~atts:atts isprogcmd c - - | VernacPolymorphic (b, c) -> - user_err Pp.(str "Polymorphism specified twice") - - | VernacLocal (b, c) when Option.is_empty atts.locality -> - aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c - - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") + and aux ~polymorphism ~atts : _ -> unit = + function | VernacLoad (_,fname) -> vernac_load control fname @@ -2240,7 +2237,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = check_vernac_supports_polymorphism c polymorphism; let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in Flags.make_universe_polymorphism polymorphic; - Obligations.set_program_mode isprogcmd; + Obligations.set_program_mode atts.program; try vernac_timeout begin fun () -> let atts = { atts with polymorphic } in @@ -2249,7 +2246,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,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 + if orig_program_mode || not !Flags.program_mode || atts.program then Flags.program_mode := orig_program_mode; if (Flags.is_universe_polymorphism() = polymorphic) then Flags.make_universe_polymorphism orig_univ_poly; diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index c0b93c163..c40ca27db 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -16,6 +16,7 @@ type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; + program : bool; } type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index ab3d4bfc5..c5e610f89 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -14,6 +14,7 @@ type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; + program : bool; } type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 4fdc78dd2..3932d1c7b 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -12,14 +12,14 @@ open Vernacexpr let rec under_control = function - | VernacExpr c -> c + | VernacExpr (_, c) -> c | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function - | VernacExpr c -> false + | VernacExpr _ -> false | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacTimeout (_,c) -> has_Fail c @@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function (* NB: Reset is now allowed again as asked by A. Chlipala *) let is_reset = function - | VernacExpr VernacResetInitial - | VernacExpr (VernacResetName _) -> true + | VernacExpr ( _, VernacResetInitial) + | VernacExpr (_, VernacResetName _) -> true | _ -> false let is_debug cmd = match under_control cmd with |