diff options
38 files changed, 196 insertions, 108 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/changes.txt b/dev/doc/changes.txt index 134a6a25e8..3de938d774 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -218,6 +218,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id for constructing compound entries still works over this scheme. Note that in the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound in the parsing rules, so beware of recursive calls. + + For example, to get "wit_constr" you must "open Constrarg" at the top of the file. - Evarutil was split in two parts. The new Evardefine file exposes functions define_evar_* mostly used internally in the unification engine. @@ -244,6 +246,10 @@ define_evar_* mostly used internally in the unification engine. ... let Sigma (xn, sigma, pn) = ... in Sigma (ans, sigma, p1 +> ... +> pn) + + Examples of `Sigma.Unsafe.of_evar_map` include: + + Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty - The Proofview.Goal.*enter family of functions now takes a polymorphic continuation given as a record as an argument. @@ -258,6 +264,9 @@ define_evar_* mostly used internally in the unification engine. - `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` - `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` +- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` + (`Global.named_context` ---> `Global.named_context_val`) + (`Context.Named.lookup` ---> `Environ.lookup_named_val`) ** Search API ** 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/doc/refman/Classes.tex b/doc/refman/Classes.tex index bd8ee450ef..acfc4bea93 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -380,6 +380,7 @@ use implicit generalization (see \ref{SectionContext}). \asubsection{\tt typeclasses eauto} \tacindex{typeclasses eauto} +\label{typeclasseseauto} The {\tt typeclasses eauto} tactic uses a different resolution engine than {\tt eauto} and {\tt auto}. The main differences are the following: 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/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/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/kernel/names.ml b/kernel/names.ml index 9267a64d61..1eb9a31751 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,9 +34,15 @@ struct let hash = String.hash + let warn_invalid_identifier = + CWarnings.create ~name:"invalid-identifier" ~category:"parsing" + ~default:CWarnings.Disabled + (fun s -> str s) + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else + if warn then warn_invalid_identifier x in Option.iter iter (Unicode.ident_refutation x) 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/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 22a2d7fc2f..6a8fa8d698 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -50,11 +50,17 @@ let eval_uconstrs ist cs = } in List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs -let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ()) +let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob ARGUMENT EXTEND auto_using TYPED AS uconstr_list PRINTED BY pr_auto_using + RAW_TYPED AS uconstr_list + RAW_PRINTED BY pr_auto_using_raw + GLOB_TYPED AS uconstr_list + GLOB_PRINTED BY pr_auto_using_glob | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] | [ ] -> [ [] ] END @@ -171,18 +177,32 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] END -let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global +let glob_hints_path_atom ist = Hints.glob_hints_path_atom ARGUMENT EXTEND hints_path_atom PRINTED BY pr_hints_path_atom -| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] + + GLOBALIZED BY glob_hints_path_atom + + RAW_PRINTED BY pr_pre_hints_path_atom + GLOB_PRINTED BY pr_hints_path_atom +| [ ne_global_list(g) ] -> [ Hints.PathHints g ] | [ "_" ] -> [ Hints.PathAny ] END let pr_hints_path prc prx pry c = Hints.pp_hints_path c - +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let glob_hints_path ist = Hints.glob_hints_path + ARGUMENT EXTEND hints_path - PRINTED BY pr_hints_path +PRINTED BY pr_hints_path + +GLOBALIZED BY glob_hints_path +RAW_PRINTED BY pr_pre_hints_path +GLOB_PRINTED BY pr_hints_path + | [ "(" hints_path(p) ")" ] -> [ p ] | [ hints_path(p) "*" ] -> [ Hints.PathStar p ] | [ "emp" ] -> [ Hints.PathEmpty ] @@ -192,8 +212,6 @@ ARGUMENT EXTEND hints_path | [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] END -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - ARGUMENT EXTEND opthints TYPED AS preident_list_opt PRINTED BY pr_hintbases @@ -203,7 +221,7 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry p in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (match dbnames with None -> ["core"] | Some l -> l) entry ] END diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index d570f015eb..aec6a32644 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -419,8 +419,8 @@ let rec comment loc bp = parser bp2 | [< '')' >] -> push_string "*)"; loc | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc | [< ''"'; s >] -> - let loc = fst (string loc ~comm_level:(Some 0) bp2 0 s) - in + let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in + push_string "\""; push_string (get_buff len); push_string "\""; comment loc bp s | [< _ = Stream.empty >] ep -> let loc = set_loc_pos loc bp ep in diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9b52d1bf31..e61be53a99 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -582,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 @@ -664,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 ]; @@ -776,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/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 95095b09cb..43fac8ad83 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -116,9 +116,9 @@ open Pp open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l -let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l -let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference +let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) +let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global let warn_deprecated_syntax = CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" 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..fcc30d702f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -219,7 +219,7 @@ module Make | ConstrContext ((_,id),c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ - str "[" ++ prlc c ++ str "]") + str "[ " ++ prlc c ++ str " ]") | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc c) | ConstrTerm c when test c -> @@ -630,7 +630,8 @@ module Make | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,()) in pr_in - (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) + (prlist_with_sep (fun () -> str",") + (fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs) let pr_orient b = if b then mt () else str "<- " @@ -675,9 +676,9 @@ module Make | Subterm (b,None,a) -> (** ppedrot: we don't make difference between [appcontext] and [context] anymore, and the interpretation is governed by a flag instead. *) - keyword "context" ++ str" [" ++ pr_pat a ++ str "]" + keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" | Subterm (b,Some id,a) -> - keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" + keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function | Hyp (nal,mp) -> @@ -1216,7 +1217,7 @@ module Make | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))) in pr_tac diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3494ad006f..5d6d36d569 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -913,7 +913,7 @@ module Make | VernacContext l -> return ( hov 1 ( - keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) + keyword "Context" ++ pr_and_type_binders_arg l) ) | VernacDeclareInstances insts -> @@ -1015,7 +1015,10 @@ module Make (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match compat with None -> [] | Some v -> [SetCompatVersion v])) + (match compat with + | None -> [] + | Some Flags.Current -> [SetOnlyParsing] + | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( @@ -1057,7 +1060,7 @@ module Make in print_arguments nargs args ++ if not (List.is_empty more_implicits) then - str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function @@ -1128,7 +1131,7 @@ module Make | VernacSetAppendOption (na,v) -> return ( hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ str v) + spc() ++ keyword "Append" ++ spc() ++ qs v) ) | VernacAddOption (na,l) -> return ( 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 e387e6322f..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 diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e44ace4257..b416bc657a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1124,12 +1124,12 @@ module Search = struct else tclDISPATCH (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) in - let finish sigma = + let finish nestedshelf sigma = let filter ev = try let evi = Evd.find_undefined sigma ev in if info.search_only_classes then - Some (ev, is_class_type sigma (Evd.evar_concl evi)) + Some (ev, not (is_class_type sigma (Evd.evar_concl evi))) else Some (ev, true) with Not_found -> None in @@ -1147,9 +1147,9 @@ module Search = struct begin (* Some existentials produced by the original tactic were not solved in the subgoals, turn them into subgoals now. *) - let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in - let shelved = List.map fst shelved and goals = List.map fst goals in - if !typeclasses_debug > 1 && not (List.is_empty goals) then + let shelved, goals = List.partition (fun (ev, s) -> s) remaining in + let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in + if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ prlist_with_sep spc (pr_ev sigma) goals ++ @@ -1162,7 +1162,8 @@ module Search = struct with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= fun s -> result s i (Some (Option.default 0 k + j))) end - in res <*> tclEVARMAP >>= finish + in with_shelf res >>= fun (sh, ()) -> + tclEVARMAP >>= finish sh in if path_matches derivs [] then aux e tl else diff --git a/tactics/hints.ml b/tactics/hints.ml index d91ea8079c..9a96b73898 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -100,18 +100,25 @@ type 'a hint_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Genarg.glob_generic_argument (* Hint Extern *) -type hints_path_atom = - | PathHints of global_reference list + +type 'a hints_path_atom_gen = + | PathHints of 'a list + (* For forward hints, their names is the list of projections *) | PathAny -type hints_path = - | PathAtom of hints_path_atom - | PathStar of hints_path - | PathSeq of hints_path * hints_path - | PathOr of hints_path * hints_path +type hints_path_atom = global_reference hints_path_atom_gen + +type 'a hints_path_gen = + | PathAtom of 'a hints_path_atom_gen + | PathStar of 'a hints_path_gen + | PathSeq of 'a hints_path_gen * 'a hints_path_gen + | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon +type pre_hints_path = Libnames.reference hints_path_gen +type hints_path = global_reference hints_path_gen + type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set @@ -393,21 +400,40 @@ let rec normalize_path h = let path_derivate hp hint = normalize_path (path_derivate hp hint) -let pp_hints_path_atom a = +let pp_hints_path_atom prg a = match a with | PathAny -> str"_" - | PathHints grs -> pr_sequence pr_global grs - -let rec pp_hints_path = function - | PathAtom pa -> pp_hints_path_atom pa - | PathStar (PathAtom PathAny) -> str"_*" - | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" - | PathSeq (p, p') -> pp_hints_path p ++ spc () ++ pp_hints_path p' - | PathOr (p, p') -> - str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ cut () ++ spc () ++ - pp_hints_path p' ++ str ")" + | PathHints grs -> pr_sequence prg grs + +let pp_hints_path_gen prg = + let rec aux = function + | PathAtom pa -> pp_hints_path_atom prg pa + | PathStar (PathAtom PathAny) -> str"_*" + | PathStar p -> str "(" ++ aux p ++ str")*" + | PathSeq (p, p') -> aux p ++ spc () ++ aux p' + | PathOr (p, p') -> + str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++ + aux p' ++ str ")" | PathEmpty -> str"emp" | PathEpsilon -> str"eps" + in aux + +let pp_hints_path = pp_hints_path_gen pr_global + +let glob_hints_path_atom p = + match p with + | PathHints g -> PathHints (List.map Nametab.global g) + | PathAny -> PathAny + +let glob_hints_path = + let rec aux = function + | PathAtom pa -> PathAtom (glob_hints_path_atom pa) + | PathStar p -> PathStar (aux p) + | PathSeq (p, p') -> PathSeq (aux p, aux p') + | PathOr (p, p') -> PathOr (aux p, aux p') + | PathEmpty -> PathEmpty + | PathEpsilon -> PathEpsilon + in aux let subst_path_atom subst p = match p with diff --git a/tactics/hints.mli b/tactics/hints.mli index 42a2896ed8..1be3e0c52f 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -42,11 +42,12 @@ type 'a hint_ast = type hint type raw_hint = constr * types * Univ.universe_context_set -type hints_path_atom = - | PathHints of global_reference list +type 'a hints_path_atom_gen = + | PathHints of 'a list (* For forward hints, their names is the list of projections *) | PathAny +type hints_path_atom = global_reference hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -67,20 +68,28 @@ type search_entry type hint_entry -type hints_path = - | PathAtom of hints_path_atom - | PathStar of hints_path - | PathSeq of hints_path * hints_path - | PathOr of hints_path * hints_path +type 'a hints_path_gen = + | PathAtom of 'a hints_path_atom_gen + | PathStar of 'a hints_path_gen + | PathSeq of 'a hints_path_gen * 'a hints_path_gen + | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon +type pre_hints_path = Libnames.reference hints_path_gen +type hints_path = global_reference hints_path_gen + val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path -val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds +val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds +val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds val pp_hints_path : hints_path -> Pp.std_ppcmds val pp_hint_mode : hint_mode -> Pp.std_ppcmds +val glob_hints_path_atom : + Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen +val glob_hints_path : + Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen module Hint_db : sig diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index f62427ef47..6b1f0315bc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -98,7 +98,7 @@ Goal exists R, @Refl nat R. solve [typeclasses eauto with foo]. Qed. -(* Set Typeclasses Compatibility "8.5". *) +Set Typeclasses Compatibility "8.5". Parameter f : nat -> Prop. Parameter g : nat -> nat -> Prop. Parameter h : nat -> nat -> nat -> Prop. @@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y. Hint Resolve a b c : mybase. Goal forall x y z, h x y z -> f x -> f y. intros. - Set Typeclasses Debug. - typeclasses eauto with mybase. + Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *) Unshelve. Abort. End bt. @@ -138,7 +137,8 @@ Notation "'return' t" := (unit t). Class A `(e: T) := { a := True }. Class B `(e_: T) := { e := e_; sg_ass :> A e }. -Set Typeclasses Debug. +(* Set Typeclasses Debug. *) +(* Set Typeclasses Debug Verbosity 2. *) Goal forall `{B T}, Prop. intros. apply a. 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/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 230e62607a..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 @@ -2135,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 |