diff options
36 files changed, 181 insertions, 76 deletions
@@ -2,6 +2,8 @@ FLG -rectypes -thread S config B config +S ide +B ide S lib B lib S intf @@ -1130,7 +1130,7 @@ Extraction instead of accessing their body, they are now considered as axioms. The previous behaviour can be reactivated via the option "Set Extraction AccessOpaque". -- The pretty-printer for Haskell now produces layout-independant code +- The pretty-printer for Haskell now produces layout-independent code - A new command "Separate Extraction cst1 cst2 ..." that mixes a minimal extracted environment a la "Recursive Extraction" and the production of several files (one per coq source) a la "Extraction Library" @@ -1815,7 +1815,7 @@ Tactics Moreover, romega now has a variant "romega with *" that can be also used on non-Z goals (nat, N, positive) via a call to a translation tactic named zify (its purpose is to Z-ify your goal...). This zify may also be used - independantly of romega. + independently of romega. - Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an diff --git a/config/coq_config.mli b/config/coq_config.mli index 6087c01169..c171bd3553 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -32,7 +32,7 @@ val cflags : string (* arguments passed to gcc *) val best : string (* byte/opt *) val arch : string (* architecture *) val arch_is_win32 : bool -val osdeplibs : string (* OS dependant link options for ocamlc *) +val osdeplibs : string (* OS dependent link options for ocamlc *) val vmbyteflags : string list (* -custom/-dllib -lcoqrun *) @@ -51,7 +51,7 @@ val exec_extension : string (* "" under Unix, ".exe" under MS-windows *) val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *) val browser : string -(** default web browser to use, may be overriden by environment +(** default web browser to use, may be overridden by environment variable COQREMOTEBROWSER *) val has_coqide : string diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion index 6274275c9d..a81f170c63 100644 --- a/dev/doc/notes-on-conversion +++ b/dev/doc/notes-on-conversion @@ -21,7 +21,7 @@ Notation OMEGA := (ack 4 4). Definition f (x:nat) := x. -(* Evaluation in tactics can somehow be controled *) +(* Evaluation in tactics can somehow be controlled *) Lemma l1 : OMEGA = OMEGA. reflexivity. (* succeed: identity *) Qed. (* succeed: identity *) diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index 6ec4dc1af0..1c415eca69 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -61,6 +61,7 @@ <li>V8.3 © INRIA 2010-2011</li> <li>V8.4 © INRIA 2012-2014</li> <li>V8.5 © INRIA 2015-2016</li> + <li>V8.6 © INRIA 2016</li> </ul> <p style="text-indent:0pt">This research was partly supported by IST diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index 328bd68daf..25fb56320b 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -39,6 +39,7 @@ <li>V8.3 © INRIA 2010-2011</li> <li>V8.4 © INRIA 2012-2014</li> <li>V8.5 © INRIA 2015-2016</li> + <li>V8.6 © INRIA 2016</li> </ul> <p style="text-indent:0pt">This research was partly supported by IST diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 48b61827d1..213fb03137 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2587,8 +2587,8 @@ It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots} \Question{What is a dependent type?} -A dependant type is a type which depends on some term. For instance -``vector of size n'' is a dependant type representing all the vectors +A dependent type is a type which depends on some term. For instance +``vector of size n'' is a dependent type representing all the vectors of size $n$. Its type depends on $n$ \Question{What is a proof by reflection?} diff --git a/ide/.merlin b/ide/.merlin index 3f3d9d275d..953b5dce4c 100644 --- a/ide/.merlin +++ b/ide/.merlin @@ -1,4 +1,4 @@ -PKG lablgtk2.sourceview2 +PKG unix laglgtk2 lablgtk2.sourceview2 S utils B utils diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index dbcd8630b1..680da7f54b 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -724,6 +724,9 @@ let rec tmpp v loc = | VernacComments (cl) -> xmlComment loc (List.flatten (List.map pp_comment cl)) + (* Stm backdoor *) + | VernacStm _ as x -> xmlTODO loc x + (* Proof management *) | VernacGoal _ as x -> xmlTODO loc x | VernacAbort _ as x -> xmlTODO loc x diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml index 9f44e5c6be..e9b19da621 100644 --- a/ide/utils/configwin_keys.ml +++ b/ide/utils/configwin_keys.ml @@ -154,7 +154,7 @@ let xk_KP_9 = 0xFFB9 (* - * Auxilliary Functions; note the duplicate definitions for left and right + * Auxiliary Functions; note the duplicate definitions for left and right * function keys; Sun keyboards and a few other manufactures have such * function key groups on the left and/or right sides of the keyboard. * We've not found a keyboard with more than 35 function keys total. diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f77a940a7e..92e4dd618e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,6 +283,16 @@ type bullet = | Star of int | Plus of int +(** {6 Types concerning Stm} *) +type 'a stm_vernac = + | JoinDocument + | Finish + | Wait + | PrintDag + | Observe of Stateid.t + | Command of 'a (* An out of flow command not to be recorded by Stm *) + | PGLast of 'a (* To ease the life of PG *) + (** {6 Types concerning the module layer} *) (** Rigid / flexible module signature *) @@ -441,6 +451,9 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list + (* Stm backdoor *) + | VernacStm of vernac_expr stm_vernac + (* Proof management *) | VernacGoal of constr_expr | VernacAbort of lident option @@ -495,7 +508,7 @@ type vernac_type = | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with - | VtBack of Stateid.t * vernac_part_of_script + | VtStm of vernac_control * vernac_part_of_script | VtUnknown and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) @@ -503,6 +516,14 @@ and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list and vernac_is_alias = bool and vernac_part_of_script = bool +and vernac_control = + | VtFinish + | VtWait + | VtJoinDocument + | VtPrintDag + | VtObserve of Stateid.t + | VtBack of Stateid.t + | VtPG and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 792a311fcf..47df22807f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,7 +23,7 @@ #include "coq_values.h" /* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)val >> 1)) +#define uint32_of_value(val) ((uint32_t)(val) >> 1) #define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1)) #define UI64_of_uint32(lo) ((uint64_t)(lo)) #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) @@ -1206,7 +1206,7 @@ value coq_interprete Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ /*unsigned shift*/ Field(accu, 0) = (value)((p >> 31)|1) ; /*higher part*/ - Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/ + Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/ } Next; } diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c6c7b42429..0f0f09aa23 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,6 +17,10 @@ let version = 1 let oc = ref None +let chop_extension f = + if check_suffix f ".v" then chop_extension f + else f + let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" diff --git a/lib/profile.ml b/lib/profile.ml index 0910db3fe2..d620fe69c4 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = number of allocated bytes may exceed the maximum integer capacity (2^31 on 32-bits architectures); therefore, allocation is measured by small steps, total allocations are computed by adding elementary - measures and carries are controled from step to step *) + measures and carries are controlled from step to step *) -(* Unix measure of time is approximative and shoitt delays are often +(* Unix measure of time is approximate and short delays are often unperceivable; therefore, total times are measured in one (big) step to avoid rounding errors and to get the best possible approximation. @@ -358,7 +358,7 @@ let declare_profile name = prof_table := (name,e)::!prof_table; e -(* Default initialisation, may be overriden *) +(* Default initialization, may be overridden *) let _ = init_profile () (******************************) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4ba9eeefa9..e61be53a99 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -64,6 +64,16 @@ GEXTEND Gram | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) + (* Stm backdoor *) + | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument + | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish + | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait + | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag + | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> + VernacStm (Observe (Stateid.of_int (int_of_string id))) + | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) + | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) + | v = vernac_poly -> v ] ] ; @@ -572,9 +582,9 @@ let warn_deprecated_implicit_arguments = let warn_deprecated_arguments_syntax = CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated" - (fun () -> strbrk "The \"/\" modifier has an effect only in the first " - ++ strbrk "arguments list. The syntax allowing it to appear" - ++ strbrk " in other lists is deprecated.") + (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only " + ++ strbrk "in the first arguments list. The syntax allowing" + ++ strbrk " them to appear in other lists is deprecated.") (* Extensions: implicits, coercions, etc. *) GEXTEND Gram @@ -654,8 +664,8 @@ GEXTEND Gram more_implicits = OPT [ ","; impl = LIST1 [ impl = LIST0 more_implicits_block -> - let warn_slash = List.exists fst impl in - if warn_slash then warn_deprecated_arguments_syntax ~loc:!@loc (); + let warn_deprecated = List.exists fst impl in + if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc (); List.flatten (List.map snd impl)] SEP "," -> impl ]; @@ -766,14 +776,19 @@ GEXTEND Gram implicit_status = MaximallyImplicit}) items ] ]; + name_or_bang: [ + [ b = OPT "!"; id = name -> + not (Option.is_empty b), id + ] + ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)]) + [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)]) | "/" -> (true (* Should warn about deprecated syntax *), []) - | "["; items = LIST1 name; "]" -> - (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items) - | "{"; items = LIST1 name; "}" -> - (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items) + | "["; items = LIST1 name_or_bang; "]" -> + (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items) + | "{"; items = LIST1 name_or_bang; "}" -> + (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items) ] ]; strategy_level: diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ec8dac8210..37165f6ceb 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -39,7 +39,7 @@ module Gram : module type of Compat.GrammarMake(CLexer) | (together with a constr entry level, e.g. 50, and indications of) | (subentries, e.g. x in constr next level and y constr same level) | - | spliting into tokens by Metasyntax.split_notation_string + | splitting into tokens by Metasyntax.split_notation_string V [String "x"; String "+"; String "y"] : symbol_token list | @@ -96,7 +96,7 @@ module Gram : module type of Compat.GrammarMake(CLexer) *) -(** Temporary activate camlp4 verbosity *) +(** Temporarily activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -232,14 +232,14 @@ type gram_reinit = gram_assoc * gram_position val grammar_extend : 'a Gram.entry -> gram_reinit option -> 'a Extend.extend_statment -> unit -(** Extend the grammar of Coq, without synchronizing it with the bactracking +(** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) (** {5 Extending the parser with summary-synchronized commands} *) module GramState : Store.S -(** Auxilliary state of the grammar. Any added data must be marshallable. *) +(** Auxiliary state of the grammar. Any added data must be marshallable. *) type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a063cbbfe3..e4b58a56f9 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1517,27 +1517,27 @@ let rec apply_ids t ids = | [] -> t | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids -let coq_Node = +let coq_Node = lazy (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") -let coq_Leaf = +let coq_Leaf = lazy (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") -let coq_Empty = +let coq_Empty = lazy (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") -let coq_VarMap = +let coq_VarMap = lazy (Coqlib.gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") let rec dump_varmap typ m = match m with - | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |]) - | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|]) - | Mc.Node(l,o,r) -> - Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) + | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |]) + | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|]) + | Mc.Node(l,o,r) -> + Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) let vm_of_list env = @@ -1709,7 +1709,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); + ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl)) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 1e618b59eb..6e40e03f5b 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1216,7 +1216,7 @@ module Make | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) + str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")" in pr_tac diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a6b1c97f5c..3494ad006f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -538,6 +538,22 @@ module Make | VernacLocal (local, v) -> return (pr_locality local ++ spc() ++ pr_vernac_body v) + (* Stm *) + | VernacStm JoinDocument -> + return (keyword "Stm JoinDocument") + | VernacStm PrintDag -> + return (keyword "Stm PrintDag") + | VernacStm Finish -> + return (keyword "Stm Finish") + | VernacStm Wait -> + return (keyword "Stm Wait") + | VernacStm (Observe id) -> + return (keyword "Stm Observe " ++ str(Stateid.to_string id)) + | VernacStm (Command v) -> + return (keyword "Stm Command " ++ pr_vernac_body v) + | VernacStm (PGLast v) -> + return (keyword "Stm PGLast " ++ pr_vernac_body v) + (* Proof management *) | VernacAbortAll -> return (keyword "Abort All") diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7605f63872..e753e972da 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -617,7 +617,7 @@ module Bullet = struct let _ = register_behavior strict end - (* Current bullet behavior, controled by the option *) + (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict let _ = diff --git a/stm/stm.ml b/stm/stm.ml index 0ddaf604ad..b4331dc460 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -896,6 +896,7 @@ end = struct (* {{{ *) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in + cur_id := Stateid.dummy; VCS.reached id; let ie = match Stateid.get info, safe_id with @@ -989,7 +990,7 @@ end = struct (* {{{ *) try match v with | VernacResetInitial -> - VtBack (Stateid.initial, true), VtNow + VtStm (VtBack Stateid.initial, true), VtNow | VernacResetName (_,name) -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try @@ -997,20 +998,20 @@ end = struct (* {{{ *) fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - VtBack (oid, true), VtNow + VtStm (VtBack oid, true), VtNow with Not_found -> - VtBack (id, true), VtNow) + VtStm (VtBack id, true), VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtBack (oid, true), VtNow + VtStm (VtBack oid, true), VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,tactic,undo) -> let value = (if tactic then 1 else 0) - undo in if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in - VtBack (oid, true), VtLater + VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -1027,16 +1028,16 @@ end = struct (* {{{ *) 0 id in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in - VtBack (oid, true), VtLater + VtStm (VtBack oid, true), VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - VtBack (oid, true), VtLater + VtStm (VtBack oid, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow + VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow | _ -> VtUnknown, VtNow with | Not_found -> @@ -2428,8 +2429,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with + (* PG stuff *) + | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok + | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") + (* Joining various parts of the document *) + | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok + | VtStm (VtFinish, b), VtNow -> finish (); `Ok + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm (VtPrintDag, b), VtNow -> + VCS.print ~now:true (); `Ok + | VtStm (VtObserve id, b), VtNow -> observe id; `Ok + | VtStm ((VtObserve _ | VtFinish | VtJoinDocument + |VtPrintDag |VtWait),_), VtLater -> + anomaly(str"classifier: join actions cannot be classified as VtLater") + (* Back *) - | VtBack(oid, true), w -> + | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in let valid = VCS.get_branch_pos head in @@ -2448,12 +2463,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok - | VtBack (id, false), VtNow -> + | VtStm (VtBack id, false), VtNow -> prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok - | VtBack (id, false), VtLater -> + | VtStm (VtBack id, false), VtLater -> anomaly(str"classifier: VtBack + VtLater must imply part_of_script") (* Query *) @@ -2590,6 +2605,15 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow") end in + (* Proof General *) + begin match expr with + | VernacStm (PGLast _) -> + if not (VCS.Branch.equal head VCS.Branch.master) then + vernac_interp Stateid.dummy + { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; + expr = VernacShow (ShowGoal OpenSubgoals) } + | _ -> () + end; prerr_endline (fun () -> "processed }}}"); VCS.print (); rc @@ -2651,8 +2675,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with - | VtBack (w,_), _ -> - ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow)) + | VtStm (w,_), _ -> + ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow)) | _ -> ignore(process_transaction ~tty:false aast (VtQuery (false,report_with), VtNow))) @@ -2799,7 +2823,7 @@ let interp verb (loc,e) = let print_goals = verb && match clas with | VtQuery _, _ -> false - | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true + | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true | _ -> not !Flags.coqtop_ui in try finish ~print_goals () with e -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f9bf9653fd..dc5be08a37 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,7 +33,10 @@ let string_of_vernac_type = function | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ " route " ^ string_of_int route - | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b + | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> + "Stm " ^ string_of_in_script b + | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b + | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function | VtLater -> "Later" @@ -52,7 +55,7 @@ let declare_vernac_classifier let elide_part_of_script_and_now (a, _) = match a with | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtBack (x, _) -> VtBack (x, false), VtNow + | VtStm (x, _) -> VtStm (x, false), VtNow | x -> x, VtNow let make_polymorphic (a, b as x) = @@ -66,12 +69,23 @@ let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = let static_classifier e = match e with + (* PG compatibility *) + | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) + | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) + when !Flags.print_emacs -> VtStm(VtPG,false), VtNow (* 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 (["Universe"; "Polymorphism"],_) | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow - + (* Stm *) + | VernacStm Finish -> VtStm (VtFinish, true), VtNow + | VernacStm Wait -> VtStm (VtWait, true), VtNow + | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow + | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow + | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow + | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) + | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e @@ -84,7 +98,7 @@ let rec classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtBack _ | VtProofMode _ ), _ as x -> x + | VtStm _ | VtProofMode _ ), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 13cb559b99..5acdb7eb7e 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -8,7 +8,7 @@ (** * Finite map library *) -(** This file proposes an implementation of the non-dependant interface +(** This file proposes an implementation of the non-dependent interface [FMapInterface.S] using lists of pairs ordered (increasing) with respect to left projection. *) diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 0f11dd7a53..130cbee871 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -8,7 +8,7 @@ (** * Finite map library *) -(** This file proposes an implementation of the non-dependant interface +(** This file proposes an implementation of the non-dependent interface [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) Require Import FMapInterface. diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index 1f36306c34..9c3ec71ae3 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [FSetInterface.S] using strictly ordered list. *) Require Export FSetInterface. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 2ea32e97cb..9dbea88495 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [FSetInterface.WS] using lists without redundancy. *) Require Import FSetInterface. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index fb0d1ad9df..05c20eb8fa 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [MSetInterface.S] using strictly ordered list. *) Require Export MSetInterface OrdersFacts OrdersLists. diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 372acd56ad..2ac57a932b 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [MSetWeakInterface.S] using lists without redundancy. *) Require Import MSetInterface. diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 45a7527c97..bd8930872c 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -10,7 +10,7 @@ (** * BigNumPrelude *) -(** Auxillary functions & theorems used for arbitrary precision efficient +(** Auxiliary functions & theorems used for arbitrary precision efficient numbers. *) @@ -22,7 +22,7 @@ Require Export Zpow_facts. Declare ML Module "numbers_syntax_plugin". (* *** Nota Bene *** - All results that were general enough has been moved in ZArith. + All results that were general enough have been moved in ZArith. Only remain here specialized lemmas and compatibility elements. (P.L. 5/11/2007). *) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 97cb746f37..55a533c55a 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -40,7 +40,7 @@ Defined. (** * Conversion between natural numbers modulo 256 and ascii characters *) -(** Auxillary function that turns a positive into an ascii by +(** Auxiliary function that turns a positive into an ascii by looking at the last 8 bits, ie z mod 2^8 *) Definition ascii_of_pos : positive -> ascii := diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ac69a69a4a..eab909f5b1 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -887,7 +887,7 @@ let merlin targets (ml_inc,_,_) = print ".merlin:\n"; print "\t@echo 'FLG -rectypes' > .merlin\n" ; List.iter (fun c -> - printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c) + printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c) lib_dirs ; List.iter (fun (_,c) -> printf "\t@echo \"B %s\" >> .merlin\n" c; diff --git a/tools/coqc.ml b/tools/coqc.ml index b59bbdb1e0..b12d48710f 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -94,7 +94,6 @@ let parse_args () = |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-native-compiler" - |"-verbose-compat-notations"|"-no-compat-notations" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 214dfb4703..8fcca535d1 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -266,9 +266,11 @@ let eval_print l coq = let to_id, _ = get_id id in eval_call (query (phrase, to_id)) coq | [ Tok(_,"WAIT") ] -> - eval_call (status false) coq + let phrase = "Stm Wait." in + eval_call (query (phrase,tip_id())) coq | [ Tok(_,"JOIN") ] -> - eval_call (status true) coq + let phrase = "Stm JoinDocument." in + eval_call (query (phrase,tip_id())) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 956a402617..38ceacf5ec 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -36,8 +36,6 @@ let print_usage_channel co command = \n -noinit start without loading the Init library\ \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ -\n -verbose-compat-notations be warned when using compatibility notations\ -\n -no-compat-notations get an error when using compatibility notations\ \n\ \n -load-ml-object f load ML object file f\ \n -load-ml-source f load ML file f\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ba5bc55069..bfdae85d50 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -27,7 +27,8 @@ let rec is_navigation_vernac = function | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ - | VernacBack _ -> true + | VernacBack _ + | VernacStm _ -> true | VernacRedirect (_, (_,c)) | VernacTime (_,c) -> is_navigation_vernac c (* Time Back* is harmless *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f0e63aa7c5..41ee165ff8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1127,7 +1127,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags (* Parts of this code are overly complicated because the implicit arguments API is completely crazy: positions (ExplByPos) are elaborated to names. This is broken by design, since not all arguments have names. So - eventhough we eventually want to map only positions to implicit statuses, + even though we eventually want to map only positions to implicit statuses, we have to check whether the corresponding arguments have names, not to trigger an error in the impargs code. Even better, the names we have to check are not the current ones (after previous renamings), but the original @@ -1941,6 +1941,7 @@ let interp ?proof ~loc locality poly c = | VernacTime _ -> assert false | VernacRedirect _ -> assert false | VernacTimeout _ -> assert false + | VernacStm _ -> assert false | VernacError e -> raise e @@ -2134,7 +2135,7 @@ let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () | Some b -> Flags.make_polymorphic_flag b; b -(** A global default timeout, controled by option "Set Default Timeout n". +(** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) let default_timeout = ref None @@ -2208,6 +2209,9 @@ let interp ?(verbosely=true) ?proof (loc,c) = aux ?locality ~polymorphism:b isprogcmd c | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" | VernacLocal _ -> CErrors.error "Locality specified twice" + | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c + | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c + | VernacStm _ -> assert false (* Done by Stm *) | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> |