diff options
182 files changed, 751 insertions, 626 deletions
diff --git a/.merlin.in b/.merlin.in index db7259dd6f..a8049361ee 100644 --- a/.merlin.in +++ b/.merlin.in @@ -1,4 +1,4 @@ -FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50 +FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48 S clib B clib diff --git a/checker/analyze.ml b/checker/analyze.ml index 7047d8a149..63324bff20 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -396,7 +396,7 @@ let parse_string s = PString.parse (s, ref 0) let instantiate (p, mem) = let len = LargeArray.length mem in let ans = LargeArray.make len (Obj.repr 0) in - (** First pass: initialize the subobjects *) + (* First pass: initialize the subobjects *) for i = 0 to len - 1 do let obj = match LargeArray.get mem i with | Struct (tag, blk) -> Obj.new_block tag (Array.length blk) @@ -408,9 +408,9 @@ let instantiate (p, mem) = | Int n -> Obj.repr n | Ptr p -> LargeArray.get ans p | Atm tag -> Obj.new_block tag 0 - | Fun _ -> assert false (** We shouldn't serialize closures *) + | Fun _ -> assert false (* We shouldn't serialize closures *) in - (** Second pass: set the pointers *) + (* Second pass: set the pointers *) for i = 0 to len - 1 do match LargeArray.get mem i with | Struct (_, blk) -> diff --git a/checker/analyze.mli b/checker/analyze.mli index 9c837643fa..d7770539df 100644 --- a/checker/analyze.mli +++ b/checker/analyze.mli @@ -30,6 +30,7 @@ sig type t val input_byte : t -> int (** Input a single byte *) + val input_binary_int : t -> int (** Input a big-endian 31-bits signed integer *) end diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4e026d6f60..ef10bf827d 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -95,11 +95,11 @@ let typecheck_arity env params inds = (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let check_subtyping cumi paramsctxt env arities = - let numparams = Context.Rel.nhyps paramsctxt in - (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available. - We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] - and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together - with the cumulativity constraints [ cumul_cst ]. *) + let numparams = Context.Rel.nhyps paramsctxt in + (* In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available. + We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] + and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together + with the cumulativity constraints [ cumul_cst ]. *) let uctx = ACumulativityInfo.univ_context cumi in let len = AUContext.size uctx in let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in @@ -238,7 +238,7 @@ let check_inductive env kn mib = let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in Environ.push_context uctx env in - (** Locally set the oracle for further typechecking *) + (* Locally set the oracle for further typechecking *) let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index b83fe831bb..086dd17e39 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -10,10 +10,10 @@ open Environ let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); - (** Locally set the oracle for further typechecking *) + (* Locally set the oracle for further typechecking *) let oracle = env.env_typing_flags.conv_oracle in let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in - (** [env'] contains De Bruijn universe variables *) + (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env @@ -40,7 +40,7 @@ let check_constant_declaration env kn cb = if poly then add_constant kn cb env else add_constant kn cb env' in - (** Reset the value of the oracle *) + (* Reset the value of the oracle *) Environ.set_oracle env oracle (** {6 Checking modules } *) diff --git a/checker/votour.ml b/checker/votour.ml index 1ea0de456e..3c088b59b5 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -366,7 +366,7 @@ let visit_vo f = |] in let repr = if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S) - (** On 32-bit machines, representation may exceed the max size of arrays *) + (* On 32-bit machines, representation may exceed the max size of arrays *) in let module Repr = (val repr : S) in let module Visit = Visit(Repr) in diff --git a/clib/backtrace.ml b/clib/backtrace.ml index 27ed6fbf72..64faa5fd2e 100644 --- a/clib/backtrace.ml +++ b/clib/backtrace.ml @@ -87,8 +87,8 @@ let get_backtrace e = let add_backtrace e = if !is_recording then - (** This must be the first function call, otherwise the stack may be - destroyed *) + (* This must be the first function call, otherwise the stack may be + destroyed *) let current = get_exception_backtrace () in let info = Exninfo.info e in begin match current with diff --git a/clib/bigint.mli b/clib/bigint.mli index ac66b41fb7..88297c353d 100644 --- a/clib/bigint.mli +++ b/clib/bigint.mli @@ -25,6 +25,7 @@ val one : bigint val two : bigint val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *) + val add_1 : bigint -> bigint val sub_1 : bigint -> bigint val mult_2 : bigint -> bigint diff --git a/clib/cArray.ml b/clib/cArray.ml index c3a693ff16..e0a1859184 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -451,7 +451,7 @@ struct end done; if !i < len then begin - (** The array is not the same as the original one *) + (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; @@ -483,7 +483,7 @@ struct end done; if !i < len then begin - (** The array is not the same as the original one *) + (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; @@ -504,7 +504,7 @@ struct let i = ref 0 in let break = ref true in let r = ref accu in - (** This variable is never accessed unset *) + (* This variable is never accessed unset *) let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in @@ -539,7 +539,7 @@ struct let i = ref 0 in let break = ref true in let r = ref accu in - (** This variable is never accessed unset *) + (* This variable is never accessed unset *) let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in @@ -620,7 +620,7 @@ struct end done; if !i < len then begin - (** The array is not the same as the original one *) + (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; diff --git a/clib/cString.mli b/clib/cString.mli index a73c2729d0..364b6a34b1 100644 --- a/clib/cString.mli +++ b/clib/cString.mli @@ -31,8 +31,8 @@ sig (** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *) val strip : string -> string - (** Alias for [String.trim] *) [@@ocaml.deprecated "Use [trim]"] + (** Alias for [String.trim] *) val drop_simple_quotes : string -> string (** Remove the eventual first surrounding simple quotes of a string. *) @@ -53,8 +53,8 @@ sig (** Generate the ordinal number in English. *) val split : char -> string -> string list - (** [split c s] alias of [String.split_on_char] *) [@@ocaml.deprecated "Use [split_on_char]"] + (** [split c s] alias of [String.split_on_char] *) val is_sub : string -> string -> int -> bool (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *) diff --git a/clib/exninfo.ml b/clib/exninfo.ml index 2d13049882..78ebd81f7e 100644 --- a/clib/exninfo.ml +++ b/clib/exninfo.ml @@ -89,18 +89,18 @@ let find_and_remove () = let info e = let (src, data) = find_and_remove () in if src == e then - (** Slightly unsound, some exceptions may not be unique up to pointer - equality. Though, it should be quite exceptional to be in a situation - where the following holds: - - 1. An argument-free exception is raised through the enriched {!raise}; - 2. It is not captured by any enriched with-clause (which would reset - the current data); - 3. The same exception is raised through the standard raise, accessing - the wrong data. + (* Slightly unsound, some exceptions may not be unique up to pointer + equality. Though, it should be quite exceptional to be in a situation + where the following holds: + + 1. An argument-free exception is raised through the enriched {!raise}; + 2. It is not captured by any enriched with-clause (which would reset + the current data); + 3. The same exception is raised through the standard raise, accessing + the wrong data. . *) data else - (** Mismatch: the raised exception is not the one stored, either because the - previous raise was not instrumented, or because something went wrong. *) + (* Mismatch: the raised exception is not the one stored, either because the + previous raise was not instrumented, or because something went wrong. *) Store.empty diff --git a/clib/hMap.mli b/clib/hMap.mli index b26d0e04e3..ab2a6bbf15 100644 --- a/clib/hMap.mli +++ b/clib/hMap.mli @@ -13,6 +13,7 @@ sig type t val compare : t -> t -> int (** Total ordering *) + val hash : t -> int (** Hashing function compatible with [compare], i.e. [compare x y = 0] implies [hash x = hash y]. *) diff --git a/clib/hashcons.mli b/clib/hashcons.mli index 223dd2a4d2..e97708cdf3 100644 --- a/clib/hashcons.mli +++ b/clib/hashcons.mli @@ -29,17 +29,21 @@ module type HashconsedType = type t (** Type of objects to hashcons. *) + type u (** Type of hashcons functions for the sub-structures contained in [t]. Usually a tuple of functions. *) + val hashcons : u -> t -> t (** The actual hashconsing function, using its fist argument to recursively hashcons substructures. It should be compatible with [eq], that is [eq x (hashcons f x) = true]. *) + val eq : t -> t -> bool (** A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the [hashcons] function, but it should be insensible to shallow copy of the compared object. *) + val hash : t -> int (** A hash function passed to the underlying hashtable structure. [hash] should be compatible with [eq], i.e. if [eq x y = true] then @@ -50,14 +54,19 @@ module type S = sig type t (** Type of objects to hashcons. *) + type u (** Type of hashcons functions for the sub-structures contained in [t]. *) + type table (** Type of hashconsing tables *) + val generate : u -> table (** This create a hashtable of the hashconsed objects. *) + val hcons : table -> t -> t (** Perform the hashconsing of the given object within the table. *) + val stats : table -> Hashset.statistics (** Recover statistics of the hashconsing table. *) end diff --git a/clib/hashset.mli b/clib/hashset.mli index 0699d4e848..6ed93d5fe7 100644 --- a/clib/hashset.mli +++ b/clib/hashset.mli @@ -31,18 +31,23 @@ type statistics = { module type S = sig type elt (** Type of hashsets elements. *) + type t (** Type of hashsets. *) + val create : int -> t (** [create n] creates a fresh hashset with initial size [n]. *) + val clear : t -> unit (** Clear the contents of a hashset. *) + val repr : int -> elt -> t -> elt (** [repr key constr set] uses [key] to look for [constr] in the hashet [set]. If [constr] is in [set], returns the specific representation that is stored in [set]. Otherwise, [constr] is stored in [set] and will be used as the canonical representation of this value in the future. *) + val stats : t -> statistics (** Recover statistics on the table. *) end diff --git a/clib/int.ml b/clib/int.ml index 3ae836aec9..fa21379565 100644 --- a/clib/int.ml +++ b/clib/int.ml @@ -114,8 +114,8 @@ struct let () = t := DSet (i, old, res) in res else match v with - | None -> t (** Nothing to do! *) - | Some _ -> (** we must resize *) + | None -> t (* Nothing to do! *) + | Some _ -> (* we must resize *) let nlen = next len (succ i) in let nlen = min nlen Sys.max_array_length in let () = assert (i < nlen) in diff --git a/clib/int.mli b/clib/int.mli index 76aecf057b..e02ca90916 100644 --- a/clib/int.mli +++ b/clib/int.mli @@ -33,10 +33,13 @@ sig type 'a t (** Persistent, auto-resizable arrays. The [get] and [set] functions never fail whenever the index is between [0] and [Sys.max_array_length - 1]. *) + val empty : int -> 'a t (** The empty array, with a given starting size. *) + val get : 'a t -> int -> 'a option (** Get a value at the given index. Returns [None] if undefined. *) + val set : 'a t -> int -> 'a option -> 'a t (** Set/unset a value at the given index. *) end diff --git a/clib/segmenttree.ml b/clib/segmenttree.ml index 24243b7a99..c3f1b44ef4 100644 --- a/clib/segmenttree.ml +++ b/clib/segmenttree.ml @@ -34,16 +34,16 @@ type elt = int integers which are _not_ in the set of keys handled by the tree. On leaves, a domain represents the st of integers which are in the set of keys. *) -type domain = - (** On internal nodes, a domain [Interval (a, b)] represents - the interval [a + 1; b - 1]. On leaves, it represents [a; b]. - We always have [a] <= [b]. *) +type domain = | Interval of elt * elt - (** On internal node or root, a domain [Universe] represents all - the integers. When the tree is not a trivial root, - [Universe] has no interpretation on leaves. (The lookup - function should never reach the leaves.) *) + (** On internal nodes, a domain [Interval (a, b)] represents + the interval [a + 1; b - 1]. On leaves, it represents [a; b]. + We always have [a] <= [b]. *) | Universe + (** On internal node or root, a domain [Universe] represents all + the integers. When the tree is not a trivial root, + [Universe] has no interpretation on leaves. (The lookup + function should never reach the leaves.) *) (** We use an array to store the almost complete tree. This array contains at least one element. *) @@ -71,26 +71,26 @@ let make segments = let tree = create nsegments (Universe, None) in let leaves_offset = (1 lsl (log2n nsegments)) - 1 in - (** The algorithm proceeds in two steps using an intermediate tree - to store minimum and maximum of each subtree as annotation of - the node. *) + (* The algorithm proceeds in two steps using an intermediate tree + to store minimum and maximum of each subtree as annotation of + the node. *) - (** We start from leaves: the last level of the tree is initialized - with the given segments... *) - list_iteri + (* We start from leaves: the last level of the tree is initialized + with the given segments... *) + list_iteri (fun i ((start, stop), value) -> let k = leaves_offset + i in let i = Interval (start, stop) in tree.(k) <- (i, Some i)) segments; - (** ... the remaining leaves are initialized with neutral information. *) + (* ... the remaining leaves are initialized with neutral information. *) for k = leaves_offset + nsegments to Array.length tree -1 do tree.(k) <- (Universe, Some Universe) done; - (** We traverse the tree bottom-up and compute the interval and - annotation associated to each node from the annotations of its - children. *) + (* We traverse the tree bottom-up and compute the interval and + annotation associated to each node from the annotations of its + children. *) for k = leaves_offset - 1 downto 0 do let node, annotation = match value_of (left_child k) tree, value_of (right_child k) tree with @@ -104,7 +104,7 @@ let make segments = tree.(k) <- (node, Some annotation) done; - (** Finally, annotation are replaced with the image related to each leaf. *) + (* Finally, annotation are replaced with the image related to each leaf. *) let final_tree = Array.mapi (fun i (segment, value) -> (segment, None)) tree in diff --git a/clib/trie.ml b/clib/trie.ml index ea43e9e0bd..96de2b920c 100644 --- a/clib/trie.ml +++ b/clib/trie.ml @@ -51,7 +51,7 @@ let next (Node (_,m)) lbl = T_codom.find lbl m let get (Node (hereset,_)) = hereset let labels (Node (_,m)) = - (** FIXME: this is order-dependent. Try to find a more robust presentation? *) + (* FIXME: this is order-dependent. Try to find a more robust presentation? *) List.rev (T_codom.fold (fun x _ acc -> x::acc) m []) let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty b) diff --git a/configure.ml b/configure.ml index ec765acc15..6db96244f5 100644 --- a/configure.ml +++ b/configure.ml @@ -610,10 +610,9 @@ let camltag = match caml_version_list with 44: "open" shadowing already defined identifier: too common, especially when some are aliases 45: "open" shadowing a label or constructor: see 44 48: implicit elimination of optional arguments: too common - 50: unexpected documentation comment: too common and annoying to avoid 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 *) -let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58" +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 8d728b5b51..cc76c44651 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -26,7 +26,7 @@ let pr_loc loc = let print_code fmt c = let loc = c.loc.loc_start in - (** Print the line location as a source annotation *) + (* Print the line location as a source annotation *) let padding = String.make (loc.pos_cnum - loc.pos_bol + 1) ' ' in let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in fprintf fmt "@[@<0>%s@]@\n" code_insert @@ -471,16 +471,16 @@ let parse_rule self r = (symbs, vars, r.tac_body) let print_rules fmt (name, rules) = - (** Rules are reversed. *) + (* Rules are reversed. *) let rules = List.rev rules in let rules = List.map (fun r -> parse_rule name r) rules in let pr fmt l = print_list fmt (fun fmt r -> fprintf fmt "(%a)" GramExt.print_extrule r) l in match rules with | [([SymbEntry (e, None)], [Some s], { code = c } )] when String.trim c = s -> - (** This is a horrible hack to work aroud limitations of camlp5 regarding - factorization of parsing rules. It allows to recognize rules of the - form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and - reuse the same entry directly. *) + (* This is a horrible hack to work aroud limitations of camlp5 regarding + factorization of parsing rules. It allows to recognize rules of the + form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and + reuse the same entry directly. *) fprintf fmt "@[Vernacextend.Arg_alias (%s)@]" e | _ -> fprintf fmt "@[Vernacextend.Arg_rules (%a)@]" pr rules diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh new file mode 100644 index 0000000000..f2a113b118 --- /dev/null +++ b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then + + mtac2_CI_REF=build+warn_50 + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b90a53220d..8f207d1e0a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -476,7 +476,7 @@ let pp_generic_argument arg = let prgenarginfo arg = let Geninterp.Val.Dyn (tag, _) = arg in let tpe = Geninterp.Val.pr tag in - (** FIXME *) + (* FIXME *) (* try *) (* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) (* str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *) @@ -1,9 +1,9 @@ ; Default flags for all Coq libraries. (env - (dev (flags :standard -rectypes -w -9-27-50+40+60)) + (dev (flags :standard -rectypes -w -9-27+40+60)) (release (flags :standard -rectypes) (ocamlopt_flags -O3 -unbox-closures)) - (ireport (flags :standard -rectypes -w -9-27-50+40+60) + (ireport (flags :standard -rectypes -w -9-27-40+60) (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))) ; The _ profile could help factoring the above, however it doesn't diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 96f1ce5e60..24d161d00a 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -606,6 +606,7 @@ let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c)) let subst_univs_level_constr subst c = of_constr (Vars.subst_univs_level_constr subst (to_constr c)) + (** Operations that dot NOT commute with evar-normalization *) let noccurn sigma n term = let rec occur_rec n c = match kind sigma c with diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 69ee5223c4..db56d0628f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -155,7 +155,7 @@ let is_ground_env = memo is_ground_env exception NoHeadEvar let head_evar sigma c = - (** FIXME: this breaks if using evar-insensitive code *) + (* FIXME: this breaks if using evar-insensitive code *) let c = EConstr.Unsafe.to_constr c in let rec hrec c = match kind c with | Evar (evk,_) -> evk @@ -288,7 +288,7 @@ let empty_csubst = { } let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c = - (** Safe because this is a substitution *) + (* Safe because this is a substitution *) let c = EConstr.Unsafe.to_constr c in let rec subst n c = match Constr.kind c with | Rel m -> @@ -318,7 +318,7 @@ let update_var src tgt subst = in match cur with | None -> - (** Missing keys stand for identity substitution [src ↦ src] *) + (* Missing keys stand for identity substitution [src ↦ src] *) let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in { subst with csubst_var; csubst_rev } @@ -366,8 +366,8 @@ let push_rel_decl_to_named_context about this whole name generation problem. *) if Flags.is_program_mode () then next_name_away na avoid else - (** id_of_name_using_hdchar only depends on the rel context which is empty - here *) + (* id_of_name_using_hdchar only depends on the rel context which is empty + here *) next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with @@ -540,8 +540,8 @@ let restrict_evar evd evk filter ?src candidates = | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None)) | _ -> let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - (** Mark new evar as future goal, removing previous one, - circumventing Proofview.advance but making Proof.run_tactic catch these. *) + (* Mark new evar as future goal, removing previous one, + circumventing Proofview.advance but making Proof.run_tactic catch these. *) let future_goals = Evd.save_future_goals evd in let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in let evd = Evd.restore_future_goals evd future_goals in @@ -779,7 +779,7 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with let r = try Id.Map.find id cache.cache with Not_found -> - (** Dummy value *) + (* Dummy value *) let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in let () = cache.cache <- Id.Map.add id r cache.cache in r diff --git a/engine/evd.ml b/engine/evd.ml index 6345046431..7bc3be87a4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -89,8 +89,8 @@ struct | Some f2 -> normalize (CList.filter_with f1 f2) let apply_subfilter_array filter subfilter = - (** In both cases we statically know that the argument will contain at - least one [false] *) + (* In both cases we statically know that the argument will contain at + least one [false] *) match filter with | None -> Some (Array.to_list subfilter) | Some f -> @@ -395,7 +395,7 @@ let rename evk id (evtoid, idtoev) = let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in match id with - | None -> names (** evk' must not be defined *) + | None -> names (* evk' must not be defined *) | Some id -> (EvMap.add evk' id (EvMap.remove evk evtoid), Id.Map.add id evk' (Id.Map.remove id idtoev)) @@ -416,7 +416,7 @@ type evar_flags = typeclass_evars : Evar.Set.t } type evar_map = { - (** Existential variables *) + (* Existential variables *) defn_evars : evar_info EvMap.t; undf_evars : evar_info EvMap.t; evar_names : EvNames.t; @@ -520,7 +520,7 @@ let inherit_evar_flags evar_flags evk evk' = let remove_evar_flags evk evar_flags = { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars; obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars; - (** Restriction information is kept. *) + (* Restriction information is kept. *) restricted_evars = evar_flags.restricted_evars } (** New evars *) @@ -1341,14 +1341,14 @@ module MiniEConstr = struct | None -> c end | App (f, args) when isEvar f -> - (** Enforce smart constructor invariant on applications *) + (* Enforce smart constructor invariant on applications *) let ev = destEvar f in begin match safe_evar_value sigma ev with | None -> c | Some f -> whd_evar sigma (mkApp (f, args)) end | Cast (c0, k, t) when isEvar c0 -> - (** Enforce smart constructor invariant on casts. *) + (* Enforce smart constructor invariant on casts. *) let ev = destEvar c0 in begin match safe_evar_value sigma ev with | None -> c diff --git a/engine/evd.mli b/engine/evd.mli index 0a8d1f3287..7560d68805 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -86,7 +86,7 @@ type evar_body = type evar_info = { evar_concl : econstr; (** Type of the evar. *) - evar_hyps : named_context_val; (** TODO econstr? *) + evar_hyps : named_context_val; (* TODO econstr? *) (** Context of the evar. *) evar_body : evar_body; (** Optional content of the evar. *) @@ -546,6 +546,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map + (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t @@ -567,6 +568,7 @@ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) + val is_flexible_level : evar_map -> Univ.Level.t -> bool (* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *) diff --git a/engine/ftactic.ml b/engine/ftactic.ml index b371884ba4..ac0344148a 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -29,8 +29,8 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function | Depends l -> let f arg = f arg >>= function | Uniform x -> - (** We dispatch the uniform result on each goal under focus, as we know - that the [m] argument was actually dependent. *) + (* We dispatch the uniform result on each goal under focus, as we know + that the [m] argument was actually dependent. *) Proofview.Goal.goals >>= fun goals -> let ans = List.map (fun g -> (g,x)) goals in Proofview.tclUNIT ans diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 4afa817b27..e0c24f049f 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -28,8 +28,10 @@ from the IO monad ([Proofview] catches errors in its compatibility layer, and when lifting goal-level expressions). *) exception Exception of exn + (** This exception is used to signal abortion in [timeout] functions. *) exception Timeout + (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system interrupts). *) diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 545334ce9a..3e57baab26 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -28,8 +28,10 @@ from the IO monad ([Proofview] catches errors in its compatibility layer, and when lifting goal-level expressions). *) exception Exception of exn + (** This exception is used to signal abortion in [timeout] functions. *) exception Timeout + (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system interrupts). *) @@ -51,8 +53,10 @@ module NonLogical : sig val ref : 'a -> 'a ref t (** [Pervasives.(:=)] *) + val (:=) : 'a ref -> 'a -> unit t (** [Pervasives.(!)] *) + val (!) : 'a ref -> 'a t val read_line : string t @@ -67,6 +71,7 @@ module NonLogical : sig (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) val raise : ?info:Exninfo.info -> exn -> 'a t + (** [try ... with ...] but restricted to {!Exception}. *) val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t val timeout : int -> 'a t -> 'a t diff --git a/engine/namegen.ml b/engine/namegen.ml index a67ff6965b..018eca1ba2 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -358,7 +358,7 @@ let next_name_away_with_default_using_types default na avoid t = let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env sigma = - (** FIXME: this is inefficient, but only used in printing *) + (* FIXME: this is inefficient, but only used in printing *) let avoid = ref (ids_of_named_context_val (named_context_val env)) in let sign = named_context_val env in let rels = rel_context env in diff --git a/engine/nameops.mli b/engine/nameops.mli index 8a93fad8cc..a5308904f5 100644 --- a/engine/nameops.mli +++ b/engine/nameops.mli @@ -16,6 +16,7 @@ val make_ident : string -> int option -> Id.t val repr_ident : Id.t -> string * int option val atompart_of_id : Id.t -> string (** remove trailing digits *) + val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) val add_suffix : Id.t -> string -> Id.t diff --git a/engine/proofview.ml b/engine/proofview.ml index 304b2dff84..8c15579bb0 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -660,9 +660,9 @@ let unifiable_delayed g l = let free_evars sigma l = let cache = Evarutil.create_undefined_evars_cache () in let map ev = - (** Computes the set of evars appearing in the hypotheses, the conclusion or - the body of the evar_info [evi]. Note: since we want to use it on goals, - the body is actually supposed to be empty. *) + (* Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) let evi = Evd.find sigma ev in let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in (ev, fevs) @@ -672,9 +672,9 @@ let free_evars sigma l = let free_evars_with_state sigma l = let cache = Evarutil.create_undefined_evars_cache () in let map ev = - (** Computes the set of evars appearing in the hypotheses, the conclusion or - the body of the evar_info [evi]. Note: since we want to use it on goals, - the body is actually supposed to be empty. *) + (* Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) let ev = drop_state ev in let evi = Evd.find sigma ev in let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in @@ -1157,7 +1157,7 @@ module Goal = struct let sigma = step.solution in let map goal = match cleared_alias sigma goal with - | None -> None (** ppedrot: Is this check really necessary? *) + | None -> None (* ppedrot: Is this check really necessary? *) | Some goal -> let gl = Env.get >>= fun env -> diff --git a/engine/proofview.mli b/engine/proofview.mli index cda4808a23..28e793f0fc 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -398,6 +398,7 @@ val tclPROGRESS : 'a tactic -> 'a tactic val tclCHECKINTERRUPT : unit tactic exception Timeout + (** [tclTIMEOUT n t] can have only one success. In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic @@ -517,8 +518,8 @@ module Goal : sig (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : (t -> unit tactic) -> unit tactic - (** Like {!enter}, but assumes exactly one goal under focus, raising *) - (** a fatal error otherwise. *) + (** Like {!enter}, but assumes exactly one goal under focus, raising + a fatal error otherwise. *) val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic (** Recover the list of current goals under focus, without evar-normalization. @@ -612,8 +613,10 @@ module Notations : sig (** {!tclBIND} *) val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic + (** {!tclTHEN} *) val (<*>) : unit tactic -> 'a tactic -> 'a tactic + (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) val (<+>) : 'a tactic -> 'a tactic -> 'a tactic diff --git a/engine/termops.ml b/engine/termops.ml index 98300764df..137770d8f0 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -197,8 +197,8 @@ let compute_evar_dependency_graph sigma = let evar_dependency_closure n sigma = let open Evd in - (** Create the DAG of depth [n] representing the recursive dependencies of - undefined evars. *) + (* Create the DAG of depth [n] representing the recursive dependencies of + undefined evars. *) let graph = compute_evar_dependency_graph sigma in let rec aux n curr accu = if Int.equal n 0 then Evar.Set.union curr accu @@ -209,9 +209,9 @@ let evar_dependency_closure n sigma = Evar.Set.union deps accu with Not_found -> accu in - (** Consider only the newly added evars *) + (* Consider only the newly added evars *) let ncurr = Evar.Set.fold fold curr Evar.Set.empty in - (** Merge the others *) + (* Merge the others *) let accu = Evar.Set.union curr accu in aux (n - 1) ncurr accu in @@ -261,13 +261,13 @@ let print_env_short env sigma = let pr_evar_constraints sigma pbs = let pr_evconstr (pbty, env, t1, t2) = let env = - (** We currently allow evar instances to refer to anonymous de - Bruijn indices, so we protect the error printing code in this - case by giving names to every de Bruijn variable in the - rel_context of the conversion problem. MS: we should rather - stop depending on anonymous variables, they can be used to - indicate independency. Also, this depends on a strategy for - naming/renaming. *) + (* We currently allow evar instances to refer to anonymous de + Bruijn indices, so we protect the error printing code in this + case by giving names to every de Bruijn variable in the + rel_context of the conversion problem. MS: we should rather + stop depending on anonymous variables, they can be used to + indicate independency. Also, this depends on a strategy for + naming/renaming. *) Namegen.make_all_name_different env sigma in print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++ diff --git a/engine/uState.ml b/engine/uState.ml index 6aecc368e6..05bef91f1e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -197,7 +197,7 @@ let process_universe_constraints ctx cstrs = | Some l -> Inr l in let equalize_variables fo l l' r r' local = - (** Assumes l = [l',0] and r = [r',0] *) + (* Assumes l = [l',0] and r = [r',0] *) let () = if is_local l' then instantiate_variable l' r vars @@ -235,8 +235,8 @@ let process_universe_constraints ctx cstrs = match cst with | ULe (l, r) -> if UGraph.check_leq univs l r then - (** Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) + (* Keep Prop/Set <= var around if var might be instantiated by prop or set + later. *) match Univ.Universe.level l, Univ.Universe.level r with | Some l, Some r -> Univ.Constraint.add (l, Univ.Le, r) local diff --git a/engine/univMinim.ml b/engine/univMinim.ml index e20055b133..1619ac3d34 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -32,15 +32,15 @@ let add_list_map u t map = let choose_canonical ctx flexible algs s = let global = LSet.diff s ctx in let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in - (** If there is a global universe in the set, choose it *) + (* If there is a global universe in the set, choose it *) if not (LSet.is_empty global) then let canon = LSet.choose global in canon, (LSet.remove canon global, rigid, flexible) - else (** No global in the equivalence class, choose a rigid one *) + else (* No global in the equivalence class, choose a rigid one *) if not (LSet.is_empty rigid) then let canon = LSet.choose rigid in canon, (global, LSet.remove canon rigid, flexible) - else (** There are only flexible universes in the equivalence + else (* There are only flexible universes in the equivalence class, choose a non-algebraic. *) let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in if not (LSet.is_empty nonalgs) then @@ -94,8 +94,8 @@ let find_inst insts v = with Found (f,l) -> (f,l) let compute_lbound left = - (** The universe variable was not fixed yet. - Compute its level using its lower bound. *) + (* The universe variable was not fixed yet. + Compute its level using its lower bound. *) let sup l lbound = match lbound with | None -> Some l @@ -154,9 +154,10 @@ let not_lower lower (d,l) = * constraints we must keep it. *) compare_constraint_type d d' > 0 with Not_found -> - (** No constraint existing on l *) true) l + (* No constraint existing on l *) true) l exception UpperBoundedAlg + (** [enforce_uppers upper lbound cstrs] interprets [upper] as upper constraints to [lbound], adding them to [cstrs]. @@ -269,7 +270,7 @@ module UPairSet = Set.Make (UPairs) let normalize_context_set g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in - (** Keep the Prop/Set <= i constraints separate for minimization *) + (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts in diff --git a/engine/univNames.ml b/engine/univNames.ml index 1019f8f0c2..39a9a8a3a5 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -37,8 +37,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty let name_universe lvl = - (** Best-effort naming from the string representation of the level. This is - completely hackish and should be solved in upper layers instead. *) + (* Best-effort naming from the string representation of the level. This is + completely hackish and should be solved in upper layers instead. *) Id.of_string_soft (Level.to_string lvl) let compute_instance_binders inst ubinders = diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 766e96fdfc..100fbc7271 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -10,6 +10,7 @@ exception Exc of Loc.t * exn for an error. This exception must not be raised by [raise] but rather by [Ploc.raise] (see below), to prevent the risk of several encapsulations of [Ploc.Exc]. *) + val raise : Loc.t -> exn -> 'a (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc], re-raise it (ignoring the new location [loc]), else raise the @@ -29,9 +30,11 @@ val sub : Loc.t -> int -> int -> Loc.t (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh] characters and with length [len]. The previous ending position of the location is lost. *) + val after : Loc.t -> int -> int -> Loc.t (** [Ploc.after loc sh len] is the location just after loc (starting at the end position of [loc]) shifted with [sh] characters and of length [len]. *) + val with_comment : Loc.t -> string -> Loc.t (** Change the comment part of the given location *) diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml index 91695e944e..8420d930d5 100644 --- a/ide/configwin_ihm.ml +++ b/ide/configwin_ihm.ml @@ -209,7 +209,8 @@ class ['a] list_selection_box () initializer - (** create the functions called when the buttons are clicked *) + + (* create the functions called when the buttons are clicked *) let f_add () = (* get the files to add with the function provided *) let l = add_function () in @@ -300,8 +301,10 @@ class string_param_box param (tt:GData.tooltips) = let _ = we#set_text (param.string_to_string param.string_value) in object (self) + (** This method returns the main box ready to be packed. *) method box = hbox#coerce + (** This method applies the new value of the parameter. *) method apply = let new_value = param.string_of_string we#text in @@ -347,9 +350,11 @@ class combo_param_box param (tt:GData.tooltips) = fun () -> wc#entry#text in object (self) + (** This method returns the main box ready to be packed. *) method box = hbox#coerce - (** This method applies the new value of the parameter. *) + + (** This method applies the new value of the parameter. *) method apply = let new_value = get_value () in if new_value <> param.combo_value then @@ -404,8 +409,10 @@ class text_param_box param (tt:GData.tooltips) = let _ = dbg "text_param_box: object(self)" in object (self) val wview = wview + (** This method returns the main box ready to be packed. *) method box = wf#coerce + (** This method applies the new value of the parameter. *) method apply = let v = param.string_of_string (buffer#get_text ()) in @@ -435,8 +442,10 @@ class bool_param_box param (tt:GData.tooltips) = let _ = wchk#misc#set_sensitive param.bool_editable in object (self) + (** This method returns the check button ready to be packed. *) method box = wchk#coerce + (** This method applies the new value of the parameter. *) method apply = let new_value = wchk#active in @@ -471,8 +480,10 @@ class modifiers_param_box param = tooltips#set_tip wev#coerce ~text: help ~privat: help in object (self) + (** This method returns the main box ready to be packed. *) method box = hbox#coerce + (** This method applies the new value of the parameter. *) method apply = let new_value = !value in @@ -500,8 +511,10 @@ class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) = in object (self) + (** This method returns the main box ready to be packed. *) method box = frame_selection#box#coerce + (** This method applies the new value of the parameter. *) method apply = param.list_f_apply !listref ; diff --git a/ide/coq.ml b/ide/coq.ml index 88ffb4f0b7..91cd448eda 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -334,8 +334,8 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = (* Parsing error at the end of s : we have only received a part of an xml answer. We store the current fragment for later *) let l_end = Lexing.lexeme_end lex in - (** Heuristic hack not to reimplement the lexer: if ever the lexer dies - twice at the same place, then this is a non-recoverable error *) + (* Heuristic hack not to reimplement the lexer: if ever the lexer dies + twice at the same place, then this is a non-recoverable error *) if state.lexerror = Some l_end then raise e; state.lexerror <- Some l_end @@ -496,7 +496,7 @@ let init_coqtop coqtop task = type 'a query = 'a Interface.value task let eval_call call handle k = - (** Send messages to coqtop and prepare the decoding of the answer *) + (* Send messages to coqtop and prepare the decoding of the answer *) Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call); assert (handle.alive && handle.waiting_for = None); handle.waiting_for <- Some (mk_ccb (call,k)); diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6c3438a4b0..8da9900724 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -255,8 +255,8 @@ object(self) let sentence = Doc.find document find in let mark = sentence.start in let iter = script#buffer#get_iter_at_mark mark in - (** Sentence starts tend to be at the end of a line, so we rather choose - the first non-line-ending position. *) + (* Sentence starts tend to be at the end of a line, so we rather choose + the first non-line-ending position. *) let rec sentence_start iter = if iter#ends_line then sentence_start iter#forward_line else iter diff --git a/ide/coqide.ml b/ide/coqide.ml index 40b8d2f484..48c08899e0 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -566,7 +566,7 @@ let update_status sn = Coq.bind (Coq.status false) next let find_next_occurrence ~backward sn = - (** go to the next occurrence of the current word, forward or backward *) + (* go to the next occurrence of the current word, forward or backward *) let b = sn.buffer in let start = find_word_start (b#get_iter_at_mark `INSERT) in let stop = find_word_end start in @@ -613,11 +613,11 @@ let printopts_callback opts v = (** Templates menu *) let get_current_word term = - (** First look to find if autocompleting *) + (* First look to find if autocompleting *) match term.script#complete_popup#proposal with | Some p -> p | None -> - (** Then look at the current selected word *) + (* Then look at the current selected word *) let buf1 = term.script#buffer in let buf2 = term.proof#buffer in if buf1#has_selection then @@ -628,7 +628,7 @@ let get_current_word term = buf2#get_text ~slice:true ~start ~stop () else if term.messages#has_selection then term.messages#get_selected_text - (** Otherwise try to find the word around the cursor *) + (* Otherwise try to find the word around the cursor *) else let it = term.script#buffer#get_iter_at_mark `INSERT in let start = find_word_start it in @@ -772,11 +772,11 @@ let uncomment = cb_on_current_term (fun t -> t.script#uncomment ()) let coqtop_arguments sn = let dialog = GWindow.dialog ~title:"Coqtop arguments" () in let coqtop = sn.coqtop in - (** Text entry *) + (* Text entry *) let args = Coq.get_arguments coqtop in let text = String.concat " " args in let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in - (** Buttons *) + (* Buttons *) let box = dialog#action_area in let ok = GButton.button ~stock:`OK ~packing:box#add () in let ok_cb () = diff --git a/ide/idetop.ml b/ide/idetop.ml index a2b85041e8..8b3b566f9c 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -263,9 +263,9 @@ let wait () = set_doc (Stm.wait ~doc) let status force = - (** We remove the initial part of the current [DirPath.t] - (usually Top in an interactive session, cf "coqtop -top"), - and display the other parts (opened sections and modules) *) + (* We remove the initial part of the current [DirPath.t] + (usually Top in an interactive session, cf "coqtop -top"), + and display the other parts (opened sections and modules) *) set_doc (Stm.finish ~doc:(get_doc ())); if force then set_doc (Stm.join ~doc:(get_doc ())); @@ -408,14 +408,12 @@ let interp ((_raw, verbose), s) = (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer before exiting. *) - let quit = ref false (** Disabled *) let print_ast id = Xml_datatype.PCData "ERROR" (** Grouping all call handlers together + error handling *) - let eval_call c = let interruptible f x = catch_break := true; diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 7044263b94..c14af7d21d 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -43,10 +43,10 @@ color on Windows. A clean fix, if ever needed, would be to combine the attribut of the tags into a single composite tag before applying. This is left as an exercise for the reader. *) let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = - (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that - it has to reimplement its own helper function. Unluckily, it relies on - a slow algorithm, so that we have to have our own quicker version here. - Alas, it is still much slower than the native version... *) + (* FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text else let it = buf#get_iter_at_mark mark in diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index debbc8301e..ccb6bedaf6 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -78,16 +78,20 @@ type option_state = { } type search_constraint = -(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) | Name_Pattern of string -(** Whether the object type satisfies a pattern *) +(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) + | Type_Pattern of string -(** Whether some subtype of object type satisfies a pattern *) +(** Whether the object type satisfies a pattern *) + | SubType_Pattern of string -(** Whether the object pertains to a module *) +(** Whether some subtype of object type satisfies a pattern *) + | In_Module of string list -(** Bypass the Search blacklist *) +(** Whether the object pertains to a module *) + | Include_Blacklist +(** Bypass the Search blacklist *) (** A list of search constraints; the boolean flag is set to [false] whenever the flag should be negated. *) diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml index 19e9799c19..b2ce55e89a 100644 --- a/ide/protocol/richpp.ml +++ b/ide/protocol/richpp.ml @@ -46,7 +46,7 @@ let rich_pp width ppcmds = let pp_buffer = Buffer.create 180 in let push_pcdata () = - (** Push the optional PCData on the above node *) + (* Push the optional PCData on the above node *) let len = Buffer.length pp_buffer in if len = 0 then () else match context.stack with @@ -77,7 +77,7 @@ let rich_pp width ppcmds = let xml = Element (node, annotation, List.rev child) in match ctx with | Leaf -> - (** Final node: we keep the result in a dummy context *) + (* Final node: we keep the result in a dummy context *) context.stack <- Node ("", [xml], 0, Leaf) | Node (node, child, pos, ctx) -> context.stack <- Node (node, xml :: child, pos, ctx) @@ -104,15 +104,15 @@ let rich_pp width ppcmds = pp_set_max_boxes ft 50 ; pp_set_ellipsis_text ft "..."; - (** The whole output must be a valid document. To that - end, we nest the document inside <pp> tags. *) + (* The whole output must be a valid document. To that + end, we nest the document inside <pp> tags. *) pp_open_box ft 0; pp_open_tag ft "pp"; Pp.(pp_with ft ppcmds); pp_close_tag ft (); pp_close_box ft (); - (** Get the resulting XML tree. *) + (* Get the resulting XML tree. *) let () = pp_print_flush ft () in let () = assert (Buffer.length pp_buffer = 0) in match context.stack with diff --git a/ide/sentence.ml b/ide/sentence.ml index 2f7820a77c..2e508969aa 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -91,8 +91,8 @@ let tag_on_insert buffer = in try let start = grab_sentence_start prev soi in - (** The status of "{" "}" as sentence delimiters is too fragile. - We retag up to the next "." instead. *) + (* The status of "{" "}" as sentence delimiters is too fragile. + We retag up to the next "." instead. *) let stop = grab_ending_dot insert in try split_slice_lax buffer start#backward_char stop with Coq_lex.Unterminated -> diff --git a/ide/session.ml b/ide/session.ml index be2bfe060c..805e1d38a7 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -217,7 +217,7 @@ let set_buffer_handlers | Some s -> Minilib.log (s^" moved") | None -> () in - (** Pluging callbacks *) + (* Pluging callbacks *) let _ = buffer#connect#insert_text ~callback:insert_cb in let _ = buffer#connect#delete_range ~callback:delete_cb in let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in @@ -427,7 +427,7 @@ let build_layout (sn:session) = GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) () in - (** Right part of the window. *) + (* Right part of the window. *) let eval_paned = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(session_box#pack ~expand:true) () in @@ -438,7 +438,7 @@ let build_layout (sn:session) = let state_paned = GPack.paned `VERTICAL ~packing:eval_paned#add2 () in - (** Proof buffer. *) + (* Proof buffer. *) let title = Printf.sprintf "Proof (%s)" sn.tab_label#text in let proof_detachable = Wg_Detachable.detachable ~title () in @@ -454,7 +454,7 @@ let build_layout (sn:session) = let proof_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_detachable#pack () in - (** Message buffer. *) + (* Message buffer. *) let message_frame = GPack.notebook ~packing:state_paned#add () in let add_msg_page pos name text (w : GObj.widget) = @@ -514,14 +514,14 @@ let build_layout (sn:session) = let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#default_route#coerce in let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in - (** When a message is received, focus on the message pane *) + (* When a message is received, focus on the message pane *) let _ = sn.messages#default_route#connect#pushed ~callback:(fun _ _ -> let num = message_frame#page_num detach#coerce in if 0 <= num then message_frame#goto_page num ) in - (** When an error occurs, paint the error label in red *) + (* When an error occurs, paint the error label in red *) let txt = label#text in let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in sn.errpage#on_update ~callback:(fun l -> diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 6a9317bc2f..c39d6d0563 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -40,7 +40,7 @@ let get_syntactic_completion (buffer : GText.buffer) pattern accu = (** Retrieve completion proposals in Coq libraries *) let get_semantic_completion pattern accu = let flags = [Interface.Name_Pattern ("^" ^ pattern), true] in - (** Only get the last part of the qualified name *) + (* Only get the last part of the qualified name *) let rec last accu = function | [] -> accu | [basename] -> Proposals.add basename accu @@ -199,15 +199,15 @@ object (self) let () = self#init_proposals w props in update_completion_signal#call (start_offset, w, props) in - (** If not in the cache, we recompute it: first syntactic *) + (* If not in the cache, we recompute it: first syntactic *) let synt = get_syntactic_completion buffer w Proposals.empty in - (** Then semantic *) + (* Then semantic *) let next prop = let () = update prop in Coq.lift k in let query = Coq.bind (get_semantic_completion w synt) next in - (** If coqtop is computing, do the syntactic completion altogether *) + (* If coqtop is computing, do the syntactic completion altogether *) let occupied () = let () = update synt in k () @@ -264,20 +264,20 @@ object (self) renderer#set_properties [`FONT_DESC font; `XPAD 10] method private coordinates pos = - (** Toplevel position w.r.t. screen *) + (* Toplevel position w.r.t. screen *) let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in - (** Position of view w.r.t. window *) + (* Position of view w.r.t. window *) let (ux, uy) = Gdk.Window.get_position view#misc#window in - (** Relative buffer position to view *) + (* Relative buffer position to view *) let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in - (** Iter position *) + (* Iter position *) let iter = view#buffer#get_iter pos in let coords = view#get_iter_location iter in let lx = Gdk.Rectangle.x coords in let ly = Gdk.Rectangle.y coords in let w = Gdk.Rectangle.width coords in let h = Gdk.Rectangle.height coords in - (** Absolute position *) + (* Absolute position *) (x + lx + ux - dx, y + ly + uy - dy, w, h) method private select_any f = @@ -374,9 +374,9 @@ object (self) else None method private manage_scrollbar () = - (** HACK: we don't have access to the treeview size because of the lack of - LablGTK binding for certain functions, so we bypass it by approximating - it through the size of the proposals *) + (* HACK: we don't have access to the treeview size because of the lack of + LablGTK binding for certain functions, so we bypass it by approximating + it through the size of the proposals *) let height = match model#store#get_iter_first with | None -> -1 | Some iter -> @@ -434,18 +434,18 @@ object (self) else false else false in - (** Style handling *) + (* Style handling *) let _ = view#misc#connect#style_set ~callback:self#refresh_style in let _ = self#refresh_style () in let _ = data#set_resize_mode `PARENT in let _ = frame#set_resize_mode `PARENT in - (** Callback to model *) + (* Callback to model *) let _ = model#connect#start_completion ~callback:self#start_callback in let _ = model#connect#update_completion ~callback:self#update_callback in let _ = model#connect#end_completion ~callback:self#end_callback in - (** Popup interaction *) + (* Popup interaction *) let _ = view#event#connect#key_press ~callback:key_cb in - (** Hiding the popup when necessary*) + (* Hiding the popup when necessary*) let _ = view#misc#connect#hide ~callback:obj#misc#hide in let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in let _ = view#connect#move_cursor ~callback:move_cb in diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index 296a942321..7d2d7da570 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -212,13 +212,13 @@ class finder name (view : GText.view) = initializer let _ = self#hide () in - (** Widget button interaction *) + (* Widget button interaction *) let _ = next_button#connect#clicked ~callback:self#find_forward in let _ = previous_button#connect#clicked ~callback:self#find_backward in let _ = replace_button#connect#clicked ~callback:self#replace in let _ = replace_all_button#connect#clicked ~callback:self#replace_all in - (** Keypress interaction *) + (* Keypress interaction *) let generic_cb esc_cb ret_cb ev = let ev_key = GdkEvent.Key.keyval ev in let (return, _) = GtkData.AccelGroup.parse "Return" in @@ -232,7 +232,7 @@ class finder name (view : GText.view) = let _ = find_entry#event#connect#key_press ~callback:find_cb in let _ = replace_entry#event#connect#key_press ~callback:replace_cb in - (** TextView interaction *) + (* TextView interaction *) let view_cb ev = if widget#visible then let ev_key = GdkEvent.Key.keyval ev in diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index a79a093e32..6b09b344b5 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -36,6 +36,7 @@ class type message_view = method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) + method has_selection : bool method get_selected_text : string end diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 472aaf5ed4..613f1b4190 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -26,6 +26,7 @@ class type message_view = method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) + method has_selection : bool method get_selected_text : string end diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 74bc0b8d53..5e26c50797 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -152,11 +152,11 @@ object(self) if self#process_delete_action del then (`OK, `WRITE) else (`FAIL, `NOOP) | Action lst -> let fold accu action = match accu with - | (`FAIL, _) -> accu (** we stop now! *) + | (`FAIL, _) -> accu (* we stop now! *) | (`OK, status) -> let (res, nstatus) = self#process_action action in let merge op1 op2 = match op1, op2 with - | `NOOP, `NOOP -> `NOOP (** only a noop when both are *) + | `NOOP, `NOOP -> `NOOP (* only a noop when both are *) | _ -> `WRITE in (res, merge status nstatus) @@ -172,8 +172,8 @@ object(self) | (`OK, _) -> history <- rem; redo <- (negate_action action) :: redo - | (`FAIL, `NOOP) -> () (** we do nothing *) - | (`FAIL, `WRITE) -> self#clear_undo () (** we don't know how we failed, so start off *) + | (`FAIL, `NOOP) -> () (* we do nothing *) + | (`FAIL, `WRITE) -> self#clear_undo () (* we don't know how we failed, so start off *) end method perform_redo () = match redo with @@ -184,8 +184,8 @@ object(self) | (`OK, _) -> redo <- rem; history <- (negate_action action) :: history; - | (`FAIL, `NOOP) -> () (** we do nothing *) - | (`FAIL, `WRITE) -> self#clear_undo () (** we don't know how we failed *) + | (`FAIL, `NOOP) -> () (* we do nothing *) + | (`FAIL, `WRITE) -> self#clear_undo () (* we don't know how we failed *) end method undo () = @@ -212,9 +212,9 @@ object(self) self#with_lock_undo self#process_begin_user_action () method process_end_user_action () = - (** Search for the pending action *) + (* Search for the pending action *) let rec split accu = function - | [] -> raise Not_found (** no pending begin action! *) + | [] -> raise Not_found (* no pending begin action! *) | EndGrp :: rem -> let grp = List.rev accu in let rec flatten = function @@ -240,7 +240,7 @@ object(self) (* Save the insert action *) let len = Glib.Utf8.length s in let mergeable = - (** heuristic: split at newline and atomic pastes *) + (* heuristic: split at newline and atomic pastes *) len = 1 && (s <> "\n") in let ins = { @@ -460,7 +460,7 @@ object (self) if not proceed then GtkSignal.stop_emit () in let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in - (** Plug on preferences *) + (* Plug on preferences *) let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in let _ = background_color#connect#changed ~callback:cb in let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index 0f5ed8d896..3b2572f9d2 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -70,7 +70,7 @@ object (self) let cb rect = let w = rect.Gtk.width in let h = rect.Gtk.height in - (** Only refresh when size actually changed, otherwise loops *) + (* Only refresh when size actually changed, otherwise loops *) if self#misc#visible && (width <> w || height <> h) then begin width <- w; height <- h; @@ -91,7 +91,7 @@ object (self) let _ = eventbox#event#connect#button_press ~callback:clicked_cb in let cb show = if show then self#misc#show () else self#misc#hide () in stick show_progress_bar self cb; - (** Initial pixmap *) + (* Initial pixmap *) draw#set_pixmap pixmap; refresh_timer.Ideutils.run ~ms:300 ~callback:(fun () -> if need_refresh then self#refresh (); true) diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 77d612cfd9..757d186c8b 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -80,8 +80,8 @@ type cases_pattern_expr_r = and cases_pattern_expr = cases_pattern_expr_r CAst.t and cases_pattern_notation_substitution = - cases_pattern_expr list * (** for constr subterms *) - cases_pattern_expr list list (** for recursive notations *) + cases_pattern_expr list * (* for constr subterms *) + cases_pattern_expr list list (* for recursive notations *) and constr_expr_r = | CRef of qualid * instance_expr option @@ -142,10 +142,10 @@ and local_binder_expr = | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t and constr_notation_substitution = - constr_expr list * (** for constr subterms *) - constr_expr list list * (** for recursive notations *) - cases_pattern_expr list * (** for binders *) - local_binder_expr list list (** for binder lists (recursive notations) *) + constr_expr list * (* for constr subterms *) + constr_expr list list * (* for recursive notations *) + cases_pattern_expr list * (* for binders *) + local_binder_expr list list (* for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3a4969a3ee..3a5af1dd5f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 = in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> - (** Don't care about the case_style *) + (* Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 @@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) + (* Don't care about the [binder_kind] *) List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) (** Folds and maps *) - let is_constructor id = try Globnames.isConstructRef (Smartlocate.global_of_extended_global diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fba03b9de9..0d0b6158d9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -960,7 +960,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GSort s -> CSort (extern_glob_sort s) - | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *) + | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) | GCast (c, c') -> CCast (sub_extern true scopes vars c, diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6313f2d7ba..40922b5c35 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1507,7 +1507,7 @@ let drop_notations_pattern looked_for genv = let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in - (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) + (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes)) | GHole (_,_,_) -> RCPatAtom (None) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 035e4bc644..61acd09d65 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -45,13 +45,15 @@ type var_internalization_type = type var_internalization_data = var_internalization_type * - (** type of the "free" variable, for coqdoc, e.g. while typing the - constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) + (* type of the "free" variable, for coqdoc, e.g. while typing the + constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) + Id.t list * - (** impargs to automatically add to the variable, e.g. for "JMeq A a B b" - in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Impargs.implicit_status list * (** signature of impargs of the variable *) - Notation_term.scope_name option list (** subscopes of the args of the variable *) + (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" + in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) + + Impargs.implicit_status list * (* signature of impargs of the variable *) + Notation_term.scope_name option list (* subscopes of the args of the variable *) (** A map of free variables to their implicit arguments and scopes *) type internalization_env = var_internalization_data Id.Map.t diff --git a/interp/declare.ml b/interp/declare.ml index 1e972d3e35..a61078705a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) = (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = - (** Never open a local definition *) + (* Never open a local definition *) if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in @@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e export_seff || not de.const_entry_opaque || is_poly de -> - (** This globally defines the side-effects in the environment. We mark - exported constants as being side-effect not to redeclare them at - caching time. *) + (* This globally defines the side-effects in the environment. We mark + exported constants as being side-effect not to redeclare them at + caching time. *) let de, export = Global.export_private_constants ~in_section de in export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) @@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest) (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) - type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) @@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let (de, eff) = Global.export_private_constants ~in_section:true de in let () = List.iter register_side_effect eff in - (** The body should already have been forced upstream because it is a - section-local definition, but it's not enforced by typing *) + (* The body should already have been forced upstream because it is a + section-local definition, but it's not enforced by typing *) let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in - (** We must declare the universe constraints before type-checking the - term. *) + (* We must declare the universe constraints before type-checking the + term. *) let () = Global.push_context_set (not poly) univs in let se = { secdef_body = body; @@ -262,7 +261,6 @@ let declare_variable id obj = oname (** Declaration of inductive blocks *) - let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); @@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let id = Label.to_id label in let univs = match univs with | Monomorphic_ind_entry _ -> - (** Global constraints already defined through the inductive *) + (* Global constraints already defined through the inductive *) Monomorphic_const_entry Univ.ContextSet.empty | Polymorphic_ind_entry (nas, ctx) -> Polymorphic_const_entry (nas, ctx) @@ -511,7 +509,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = load_function = load_univ_names; open_function = open_univ_names; discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); + subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } let declare_univ_binders gr pl = diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 931d05a975..554da7603f 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -18,6 +18,7 @@ val dump : unit -> bool val noglob : unit -> unit val dump_into_file : string -> unit (** special handling of "stdout" *) + val dump_to_dotglob : unit -> unit val feedback_glob : unit -> unit diff --git a/interp/impargs.ml b/interp/impargs.ml index d024a9e808..8a89bcdf26 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -448,7 +448,7 @@ let compute_mib_implicits flags kn = Array.to_list (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> - (** No need to care about constraints here *) + (* No need to care about constraints here *) let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in diff --git a/interp/impargs.mli b/interp/impargs.mli index ea5aa90f68..4afc2af5e9 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -65,6 +65,7 @@ type implicit_explanation = operational only if [conclusion_matters] is true. *) type maximal_insertion = bool (** true = maximal contextual insertion *) + type force_inference = bool (** true = always infer, never turn into evar/subgoal *) type implicit_status = (Id.t * implicit_explanation * diff --git a/interp/notation.ml b/interp/notation.ml index 0af75b5bfa..e17cc65042 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -308,7 +308,7 @@ let declare_delimiters scope key = | None -> scope_map := String.Map.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - (** FIXME: implement multikey scopes? *) + (* FIXME: implement multikey scopes? *) Flags.if_verbose Feedback.msg_info (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map diff --git a/interp/notation.mli b/interp/notation.mli index 3480d1c8f2..ab0501a1e1 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool (** Open scope *) val open_close_scope : - (** locality *) bool * (* open *) bool * scope_name -> unit + (* locality *) bool * (* open *) bool * scope_name -> unit (** Extend a list of scopes *) val empty_scope_stack : scopes diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7a525f84a5..55a87fcd4d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | _ -> false) | NApp (t1, a1), NApp (t2, a2) -> (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *) | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 && b1 == b2 @@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> Name.equal na1 na2 && eq_notation_constr vars b1 b2 && Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && (eq_notation_constr vars) t1 t2 @@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Option.equal (eq_notation_constr vars) o1 o2 && (eq_notation_constr vars) u1 u2 && (eq_notation_constr vars) r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) let eq (na1, o1, t1) (na2, o2, t2) = Name.equal na1 na2 && Option.equal (eq_notation_constr vars) o1 o2 && diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5fb0ca1b43..0ef1f267f6 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -20,13 +20,13 @@ open Glob_term as well as non global expressions such as existential variables. *) type notation_constr = - (** Part common to [glob_constr] and [cases_pattern] *) + (* Part common to [glob_constr] and [cases_pattern] *) | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - (** Part only in [glob_constr] *) + (* Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool diff --git a/kernel/.merlin.in b/kernel/.merlin.in index 912ff61496..29da7d2cf6 100644 --- a/kernel/.merlin.in +++ b/kernel/.merlin.in @@ -1,4 +1,4 @@ -FLG -rectypes -thread -safe-string -w +a-4-44-50 +FLG -rectypes -thread -safe-string -w +a-4-44 S ../clib B ../clib diff --git a/lib/control.ml b/lib/control.ml index 3fbeb168c4..e09068740d 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -62,8 +62,8 @@ let windows_timeout n f x e = let res = f x in let () = killed := true in let cur = Unix.gettimeofday () in - (** The thread did not interrupt, but the computation took longer than - expected. *) + (* The thread did not interrupt, but the computation took longer than + expected. *) let () = if float_of_int n <= cur -. init then begin exited := true; raise Sys.Break @@ -71,7 +71,7 @@ let windows_timeout n f x e = res with | Sys.Break -> - (** Just in case, it could be a regular Ctrl+C *) + (* Just in case, it could be a regular Ctrl+C *) if not !exited then begin killed := true; raise Sys.Break end else raise e | e -> diff --git a/lib/system.mli b/lib/system.mli index f13fd30923..a3b79ee528 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -102,6 +102,7 @@ type time val get_time : unit -> time val time_difference : time -> time -> float (** in seconds *) + val fmt_time_difference : time -> time -> Pp.t val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b diff --git a/library/coqlib.mli b/library/coqlib.mli index 351a0a7e84..f6779dbbde 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -190,12 +190,18 @@ val build_bool_type : coq_bool_data delayed val build_prod : coq_sigma_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] -val build_coq_eq : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] -val build_coq_eq_refl : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *) +(** = [(build_coq_eq_data()).eq] *) + +val build_coq_eq_refl : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] -val build_coq_eq_sym : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *) +(** = [(build_coq_eq_data()).refl] *) + +val build_coq_eq_sym : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] +(** = [(build_coq_eq_data()).sym] *) + val build_coq_f_equal2 : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] @@ -222,8 +228,8 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed val build_coq_sumbool : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] -(** {6 ... } *) -(** Connectives +(** {6 ... } + Connectives The False proposition *) val build_coq_False : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] diff --git a/library/decls.mli b/library/decls.mli index 401884736e..c0db537427 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -19,7 +19,7 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - DirPath.t * bool (** opacity *) * Univ.ContextSet.t * polymorphic * logical_kind + DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t diff --git a/library/goptions.ml b/library/goptions.ml index 98efb512ab..340d74151b 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -246,14 +246,14 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) | OptGlobal -> cache_options o | OptExport -> () | OptLocal | OptDefault -> - (** Ruled out by classify_function *) + (* Ruled out by classify_function *) assert false in let open_options i (_, (l, _, _) as o) = match l with | OptExport -> if Int.equal i 1 then cache_options o | OptGlobal -> () | OptLocal | OptDefault -> - (** Ruled out by classify_function *) + (* Ruled out by classify_function *) assert false in let subst_options (subst,obj) = obj in diff --git a/library/lib.ml b/library/lib.ml index 9c13cdafdb..cce5feeb4a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -481,8 +481,8 @@ let named_of_variable_context = List.map fst let name_instance inst = - (** FIXME: this should probably be done at an upper level, by storing the - name information in the section data structure. *) + (* FIXME: this should probably be done at an upper level, by storing the + name information in the section data structure. *) let map lvl = match Univ.Level.name lvl with | None -> (* Having Prop/Set/Var as section universes makes no sense *) assert false @@ -491,8 +491,8 @@ let name_instance inst = let qid = Nametab.shortest_qualid_of_universe na in Name (Libnames.qualid_basename qid) with Not_found -> - (** Best-effort naming from the string representation of the level. - See univNames.ml for a similar hack. *) + (* Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) Name (Id.of_string_soft (Univ.Level.to_string lvl)) in Array.map map (Univ.Instance.to_array inst) diff --git a/library/libnames.mli b/library/libnames.mli index 9960603cbb..bbb4d2a058 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -94,8 +94,8 @@ val qualid_basename : qualid -> Id.t val default_library : DirPath.t (** This is the root of the standard library of Coq *) -val coq_root : module_ident (** "Coq" *) -val coq_string : string (** "Coq" *) +val coq_root : module_ident (* "Coq" *) +val coq_string : string (* "Coq" *) (** This is the default root prefix for developments which doesn't mention a root *) diff --git a/library/library.mli b/library/library.mli index d298a371b5..c016352808 100644 --- a/library/library.mli +++ b/library/library.mli @@ -19,8 +19,8 @@ open Libnames written at various dates. *) -(** {6 ... } *) -(** Require = load in the environment + open (if the optional boolean +(** {6 ... } + Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit diff --git a/library/nametab.ml b/library/nametab.ml index e29c7b2960..503cf515d5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -107,6 +107,7 @@ module type NAMETREE = sig val user_name : qualid -> t -> user_name val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list + (** Matches a prefix of [qualid], useful for completion *) val match_prefixes : qualid -> t -> elt list end diff --git a/library/nametab.mli b/library/nametab.mli index 24af07619d..78d0f83b6e 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -173,7 +173,9 @@ val exists_cci : full_path -> bool val exists_modtype : full_path -> bool val exists_dir : DirPath.t -> bool val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) + val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) + val exists_universe : full_path -> bool (** {6 These functions locate qualids into full user names } *) diff --git a/library/summary.ml b/library/summary.ml index 9b22945919..b68f1fb01b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -92,7 +92,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } = | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module end; - (** We must be independent on the order of the map! *) + (* We must be independent on the order of the map! *) let ufz name decl = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> diff --git a/library/summary.mli b/library/summary.mli index 7d91a79188..64222761ba 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -19,9 +19,9 @@ type marshallable = (** Types of global Coq states. The ['a] type should be pure and marshallable by the standard OCaml marshalling function. *) type 'a summary_declaration = { - (** freeze_function [true] is for marshalling to disk. - * e.g. lazy must be forced *) freeze_function : marshallable -> 'a; + (** freeze_function [true] is for marshalling to disk. + * e.g. lazy must be forced *) unfreeze_function : 'a -> unit; init_function : unit -> unit } diff --git a/parsing/extend.ml b/parsing/extend.ml index 050ed49622..9b5537d7f6 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -106,11 +106,11 @@ type 'a production_rule = type 'a single_extend_statement = string option * - (** Level *) + (* Level *) Gramlib.Gramext.g_assoc option * - (** Associativity *) + (* Associativity *) 'a production_rule list - (** Symbol list with the interpretation function *) + (* Symbol list with the interpretation function *) type 'a extend_statement = Gramlib.Gramext.position option * diff --git a/parsing/tok.mli b/parsing/tok.mli index 9b8c008555..55fcd33272 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -27,6 +27,7 @@ val to_string : t -> string (* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool + (** for camlp5 *) val of_pattern : string*string -> t val to_pattern : t -> string*string diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 480819ebe1..6f9384941b 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -27,12 +27,12 @@ let start_deriving f suchthat lemma = let sigma = Evd.from_env env in let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - (** create a sort variable for the type of [f] *) + (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one that looked the most general. *) let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in let f_type_type = EConstr.mkSort f_type_sort in - (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) + (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> @@ -45,14 +45,14 @@ let start_deriving f suchthat lemma = TNil sigma)))))) in - (** The terminator handles the registering of constants when the proof is closed. *) + (* The terminator handles the registering of constants when the proof is closed. *) let terminator com = let open Proof_global in - (** Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) + (* Extracts the relevant information from the proof. [Admitted] + and [Save] result in user errors. [opaque] is [true] if the + proof was concluded by [Qed], and [false] if [Defined]. [f_def] + and [lemma_def] correspond to the proof of [f] and of + [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") @@ -64,26 +64,26 @@ let start_deriving f suchthat lemma = opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in - (** The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) let f_def = { f_def with Entries.const_entry_opaque = false } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in let f_kn_term = mkConst f_kn in - (** In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in - (** Extracts the type of the proof of [suchthat]. *) + (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = match Entries.(lemma_def.const_entry_type) with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in - (** The references of [f] are subsituted appropriately. *) + (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in - (** The same is done in the body of the proof. *) + (* The same is done in the body of the proof. *) let lemma_body = map_const_entry_body substf Entries.(lemma_def.const_entry_body) in @@ -105,7 +105,3 @@ let start_deriving f suchthat lemma = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end in () - - - - diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index 9c0f373c6a..c675eacc92 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -20,8 +20,10 @@ type big_int = Big_int.big_int let zero = zero_big_int (** The big integer [0]. *) + let one = unit_big_int (** The big integer [1]. *) + let two = big_int_of_int 2 (** The big integer [2]. *) @@ -29,28 +31,39 @@ let two = big_int_of_int 2 let opp = minus_big_int (** Unary negation. *) + let abs = abs_big_int (** Absolute value. *) + let add = add_big_int (** Addition. *) + let succ = succ_big_int (** Successor (add 1). *) + let add_int = add_int_big_int (** Addition of a small integer to a big integer. *) + let sub = sub_big_int (** Subtraction. *) + let pred = pred_big_int (** Predecessor (subtract 1). *) + let mult = mult_big_int (** Multiplication of two big integers. *) + let mult_int = mult_int_big_int (** Multiplication of a big integer by a small integer *) + let square = square_big_int (** Return the square of the given big integer *) + let sqrt = sqrt_big_int (** [sqrt_big_int a] returns the integer square root of [a], that is, the largest big integer [r] such that [r * r <= a]. Raise [Invalid_argument] if [a] is negative. *) + let quomod = quomod_big_int (** Euclidean division of two big integers. The first part of the result is the quotient, @@ -58,14 +71,18 @@ let quomod = quomod_big_int Writing [(q,r) = quomod_big_int a b], we have [a = q * b + r] and [0 <= r < |b|]. Raise [Division_by_zero] if the divisor is zero. *) + let div = div_big_int (** Euclidean quotient of two big integers. This is the first result [q] of [quomod_big_int] (see above). *) + let modulo = mod_big_int (** Euclidean modulus of two big integers. This is the second result [r] of [quomod_big_int] (see above). *) + let gcd = gcd_big_int (** Greatest common divisor of two big integers. *) + let power = power_big_int_positive_big_int (** Exponentiation functions. Return the big integer representing the first argument [a] raised to the power [b] @@ -78,18 +95,22 @@ let power = power_big_int_positive_big_int let sign = sign_big_int (** Return [0] if the given big integer is zero, [1] if it is positive, and [-1] if it is negative. *) + let compare = compare_big_int (** [compare_big_int a b] returns [0] if [a] and [b] are equal, [1] if [a] is greater than [b], and [-1] if [a] is smaller than [b]. *) + let eq = eq_big_int let le = le_big_int let ge = ge_big_int let lt = lt_big_int let gt = gt_big_int (** Usual boolean comparisons between two big integers. *) + let max = max_big_int (** Return the greater of its two arguments. *) + let min = min_big_int (** Return the smaller of its two arguments. *) @@ -98,6 +119,7 @@ let min = min_big_int let to_string = string_of_big_int (** Return the string representation of the given big integer, in decimal (base 10). *) + let of_string = big_int_of_string (** Convert a string to a big integer, in decimal. The string consists of an optional [-] or [+] sign, @@ -107,6 +129,7 @@ let of_string = big_int_of_string let of_int = big_int_of_int (** Convert a small integer to a big integer. *) + let is_int = is_int_big_int (** Test whether the given big integer is small enough to be representable as a small integer (type [int]) @@ -115,6 +138,7 @@ let is_int = is_int_big_int [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform, [is_int_big_int a] returns [true] if and only if [a] is between -2{^62} and 2{^62}-1. *) + let to_int = int_of_big_int (** Convert a big integer to a small integer (type [int]). Raises [Failure "int_of_big_int"] if the big integer diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bdeb6fca60..59c57cc544 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -125,7 +125,7 @@ module KOrd = struct type t = kind * string let compare (k1, s1) (k2, s2) = - let c = Pervasives.compare k1 k2 (** OK *) in + let c = Pervasives.compare k1 k2 (* OK *) in if c = 0 then String.compare s1 s2 else c end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 4cdfc6fac5..12b68e208c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -41,7 +41,7 @@ let pop t = Vars.lift (-1) t *) let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let princ_type = EConstr.of_constr princ_type in - let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in + let princ_type_info = compute_elim_sig Evd.empty princ_type (* FIXME *) in let env = Global.env () in let env_with_params = EConstr.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 603dd60cf2..ec2adf065a 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -306,8 +306,8 @@ let add_rewrite_hint ~poly bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (** This is a global universe context that shouldn't be - refreshed at every use of the hint, declare it globally. *) + else (* This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) (Declare.declare_universe_context false ctx; Univ.ContextSet.empty) in @@ -738,7 +738,8 @@ let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - (** FIXME: this looks really wrong. Does anybody really use this tactic? *) + (* FIXME: this looks really wrong. Does anybody really use + this tactic? *) let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in change_concl c end; diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index ef18dd6cdc..1ea6ff84d4 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -24,7 +24,7 @@ let (set_default_tactic, get_default_tactic, print_default_tactic) = Tactic_option.declare_tactic_option "Program tactic" let () = - (** Delay to recover the tactic imperatively *) + (* Delay to recover the tactic imperatively *) let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> snd (get_default_tactic ()) end in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 55e58187b0..2267d43d93 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -235,8 +235,8 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_tacarg_using_rule pr_gen l = let l = match l with | TacTerm s :: l -> - (** First terminal token should be considered as the name of the tactic, - so we tag it differently than the other terminal tokens. *) + (* First terminal token should be considered as the name of the tactic, + so we tag it differently than the other terminal tokens. *) primitive s :: tacarg_using_rule_token pr_gen l | _ -> tacarg_using_rule_token pr_gen l in @@ -1180,7 +1180,7 @@ let pr_goal_selector ~toplevel s = pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; - (** Those are not used by the atomic printer *) + (* Those are not used by the atomic printer *) pr_generic = (fun _ -> assert false); pr_extend = (fun _ _ _ -> assert false); pr_alias = (fun _ _ _ -> assert false); diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 06783de614..e626df5579 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -97,7 +97,7 @@ let goalevars evars = fst evars let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = - (** We handle the typeclass resolution of constraints ourselves *) + (* We handle the typeclass resolution of constraints ourselves *) let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in let ev, _ = destEvar evd' t in (evd', Evar.Set.add ev cstrs), t @@ -474,7 +474,7 @@ let get_symmetric_proof b = let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = - (** Head normalize for compatibility with the old meta mechanism *) + (* Head normalize for compatibility with the old meta mechanism *) let t = Reductionops.whd_betaiota evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false @@ -613,7 +613,7 @@ let solve_remaining_by env sigma holes by = Some evk | _ -> None in - (** Only solve independent holes *) + (* Only solve independent holes *) let indep = List.map_filter map holes in let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in let solve_tac = match tac with @@ -628,7 +628,7 @@ let solve_remaining_by env sigma holes by = in match evi with | None -> sigma - (** Evar should not be defined, but just in case *) + (* Evar should not be defined, but just in case *) | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in @@ -646,6 +646,7 @@ let poly_inverse sort = type rewrite_proof = | RewPrf of constr * constr (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *) + | RewCast of cast_kind (** A proof of convertibility (with casts) *) @@ -1561,7 +1562,7 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in - (** For compatibility *) + (* For compatibility *) let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in let treat sigma res = @@ -1611,7 +1612,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let env = match clause with | None -> env | Some id -> - (** Only consider variables not depending on [id] *) + (* Only consider variables not depending on [id] *) let ctx = named_context env in let filter decl = not (occur_var_in_decl env sigma id decl) in let nctx = List.filter filter ctx in @@ -1623,7 +1624,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> - (** For compatibility *) + (* For compatibility *) beta <*> Proofview.shelve_unifiable with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 2aee809eb6..b770b97384 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -169,7 +169,7 @@ let add_tactic_entry (kn, ml, tg) state = let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = let map arg = - (** HACK to handle especially the tactic(...) entry *) + (* HACK to handle especially the tactic(...) entry *) let wit = Genarg.rawwit Tacarg.wit_tactic in if Genarg.has_type arg wit && not ml then Tacexp (Genarg.out_gen wit arg) @@ -223,7 +223,7 @@ let interp_prod_item = function | Some arg -> arg end | Some n -> - (** FIXME: do better someday *) + (* FIXME: do better someday *) assert (String.equal s "tactic"); begin match Tacarg.wit_tactic with | ExtraArg tag -> ArgT.Any tag @@ -241,9 +241,9 @@ let make_fresh_key = | TacNonTerm _ -> "#" in let prods = String.concat "_" (List.map map prods) in - (** We embed the hash of the kernel name in the label so that the identifier - should be mostly unique. This ensures that including two modules - together won't confuse the corresponding labels. *) + (* We embed the hash of the kernel name in the label so that the identifier + should be mostly unique. This ensures that including two modules + together won't confuse the corresponding labels. *) let hash = (cur lxor (ModPath.hash (Lib.current_mp ()))) land 0x7FFFFFFF in let lbl = Id.of_string_soft (Printf.sprintf "%s_%08X" prods hash) in Lib.make_kn lbl @@ -281,7 +281,7 @@ let open_tactic_notation i (_, tobj) = let load_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in let () = check_key key in - (** Only add the printing and interpretation rules. *) + (* Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram); if Int.equal i 1 && not tobj.tacobj_local then @@ -342,7 +342,7 @@ let extend_atomic_tactic name entries = let map_prod prods = let (hd, rem) = match prods with | TacTerm s :: rem -> (s, rem) - | _ -> assert false (** Not handled by the ML extension syntax *) + | _ -> assert false (* Not handled by the ML extension syntax *) in let empty_value = function | TacTerm s -> raise NonEmptyArgument @@ -383,8 +383,8 @@ let add_ml_tactic_notation name ~level ?deprecation prods = add_glob_tactic_notation false ~level ?deprecation prods true ids tac in List.iteri iter (List.rev prods); - (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at - tactic_expr level 0) *) + (* We call [extend_atomic_tactic] only for "basic tactics" (the ones + at tactic_expr level 0) *) if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) @@ -474,8 +474,9 @@ let register_ltac local ?deprecation tacl = (name, body) in let defs () = - (** Register locally the tactic to handle recursivity. This function affects - the whole environment, so that we transactify it afterwards. *) + (* Register locally the tactic to handle recursivity. This + function affects the whole environment, so that we transactify + it afterwards. *) let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in let () = List.iter iter_rec recvars in List.map map rfun @@ -557,7 +558,7 @@ let () = register_grammars_by_name "tactic" entries let get_identifier i = - (** Workaround for badly-designed generic arguments lacking a closure *) + (* Workaround for badly-designed generic arguments lacking a closure *) Names.Id.of_string_soft (Printf.sprintf "$%i" i) type _ ty_sig = @@ -650,20 +651,22 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = in match sign with | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> - (** The extension is only made of a name followed by constr entries: we do not - add any grammar nor printing rule and add it as a true Ltac definition. *) + (* The extension is only made of a name followed by constr + entries: we do not add any grammar nor printing rule and add it + as a true Ltac definition. *) let vars = mk_sign_vars 1 s in let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in let tac = match s with | TyNil -> eval ml_tac - (** Special handling of tactics without arguments: such tactics do not do - a Proofview.Goal.nf_enter to compute their arguments. It matters for some - whole-prof tactics like [shelve_unifiable]. *) + (* Special handling of tactics without arguments: such tactics do + not do a Proofview.Goal.nf_enter to compute their arguments. It + matters for some whole-prof tactics like [shelve_unifiable]. *) | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac) in - (** Arguments are not passed directly to the ML tactic in the TacML node, - the ML tactic retrieves its arguments in the [ist] environment instead. - This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) + (* Arguments are not passed directly to the ML tactic in the TacML + node, the ML tactic retrieves its arguments in the [ist] + environment instead. This is the rôle of the + [lift_constr_tac_to_ml_tac] function. *) let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in let id = Names.Id.of_string name in let obj () = Tacenv.register_ltac true false id body ?deprecation in diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 2bd21f9d7a..83f563e2ab 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -78,12 +78,12 @@ type ('a,'t) match_rule = (** Extension indentifiers for the TACTIC EXTEND mechanism. *) type ml_tactic_name = { + mltac_plugin : string; (** Name of the plugin where the tactic is defined, typically coming from a DECLARE PLUGIN statement in the source. *) - mltac_plugin : string; + mltac_tactic : string; (** Name of the tactic entry where the tactic is defined, typically found after the TACTIC EXTEND statement in the source. *) - mltac_tactic : string; } type ml_tactic_entry = { diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 0c27f3bfe2..da0ecfc449 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -78,12 +78,12 @@ type ('a,'t) match_rule = (** Extension indentifiers for the TACTIC EXTEND mechanism. *) type ml_tactic_name = { + mltac_plugin : string; (** Name of the plugin where the tactic is defined, typically coming from a DECLARE PLUGIN statement in the source. *) - mltac_plugin : string; + mltac_tactic : string; (** Name of the tactic entry where the tactic is defined, typically found after the TACTIC EXTEND statement in the source. *) - mltac_tactic : string; } type ml_tactic_entry = { diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 85c6348b52..a1e21aab04 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -843,8 +843,9 @@ let notation_subst bindings tac = (make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in - (** This is theoretically not correct due to potential variable capture, but - Ltac has no true variables so one cannot simply substitute *) + (* This is theoretically not correct due to potential variable + capture, but Ltac has no true variables so one cannot simply + substitute *) TacLetIn (false, bindings, tac) let () = Genintern.register_ntn_subst0 wit_tactic notation_subst diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cf5eb442be..284642b38c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -50,7 +50,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w let Val.Dyn (t, _) = v in let t' = match val_tag wit with | Val.Base t' -> t' - | _ -> assert false (** not used in this module *) + | _ -> assert false (* not used in this module *) in match Val.eq t t' with | None -> false @@ -68,13 +68,13 @@ let in_list tag v = let in_gen wit v = let t = match val_tag wit with | Val.Base t -> t - | _ -> assert false (** not used in this module *) + | _ -> assert false (* not used in this module *) in Val.Dyn (t, v) let out_gen wit v = let t = match val_tag wit with | Val.Base t -> t - | _ -> assert false (** not used in this module *) + | _ -> assert false (* not used in this module *) in match prj t v with None -> assert false | Some x -> x @@ -585,8 +585,8 @@ let interp_pure_open_constr ist = let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in - (** FIXME: it is necessary to be unsafe here because of the way we handle - evars in the pretyper. Sometimes they get solved eagerly. *) + (* FIXME: it is necessary to be unsafe here because of the way we handle + evars in the pretyper. Sometimes they get solved eagerly. *) pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) (* Interprets a constr expression *) @@ -897,7 +897,7 @@ let interp_destruction_arg ist gl arg = end) in try - (** FIXME: should be moved to taccoerce *) + (* FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in @@ -1020,7 +1020,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr | TacArg {loc;v} -> interp_tacarg ist v | t -> - (** Delayed evaluation *) + (* Delayed evaluation *) Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t))) in let open Ftactic in @@ -1396,12 +1396,12 @@ and interp_match_successes lz ist s = general | Select -> begin - (** Only keep the first matching result, we don't backtrack on it *) + (* Only keep the first matching result, we don't backtrack on it *) let s = Proofview.tclONCE s in s >>= fun ans -> interp_match_success ist ans end | Once -> - (** Once a tactic has succeeded, do not backtrack anymore *) + (* Once a tactic has succeeded, do not backtrack anymore *) Proofview.tclONCE general (* Interprets the Match expressions *) @@ -1438,7 +1438,7 @@ and interp_match_goal ist lz lr lmr = (* Interprets extended tactic generic arguments *) and interp_genarg ist x : Val.t Ftactic.t = let open Ftactic.Notations in - (** Ad-hoc handling of some types. *) + (* Ad-hoc handling of some types. *) let tag = genarg_tag x in if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then interp_genarg_var_list ist x diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index c949589e22..54924f1644 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -59,7 +59,7 @@ let id_map_try_add_name id x m = the binding of the right-hand argument shadows that of the left-hand argument. *) let id_map_right_biased_union m1 m2 = - if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *) + if Id.Map.is_empty m1 then m2 (* Don't reconstruct the whole map *) else Id.Map.fold Id.Map.add m2 m1 (** Tests whether the substitution [s] is empty. *) @@ -102,7 +102,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = else raise Not_coherent_metas in let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in - (** ppedrot: Is that even correct? *) + (* ppedrot: Is that even correct? *) let merged = ln +++ ln1 in (merged, Id.Map.merge merge lcm lm) @@ -263,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct | All lhs -> wildcard_match_term lhs | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs | Pat _ -> - (** Rules with hypotheses, only work in match goal. *) - fail + (* Rules with hypotheses, only work in match goal. *) + fail (** [match_term term rules] matches the term [term] with the set of matching rules [rules].*) diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml index dc1df7ec9f..44cad820ed 100644 --- a/plugins/micromega/itv.ml +++ b/plugins/micromega/itv.ml @@ -11,10 +11,11 @@ (** Intervals (extracted from mfourier.ml) *) open Num + (** The type of intervals is *) type interval = num option * num option - (** None models the absence of bound i.e. infinity *) - (** As a result, + (** None models the absence of bound i.e. infinity + As a result, - None , None -> \]-oo,+oo\[ - None , Some v -> \]-oo,v\] - Some v, None -> \[v,+oo\[ diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index f5e9a9f34c..23f3470d77 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -103,7 +103,7 @@ module Poly : sig end -type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (** Representation of linear constraints *) +type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (* Representation of linear constraints *) and op = Eq | Ge | Gt val eval_op : op -> Num.num -> Num.num -> bool diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 8d8c6ea90b..4465aa1ee1 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -20,6 +20,7 @@ type iset = unit IMap.t type tableau = Vect.t IMap.t (** Mapping basic variables to their equation. All variables >= than a threshold rst are restricted.*) + module Restricted = struct type t = diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index f8fc943713..1825a4d77c 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -609,7 +609,7 @@ type current_problem = { exception NotInIdealUpdate of current_problem let test_dans_ideal cur_pb table metadata p lp len0 = - (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) + (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) let (c,r) = reduce2 table cur_pb.cur_poly lp in info (fun () -> "remainder: "^(stringPcut metadata r)); let cur_pb = { @@ -657,7 +657,7 @@ let deg_hom p = | (a,m)::_ -> Monomial.deg m let pbuchf table metadata cur_pb homogeneous (lp, lpc) p = - (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) + (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) sinfo "computation of the Groebner basis"; let () = match table.hmon with | None -> () diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index ef60a23e80..1777418ef6 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -374,7 +374,7 @@ let remove_zeros lci = let m = List.length lci in let u = Array.make m false in let rec utiles k = - (** TODO: Find a more reasonable implementation of this traversal. *) + (* TODO: Find a more reasonable implementation of this traversal. *) if k >= m || u.(k) then () else let () = u.(k) <- true in diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index e66fa10d5b..f1fa694356 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -131,7 +131,7 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || (Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) typ != InProp) then diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 4109e9cf38..9fea3ddcda 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -194,12 +194,12 @@ let exec_tactic env evd n f args = in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in - (** Build the getter *) + (* Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in - (** Evaluate the whole result *) + (* Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd = Evd.minimize_universes (Refiner.project gls) in diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index bb8a0faf2e..11e282e4f5 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -104,6 +104,7 @@ type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats type ssrfwdid = Id.t + (** Binders (for fwd tactics) *) type 'term ssrbind = | Bvar of Name.t diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index efc4a2c743..cd9af84ed9 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -263,7 +263,7 @@ let of_ftactic ftac gl = let tac = Proofview.V82.of_tactic tac in let { sigma = sigma } = tac gl in let ans = match !r with - | None -> assert false (** If the tactic failed we should not reach this point *) + | None -> assert false (* If the tactic failed we should not reach this point *) | Some ans -> ans in (sigma, ans) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 0553260472..18b4aeab1e 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -86,9 +86,9 @@ end (* }}} *************************************************************** *) open State -(** [=> *] ****************************************************************) -(** [nb_assums] returns the number of dependent premises *) -(** Warning: unlike [nb_deps_assums], it does not perform reduction *) +(***[=> *] ****************************************************************) +(** [nb_assums] returns the number of dependent premises + Warning: unlike [nb_deps_assums], it does not perform reduction *) let rec nb_assums cur env sigma t = match EConstr.kind sigma t with | Prod(name,ty,body) -> @@ -148,7 +148,7 @@ let tac_case t = Ssrelim.ssrscasetac t end -(** [=> [: id]] ************************************************************) +(***[=> [: id]] ************************************************************) [@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4ed75cdbe4..191a4e9a20 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in + let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 6497b6ff98..efd65ade15 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -122,6 +122,7 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t + (** Constructors for constr_expr *) let isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false let destCVar = function @@ -139,6 +140,7 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((CAst.make ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) + (** Constructors for rawconstr *) let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) @@ -925,7 +927,7 @@ let of_ftactic ftac gl = let tac = Proofview.V82.of_tactic tac in let { sigma = sigma } = tac gl in let ans = match !r with - | None -> assert false (** If the tactic failed we should not reach this point *) + | None -> assert false (* If the tactic failed we should not reach this point *) | Some ans -> ans in (sigma, ans) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 8672c55767..f0bb6f58a6 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -194,6 +194,7 @@ val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> c (** [do_once r f] calls [f] and updates the ref only once *) val do_once : 'a option ref -> (unit -> 'a) -> unit + (** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) val assert_done : 'a option ref -> 'a diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fe67f5767b..62c27297f3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1015,9 +1015,9 @@ let add_assert_false_case pb tomatch = let adjust_impossible_cases sigma pb pred tomatch submat = match submat with | [] -> - (** FIXME: This breaks if using evar-insensitive primitives. In particular, - this means that the Evd.define below may redefine an already defined - evar. See e.g. first definition of test for bug #3388. *) + (* FIXME: This breaks if using evar-insensitive primitives. In particular, + this means that the Evd.define below may redefine an already defined + evar. See e.g. first definition of test for bug #3388. *) let pred = EConstr.Unsafe.to_constr pred in begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk sigma) == Evar_kinds.ImpossibleCase -> @@ -1684,8 +1684,8 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = convertible subterms of the substitution *) let evdref = ref sigma in let rec aux (k,env,subst as x) t = - (** Use a reference because the [map_constr_with_full_binders] does not - allow threading a state. *) + (* Use a reference because the [map_constr_with_full_binders] does not + allow threading a state. *) let sigma = !evdref in match EConstr.kind sigma t with | Rel n when is_local_def (lookup_rel n !!env) -> t @@ -2021,7 +2021,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let refresh_tycon sigma t = - (** If we put the typing constraint in the term, it has to be + (* If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe can appear in the term. *) refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index d7118efd7a..032e4bbf85 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -96,8 +96,8 @@ let rec build_lambda sigma vars ctx m = match vars with | (_, id, t) :: suf -> (Name id, t, suf) in - (** Check that the abstraction is legal by generating a transitive closure of - its dependencies. *) + (* Check that the abstraction is legal by generating a transitive closure of + its dependencies. *) let is_nondep t clear = match clear with | [] -> true | _ -> @@ -106,12 +106,12 @@ let rec build_lambda sigma vars ctx m = match vars with List.for_all_i check 1 clear in let fold (_, _, t) clear = is_nondep t clear :: clear in - (** Produce a list of booleans: true iff we keep the hypothesis *) + (* Produce a list of booleans: true iff we keep the hypothesis *) let clear = List.fold_right fold pre [false] in let clear = List.drop_last clear in - (** If the conclusion depends on a variable we cleared, failure *) + (* If the conclusion depends on a variable we cleared, failure *) let () = if not (is_nondep m clear) then raise PatternMatchingFailure in - (** Create the abstracted term *) + (* Create the abstracted term *) let fold (k, accu) keep = if keep then let k = succ k in @@ -121,10 +121,10 @@ let rec build_lambda sigma vars ctx m = match vars with let keep, shift = List.fold_left fold (0, []) clear in let shift = List.rev shift in let map = function - | None -> mkProp (** dummy term *) + | None -> mkProp (* dummy term *) | Some i -> mkRel (i + 1) in - (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *) + (* [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *) let subst = List.map map shift @ mkRel 1 :: @@ -143,12 +143,12 @@ let rec build_lambda sigma vars ctx m = match vars with if i > n then i - n + keep else match List.nth shift (i - 1) with | None -> - (** We cleared a variable that we wanted to abstract! *) + (* We cleared a variable that we wanted to abstract! *) raise PatternMatchingFailure | Some k -> k in let vars = List.map map vars in - (** Create the abstraction *) + (* Create the abstraction *) let m = mkLambda (na, Vars.lift keep t, m) in build_lambda sigma vars (pre @ suf) m @@ -377,8 +377,8 @@ let matches_core env sigma allow_bound_rels let () = match ci1.cip_ind with | None -> () | Some ind1 -> - (** ppedrot: Something spooky going here. The comparison used to be - the generic one, so I may have broken something. *) + (* ppedrot: Something spooky going here. The comparison used to be + the generic one, so I may have broken something. *) if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure in let () = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 33ced6d6e0..0b545dc191 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -688,7 +688,7 @@ and detype_r d flags avoid env sigma t = [detype d flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then - (** Print the compatibility match version *) + (* Print the compatibility match version *) let c' = try let ind = Projection.inductive p in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6c268de3b3..e6e1530e36 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1311,10 +1311,10 @@ let max_undefined_with_candidates evd = | None -> () | Some l -> raise (MaxUndefined (evk, evi, l)) in - (** [fold_right] traverses the undefined map in decreasing order of indices. - The evar with candidates of maximum index is thus the first evar with - candidates found by a [fold_right] traversal. This has a significant impact on - performance. *) + (* [fold_right] traverses the undefined map in decreasing order of + indices. The evar with candidates of maximum index is thus the + first evar with candidates found by a [fold_right] + traversal. This has a significant impact on performance. *) try let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in None diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4692fe0057..4c4a236620 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -80,7 +80,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if v' == v then t else mkProd (na, u, v') | _ -> t in - (** Refresh the types of evars under template polymorphic references *) + (* Refresh the types of evars under template polymorphic references *) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> @@ -1385,7 +1385,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = let occur_evar_upto_types sigma n c = let c = EConstr.Unsafe.to_constr c in let seen = ref Evar.Set.empty in - (** FIXME: Is that supposed to be evar-insensitive? *) + (* FIXME: Is that supposed to be evar-insensitive? *) let rec occur_rec c = match Constr.kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> @@ -1581,7 +1581,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = Id.Set.subset (collect_vars evd rhs) !names in let body = - if fast rhs then nf_evar evd rhs (** FIXME? *) + if fast rhs then nf_evar evd rhs (* FIXME? *) else let t' = imitate (env,0) rhs in if !progress then diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9b2da0b084..e14766f370 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -148,7 +148,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Array.equal f c1 c2 && Array.equal f t1 t2 | GSort s1, GSort s2 -> glob_sort_eq s1 s2 | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Option.equal (==) gn1 gn2 (* Only thing sensible *) && Namegen.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index c6fdb0ec14..c405fcfc72 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -106,6 +106,7 @@ and 'a tomatch_tuples_g = 'a tomatch_tuple_g list and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables of [t] are members of [il]. *) + and 'a cases_clauses_g = 'a cases_clause_g list type glob_constr = [ `any ] glob_constr_g diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 10d8451947..ff552c7caf 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -469,9 +469,9 @@ let compute_projections env (kn, i as ind) = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in - (** We build a substitution smashing the lets in the record parameters so - that typechecking projections requires just a substitution and not - matching with a parameter context. *) + (* We build a substitution smashing the lets in the record parameters so + that typechecking projections requires just a substitution and not + matching with a parameter context. *) let indty = (* [ty] = [Ind inst] is typed in context [params] *) let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in @@ -748,7 +748,7 @@ let type_of_projection_knowing_arg env sigma p c ty = let control_only_guard env sigma c = let c = Evarutil.nf_evar sigma c in let check_fix_cofix e c = - (** [c] has already been normalized upfront *) + (* [c] has already been normalized upfront *) let c = EConstr.Unsafe.to_constr c in match kind c with | CoFix (_,(_,_,_) as cofix) -> diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 022c383f60..dc2663c1ca 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -406,14 +406,15 @@ and nf_evar env sigma evk args = mkEvar (evk, [||]), ty end else - (** Let-bound arguments are present in the evar arguments but not in the - type, so we turn the let into a product. *) + (* Let-bound arguments are present in the evar arguments but not + in the type, so we turn the let into a product. *) let hyps = Context.Named.drop_bodies hyps in let fold accu d = Term.mkNamedProd_or_LetIn d accu in let t = List.fold_left fold ty hyps in let ty, args = nf_args env sigma args t in - (** nf_args takes arguments in the reverse order but produces them in the - correct one, so we have to reverse them again for the evar node *) + (* nf_args takes arguments in the reverse order but produces them + in the correct one, so we have to reverse them again for the + evar node *) mkEvar (evk, Array.rev_of_list args), ty let evars_of_evar_map sigma = diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3c1c470053..a3ab250784 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -256,7 +256,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *) + (* FIXME: Stupid workaround to pattern_of_constr being evar sensitive *) let c = Evarutil.nf_evar sigma c in pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) with Not_found (* List.index failed *) -> diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 054f0c76a9..51103ca194 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -38,12 +38,15 @@ type subterm_unification_error = bool * position_reporting * position_reporting type type_error = (constr, types) ptype_error type pretype_error = - (** Old Case *) | CantFindCaseType of constr - (** Type inference unification *) + (** Old Case *) + | ActualTypeNotCoercible of unsafe_judgment * types * unification_error - (** Tactic Unification *) + (** Type inference unification *) + | UnifOccurCheck of Evar.t * constr + (** Tactic Unification *) + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f5e48bcd39..74ef1ddbca 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -212,7 +212,7 @@ type frozen = let frozen_and_pending_holes (sigma, sigma') = let undefined0 = Option.cata Evd.undefined_map Evar.Map.empty sigma in - (** Fast path when the undefined evars where not modified *) + (* Fast path when the undefined evars where not modified *) if undefined0 == Evd.undefined_map sigma' then FrozenId undefined0 else @@ -579,7 +579,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma sigma ctxtv vdef in let sigma = Typing.check_type_fixpoint ?loc !!env sigma names ftys vdefj in let nf c = nf_evar sigma c in - let ftys = Array.map nf ftys in (** FIXME *) + let ftys = Array.map nf ftys in (* FIXME *) let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in let fixj = match fixkind with | GFix (vn,i) -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index fe9b69dbbc..0c4a2e2a99 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -374,7 +374,7 @@ let decompose_projection sigma c args = match EConstr.kind sigma c with | Const (c, u) -> let n = find_projection_nparams (ConstRef c) in - (** Check if there is some canonical projection attached to this structure *) + (* Check if there is some canonical projection attached to this structure *) let _ = GlobRef.Map.find (ConstRef c) !object_table in let arg = Stack.nth args n in arg diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a57ee6e292..f8e8fa9eb9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -203,6 +203,7 @@ end (** Machinery about stack of unfolded constants *) module Cst_stack = struct open EConstr + (** constant * params * args - constant applied to params = term in head applied to args @@ -1342,7 +1343,7 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = - (** FIXME *) + (* FIXME *) try let ans = match pb with | Reduction.CUMUL -> @@ -1632,7 +1633,7 @@ let meta_reducible_instance evd b = in let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = - let u = whd_betaiota Evd.empty u (** FIXME *) in + let u = whd_betaiota Evd.empty u (* FIXME *) in match EConstr.kind evd u with | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 088e898a99..a1fd610676 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -77,7 +77,9 @@ module Stack : sig | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t - | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) + | Cst of cst_member + * int (* current foccussed arg *) + * int list (* remaining args *) * 'a t * Cst_stack.t and 'a t = 'a member list @@ -93,6 +95,7 @@ module Stack : sig val compare_shape : 'a t -> 'a t -> bool exception IncompatibleFold2 + (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)]. @return the result and the lifts to apply on the terms @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *) @@ -104,6 +107,7 @@ module Stack : sig (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not start by App *) val strip_app : 'a t -> 'a t * 'a t + (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index d9df8c8cf8..2e7176a6b3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -250,7 +250,7 @@ let invert_name labs l na0 env sigma ref = function let labs',ccl = decompose_lam sigma c in let _, l' = whd_betalet_stack sigma ccl in let labs' = List.map snd labs' in - (** ppedrot: there used to be generic equality on terms here *) + (* ppedrot: there used to be generic equality on terms here *) let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in if List.equal eq_constr labs' labs && List.equal eq_constr l l' then Some (minfxargs,ref) @@ -450,7 +450,7 @@ let substl_checking_arity env subst sigma c = the other ones are replaced by the function symbol *) let rec nf_fix c = match EConstr.kind sigma c with | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs -> - (** FIXME: find a less hackish way of doing this *) + (* FIXME: find a less hackish way of doing this *) begin match EConstr.kind sigma' c with | Evar _ -> f | c -> EConstr.of_kind c @@ -943,7 +943,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | _ -> false) -> let npars = Projection.npars p in if List.length stack <= npars then - (** Do not show the eta-expanded form *) + (* Do not show the eta-expanded form *) s' else redrec (applist (c, stack)) | _ -> redrec (applist(c, stack))) @@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = begin fun env sigma t -> let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref 1 in - (** FIXME: we do suspicious things with this evarmap *) + (* FIXME: we do suspicious things with this evarmap *) let evd = ref sigma in let rec traverse nested (env,c as envc) t = if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index d00195678b..f8aedf88c2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,33 +25,33 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen (** This module defines type-classes *) type typeclass = { + cl_univs : Univ.AUContext.t; (** The toplevel universe quantification in which the typeclass lives. In particular, [cl_props] and [cl_context] are quantified over it. *) - cl_univs : Univ.AUContext.t; + cl_impl : GlobRef.t; (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) - cl_impl : GlobRef.t; + cl_context : GlobRef.t option list * Constr.rel_context; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : GlobRef.t option list * Constr.rel_context; - (** Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; + (** Context of definitions and properties on defs, will not be shared *) + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; - (** Whether we use matching or full unification during resolution *) cl_strict : bool; + (** Whether we use matching or full unification during resolution *) + cl_unique : bool; (** Whether we can assume that instances are unique, which allows no backtracking and sharing of resolution. *) - cl_unique : bool; } type instance diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 366af0772f..79f2941554 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -36,8 +36,8 @@ val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) val solve_evars : env -> evar_map -> constr -> evar_map * constr -(** Raise an error message if incorrect elimination for this inductive *) -(** (first constr is term to match, second is return predicate) *) +(** Raise an error message if incorrect elimination for this inductive + (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 094fcd923e..f0cd5c5f6a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -76,8 +76,8 @@ let unsafe_occur_meta_or_existential c = let occur_meta_or_undefined_evar evd c = - (** This is performance-critical. Using the evar-insensitive API changes the - resulting heuristic. *) + (* This is performance-critical. Using the evar-insensitive API changes the + resulting heuristic. *) let c = EConstr.Unsafe.to_constr c in let rec occrec c = match Constr.kind c with | Meta _ -> raise Occur @@ -134,7 +134,7 @@ let abstract_list_all env evd typ c l = | UserError _ -> error_cannot_find_well_typed_abstraction env evd p l None | Type_errors.TypeError (env',x) -> - (** FIXME: plug back the typing information *) + (* FIXME: plug back the typing information *) error_cannot_find_well_typed_abstraction env evd p l None | Pretype_errors.PretypeError (env',evd,TypingError x) -> error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in @@ -154,11 +154,9 @@ let abstract_list_all_with_dependencies env evd typ c l = if b then let p = nf_evar evd ev in evd, p - else error_cannot_find_well_typed_abstraction env evd + else error_cannot_find_well_typed_abstraction env evd c l None -(**) - (* A refinement of [conv_pb]: the integers tells how many arguments were applied in the context of the conversion problem; if the number is non zero, steps of eta-expansion will be allowed @@ -598,8 +596,9 @@ let isAllowedEvar sigma flags c = match EConstr.kind sigma c with let subst_defined_metas_evars sigma (bl,el) c = - (** This seems to be performance-critical, and using the evar-insensitive - primitives blow up the time passed in this function. *) + (* This seems to be performance-critical, and using the + evar-insensitive primitives blow up the time passed in this + function. *) let c = EConstr.Unsafe.to_constr c in let rec substrec c = match Constr.kind c with | Meta i -> @@ -656,7 +655,7 @@ let is_eta_constructor_app env sigma ts f l1 term = | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && let (_, projs, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> - (** Check that the other term is neutral *) + (* Check that the other term is neutral *) is_neutral env sigma ts term | _ -> false) | _ -> false @@ -783,7 +782,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) - (** Fast path for projections. *) + (* Fast path for projections. *) | Proj (p1,c1), Proj (p2,c2) when Constant.equal (Projection.constant p1) (Projection.constant p2) -> (try unify_same_proj curenvnb cv_pb {opt with at_top = true} @@ -908,7 +907,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e match EConstr.kind sigma c with | Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' -> (try destApp sigma (Retyping.expand_projection curenv sigma p t (Array.to_list l)) - with RetypeError _ -> (** Unification can be called on ill-typed terms, due + with RetypeError _ -> (* Unification can be called on ill-typed terms, due to FO and eta in particular, fail gracefully in that case *) (c, l)) | _ -> (c, l) @@ -1604,7 +1603,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = with | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) - (** MS: This is pretty bad, it catches Not_found for example *) + (* MS: This is pretty bad, it catches Not_found for example *) | e when CErrors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c30c4f0932..113aac25da 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -207,10 +207,10 @@ and nf_evar env sigma evk stk = nf_stk env sigma (mkEvar (evk, [||])) concl stk else match stk with | Zapp args :: stk -> - (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that - really an invariant? *) - (** Let-bound arguments are present in the evar arguments but not in the - type, so we turn the let into a product. *) + (* We assume that there is no consecutive Zapp nodes in a VM stack. Is that + really an invariant? *) + (* Let-bound arguments are present in the evar arguments but not in the + type, so we turn the let into a product. *) let hyps = Context.Named.drop_bodies hyps in let fold accu d = Term.mkNamedProd_or_LetIn d accu in let t = List.fold_left fold concl hyps in @@ -388,7 +388,7 @@ and nf_cofix env sigma cf = let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); - (** This evar-normalizes terms beforehand *) + (* This evar-normalizes terms beforehand *) let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in let v = Csymtable.val_of_constr env c in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f9f4d7f7f8..8f7e4470f9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -427,7 +427,7 @@ let locate_modtype qid = let all = Nametab.locate_extended_all_modtype qid in let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in let modtypes = List.map map all in - (** Don't forget the opened module types: they are not part of the same name tab. *) + (* Don't forget the opened module types: they are not part of the same name tab. *) let all = Nametab.locate_extended_all_dir qid in let map dir = let open Nametab.GlobDirRef in match dir with | DirOpenModtype _ -> Some (Dir dir, qid) diff --git a/printing/printer.ml b/printing/printer.ml index 2bbda279bd..83f1f8d8e9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -605,12 +605,12 @@ let print_evar_constraints gl sigma = let t1 = Evarutil.nf_evar sigma t1 and t2 = Evarutil.nf_evar sigma t2 in let env = - (** We currently allow evar instances to refer to anonymous de Bruijn - indices, so we protect the error printing code in this case by giving - names to every de Bruijn variable in the rel_context of the conversion - problem. MS: we should rather stop depending on anonymous variables, they - can be used to indicate independency. Also, this depends on a strategy for - naming/renaming *) + (* We currently allow evar instances to refer to anonymous de Bruijn + indices, so we protect the error printing code in this case by giving + names to every de Bruijn variable in the rel_context of the conversion + problem. MS: we should rather stop depending on anonymous variables, they + can be used to indicate independency. Also, this depends on a strategy for + naming/renaming *) Namegen.make_all_name_different env sigma in str" " ++ hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ @@ -686,7 +686,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | None -> GoalMap.empty in - (** Printing functions for the extra informations. *) + (* Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a | b::l -> Pp.int a ++ str"-" ++ print_stack b l @@ -753,7 +753,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | None -> () in - (** Main function *) + (* Main function *) match goals with | [] -> begin diff --git a/printing/printer.mli b/printing/printer.mli index b0232ec4ac..357f30d1f4 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -112,6 +112,7 @@ val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t (** Contexts *) + (** Display compact contexts of goals (simple hyps on the same line) *) val set_compact_context : bool -> unit val get_compact_context : unit -> bool diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index ce9ee5ae6f..1ebde3d572 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -12,6 +12,7 @@ (** Controls whether to show diffs. Takes values "on", "off", "removed" *) val write_diffs_option : string -> unit + (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool diff --git a/proofs/clenv.ml b/proofs/clenv.ml index b7ccd647b5..1f1bdf4da7 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -601,17 +601,17 @@ let make_evar_clause env sigma ?len t = | None -> -1 | Some n -> assert (0 <= n); n in - (** FIXME: do the renaming online *) + (* FIXME: do the renaming online *) let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let rec clrec (sigma, holes) inst n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with | Cast (t, _, _) -> clrec (sigma, holes) inst n t | Prod (na, t1, t2) -> - (** Share the evar instances as we are living in the same context *) + (* Share the evar instances as we are living in the same context *) let inst, ctx, args, subst = match inst with | None -> - (** Dummy type *) + (* Dummy type *) let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in Some (ctx, args, subst), ctx, args, subst | Some (ctx, args, subst) -> inst, ctx, args, subst @@ -688,7 +688,7 @@ let solve_evar_clause env sigma hyp_only clause = function let open EConstr in let fold holes h = if h.hole_deps then - (** Some subsequent term uses the hole *) + (* Some subsequent term uses the hole *) let (ev, _) = destEvar sigma h.hole_evar in let is_dep hole = occur_evar sigma ev hole.hole_type in let in_hyp = List.exists is_dep holes in @@ -697,7 +697,7 @@ let solve_evar_clause env sigma hyp_only clause = function let h = { h with hole_deps = dep } in h :: holes else - (** The hole does not occur anywhere *) + (* The hole does not occur anywhere *) h :: holes in let holes = List.fold_left fold [] (List.rev clause.cl_holes) in diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 4720328893..c36b0fa337 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -61,9 +61,9 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv = clenv_pose_metas_as_evars clenv dep_mvs let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - (** ppedrot: a Goal.enter here breaks things, because the tactic below may - solve goals by side effects, while the compatibility layer keeps those - useless goals. That deserves a FIXME. *) + (* ppedrot: a Goal.enter here breaks things, because the tactic below may + solve goals by side effects, while the compatibility layer keeps those + useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = diff --git a/proofs/logic.ml b/proofs/logic.ml index 15ba0a704f..456ab879eb 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -373,8 +373,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm = check_typability env sigma ty; let sigma = check_conv_leq_goal env sigma trm ty conclty in let res = mk_refgoals sigma goal goalacc ty t in - (** we keep the casts (in particular VMcast and NATIVEcast) except - when they are annotating metas *) + (* we keep the casts (in particular VMcast and NATIVEcast) except + when they are annotating metas *) if isMeta t then begin assert (k != VMcast && k != NATIVEcast); res diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 886a62cb89..acf5510aa0 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -167,23 +167,23 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = cb, status, univs let refine_by_tactic env sigma ty tac = - (** Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) + (* Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in - (** Save the existing goals *) + (* Save the existing goals *) let prev_future_goals = save_future_goals sigma in - (** Start a proof *) + (* Start a proof *) let prf = Proof.start sigma [env, ty] in let (prf, _) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> - (** Catch the inner error of the monad tactic *) + (* Catch the inner error of the monad tactic *) let (_, info) = CErrors.push src in iraise (e, info) in - (** Plug back the retrieved sigma *) + (* Plug back the retrieved sigma *) let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in assert (stack = []); let ans = match Proof.initial_goals prf with @@ -191,26 +191,26 @@ let refine_by_tactic env sigma ty tac = | _ -> assert false in let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in - (** [neff] contains the freshly generated side-effects *) + (* [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in - (** Reset the old side-effects *) + (* Reset the old side-effects *) let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in - (** Restore former goals *) + (* Restore former goals *) let sigma = restore_future_goals sigma prev_future_goals in - (** Push remaining goals as future_goals which is the only way we - have to inform the caller that there are goals to collect while - not being encapsulated in the monad *) - (** Goals produced by tactic "shelve" *) + (* Push remaining goals as future_goals which is the only way we + have to inform the caller that there are goals to collect while + not being encapsulated in the monad *) + (* Goals produced by tactic "shelve" *) let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in - (** Goals produced by tactic "give_up" *) + (* Goals produced by tactic "give_up" *) let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in - (** Other goals *) + (* Other goals *) let sigma = List.fold_right Evd.declare_future_goal goals sigma in - (** Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) + (* Get rid of the fresh side-effects by internalizing them in the term + itself. Note that this is unsound, because the tactic may have solved + other goals that were already present during its invocation, so that + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 67e19df0e7..76a1e61ad2 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -422,9 +422,9 @@ let return_proof ?(allow_partial=false) () = let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in let eff = Evd.eval_side_effects evd in - (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else @@ -432,9 +432,9 @@ let return_proof ?(allow_partial=false) () = let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in - (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) let proofs = List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd diff --git a/proofs/refine.ml b/proofs/refine.ml index 540a8bb420..d812a8cad7 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -27,7 +27,7 @@ let extract_prefix env info = let typecheck_evar ev env sigma = let info = Evd.find sigma ev in - (** Typecheck the hypotheses. *) + (* Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = let t = NamedDecl.get_type decl in let sigma, _ = Typing.sort_of env sigma t in @@ -40,7 +40,7 @@ let typecheck_evar ev env sigma = let (common, changed) = extract_prefix env info in let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in - (** Typecheck the conclusion *) + (* Typecheck the conclusion *) let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma @@ -60,39 +60,39 @@ let generic_refine ~typecheck f gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let state = Proofview.Goal.state gl in - (** Save the [future_goals] state to restore them after the - refinement. *) + (* Save the [future_goals] state to restore them after the + refinement. *) let prev_future_goals = Evd.save_future_goals sigma in - (** Create the refinement term *) + (* Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.V82.wrap_exceptions begin fun () -> let evs = Evd.save_future_goals sigma in - (** Redo the effects in sigma in the monad's env *) + (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in let sideff = Safe_typing.side_effects_of_private_constants privates_csts in let env = add_side_effects env sideff in - (** Check that the introduced evars are well-typed *) + (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in - (** Check that the refined term is typesafe *) + (* Check that the refined term is typesafe *) let sigma = if typecheck then Typing.check env sigma c concl else sigma in - (** Check that the goal itself does not appear in the refined term *) + (* Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () else Pretype_errors.error_occur_check env sigma self c in - (** Restore the [future goals] state. *) + (* Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals in - (** Select the goals *) + (* Select the goals *) let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in - (** Proceed to the refinement *) + (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> - (** Nothing to do, the goal has been solved by side-effect *) + (* Nothing to do, the goal has been solved by side-effect *) sigma | Some self -> match evkmain with @@ -104,7 +104,7 @@ let generic_refine ~typecheck f gl = | None -> sigma | Some id -> Evd.rename evk id sigma in - (** Mark goals *) + (* Mark goals *) let sigma = Proofview.Unsafe.mark_as_goals sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 64d7630d55..a5f691babb 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -133,7 +133,7 @@ module New = struct f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } let pf_global id gl = - (** We only check for the existence of an [id] in [hyps] *) + (* We only check for the existence of an [id] in [hyps] *) let hyps = Proofview.Goal.hyps gl in Constrintern.construct_reference hyps id @@ -149,12 +149,12 @@ module New = struct let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 let pf_ids_of_hyps gl = - (** We only get the identifiers in [hyps] *) + (* We only get the identifiers in [hyps] *) let hyps = Proofview.Goal.hyps gl in ids_of_named_context hyps let pf_ids_set_of_hyps gl = - (** We only get the identifiers in [hyps] *) + (* We only get the identifiers in [hyps] *) let env = Proofview.Goal.env gl in Environ.ids_of_named_context_val (Environ.named_context_val env) @@ -186,7 +186,7 @@ module New = struct List.hd hyps let pf_nf_concl (gl : Proofview.Goal.t) = - (** We normalize the conclusion just after *) + (* We normalize the conclusion just after *) let concl = Proofview.Goal.concl gl in let sigma = project gl in nf_evar sigma concl diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index 6e6827c73f..067ea5df0c 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -70,6 +70,7 @@ module type Task = sig (** UID of the task kind, for -toploop *) val name : string ref + (** Extra arguments of the task kind, for -toploop *) val extra_env : unit -> string array diff --git a/stm/stm.ml b/stm/stm.ml index 3444229735..e835bdcb1e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1087,7 +1087,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else match cmd with - | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *) + | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *) | _ -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr) @@ -1750,7 +1750,7 @@ end = struct (* {{{ *) let uc = Option.get (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in - (** We only manipulate monomorphic terms here. *) + (* We only manipulate monomorphic terms here. *) let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in let pr = Future.from_val (map (Option.get (Global.body_of_constant_body c))) in diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 3c262de910..3a687a6b41 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -76,7 +76,7 @@ let shrink_entry sign const = | None -> assert false | Some t -> t in - (** The body has been forced by the call to [build_constant_by_tactic] *) + (* The body has been forced by the call to [build_constant_by_tactic] *) let () = assert (Future.is_over const.const_entry_body) in let ((body, uctx), eff) = Future.force const.const_entry_body in let (body, typ, ctx) = decompose (List.length sign) body typ [] in @@ -140,18 +140,18 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in let cst () = - (** do not compute the implicit arguments, it may be costly *) + (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in - (** ppedrot: seems legit to have abstracted subproofs as local*) + (* ppedrot: seems legit to have abstracted subproofs as local*) Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in let cst = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_const_entry _ -> EInstance.empty | Entries.Polymorphic_const_entry (_, ctx) -> - (** We mimick what the kernel does, that is ensuring that no additional - constraints appear in the body of polymorphic constants. Ideally this - should be enforced statically. *) + (* We mimick what the kernel does, that is ensuring that no additional + constraints appear in the body of polymorphic constants. Ideally this + should be enforced statically. *) let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in let () = assert (Univ.ContextSet.is_empty body_uctx) in EInstance.make (Univ.UContext.instance ctx) diff --git a/tactics/auto.ml b/tactics/auto.ml index 441fb68acc..c030c77d4d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -70,19 +70,19 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) let connect_hint_clenv poly (c, _, ctx) clenv gl = - (** [clenv] has been generated by a hint-making function, so the only relevant - data in its evarmap is the set of metas. The [evar_reset_evd] function - below just replaces the metas of sigma by those coming from the clenv. *) + (* [clenv] has been generated by a hint-making function, so the only relevant + data in its evarmap is the set of metas. The [evar_reset_evd] function + below just replaces the metas of sigma by those coming from the clenv. *) let sigma = Tacmach.New.project gl in let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in - (** Still, we need to update the universes *) + (* Still, we need to update the universes *) let clenv, c = if poly then - (** Refresh the instance of the hint *) + (* Refresh the instance of the hint *) let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - (** Only metas are mentioning the old universes. *) + (* Only metas are mentioning the old universes. *) let clenv = { templval = Evd.map_fl emap clenv.templval; templtyp = Evd.map_fl emap clenv.templtyp; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index fd2a163f80..ba7645446d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1096,8 +1096,8 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = let initial_select_evars filter = fun evd ev evi -> filter ev (Lazy.from_val (snd evi.Evd.evar_source)) && - (** Typeclass evars can contain evars whose conclusion is not - yet determined to be a class or not. *) + (* Typeclass evars can contain evars whose conclusion is not + yet determined to be a class or not. *) Typeclasses.is_class_evar evd evi let resolve_typeclass_evars debug depth unique env evd filter split fail = diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 46dff34f89..a6922213d0 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -39,20 +39,20 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic module Search : sig val eauto_tac : - ?st:TransparentState.t -> + ?st:TransparentState.t (** The transparent_state used when working with local hypotheses *) - ?unique:bool -> + -> ?unique:bool (** Should we force a unique solution *) - only_classes:bool -> + -> only_classes:bool (** Should non-class goals be shelved and resolved at the end *) - ?strategy:search_strategy -> + -> ?strategy:search_strategy (** Is a traversing-strategy specified? *) - depth:Int.t option -> + -> depth:Int.t option (** Bounded or unbounded search *) - dep:bool -> + -> dep:bool (** Should the tactic be made backtracking on the initial goals, - whatever their internal dependencies are. *) - Hints.hint_db list -> + whatever their internal dependencies are. *) + -> Hints.hint_db list (** The list of hint databases to use *) - unit Proofview.tactic + -> unit Proofview.tactic end diff --git a/tactics/equality.ml b/tactics/equality.ml index bdc95941b2..769e702da1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1742,7 +1742,7 @@ let subst_one_var dep_proof_ok x = (* Find a non-recursive definition for x *) let res = try - (** [is_eq_x] ensures nf_evar on its side *) + (* [is_eq_x] ensures nf_evar on its side *) let hyps = Proofview.Goal.hyps gl in let test hyp _ = is_eq_x gl x hyp in Context.Named.fold_outside test ~init:() hyps; diff --git a/tactics/hints.ml b/tactics/hints.ml index 77479f9efa..c20feccace 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -210,9 +210,9 @@ let fresh_key = let lbl = Id.of_string ("_" ^ string_of_int cur) in let kn = Lib.make_kn lbl in let (mp, _) = KerName.repr kn in - (** We embed the full path of the kernel name in the label so that the - identifier should be unique. This ensures that including two modules - together won't confuse the corresponding labels. *) + (* We embed the full path of the kernel name in the label so that + the identifier should be unique. This ensures that including + two modules together won't confuse the corresponding labels. *) let lbl = Id.of_string_soft (Printf.sprintf "%s#%i" (ModPath.to_string mp) cur) in @@ -558,7 +558,7 @@ struct let realize_tac secvars (id,tac) = if Id.Pred.subset tac.secvars secvars then Some tac else - (** Warn about no longer typable hint? *) + (* Warn about no longer typable hint? *) None let head_evar sigma c = @@ -601,7 +601,7 @@ struct let se = find k db in merge_entry secvars db se.sentry_nopat se.sentry_pat - (** Precondition: concl has no existentials *) + (* Precondition: concl has no existentials *) let map_auto sigma ~secvars (k,args) concl db = let se = find k db in let st = if db.use_dn then (Some db.hintdb_state) else None in @@ -644,7 +644,7 @@ struct | None -> let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in if not (List.exists is_present db.hintdb_nopat) then - (** FIXME *) + (* FIXME *) { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } else db | Some gr -> @@ -738,7 +738,6 @@ module Hintdbmap = String.Map type hint_db = Hint_db.t (** Initially created hint databases, for typeclasses and rewrite *) - let typeclasses_db = "typeclass_instances" let rewrite_db = "rewrite" @@ -1586,7 +1585,7 @@ let log_hint h = let store = get_extra_data sigma in match Store.get store hint_trace with | None -> - (** All calls to hint logging should be well-scoped *) + (* All calls to hint logging should be well-scoped *) assert false | Some trace -> let trace = KNmap.add h.uid h trace in diff --git a/tactics/inv.ml b/tactics/inv.ml index 6a39a10fc4..2ae37ab471 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -365,7 +365,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = let substHypIfVariable tac id = Proofview.Goal.enter begin fun gl -> let sigma = project gl in - (** We only look at the type of hypothesis "id" *) + (* We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 224cd68cf9..bfbce8f6eb 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -572,7 +572,7 @@ module New = struct with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.") let nthHypId m gl = - (** We only use [id] *) + (* We only use [id] *) nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -688,12 +688,12 @@ module New = struct end) end let elimination_sort_of_goal gl = - (** Retyping will expand evars anyway. *) + (* Retyping will expand evars anyway. *) let c = Proofview.Goal.concl gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_hyp id gl = - (** Retyping will expand evars anyway. *) + (* Retyping will expand evars anyway. *) let c = pf_get_hyp_typ id gl in pf_apply Retyping.get_sort_family_of gl c diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2947e44f7a..201b7801c3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -191,6 +191,7 @@ module New : sig val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic + (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b3ea13cf4f..9e9d52b72c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -183,7 +183,7 @@ let convert_gen pb x y = | Some sigma -> Proofview.Unsafe.tclEVARS sigma | None -> Tacticals.New.tclFAIL 0 (str "Not convertible") | exception _ -> - (** FIXME: Sometimes an anomaly is raised from conversion *) + (* FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") end @@ -241,7 +241,7 @@ let clear_gen fail = function | ids -> Proofview.Goal.enter begin fun gl -> let ids = List.fold_right Id.Set.add ids Id.Set.empty in - (** clear_hyps_in_evi does not require nf terms *) + (* clear_hyps_in_evi does not require nf terms *) let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -307,7 +307,7 @@ let rename_hyp repl = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - (** Check that we do not mess variables *) + (* Check that we do not mess variables *) let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = @@ -322,7 +322,7 @@ let rename_hyp repl = CErrors.user_err (Id.print elt ++ str " is already used") with Not_found -> () in - (** All is well *) + (* All is well *) let make_subst (src, dst) = (src, mkVar dst) in let subst = List.map make_subst repl in let subst c = Vars.replace_vars subst c in @@ -1235,7 +1235,7 @@ let cut c = let concl = Proofview.Goal.concl gl in let is_sort = try - (** Backward compat: ensure that [c] is well-typed. *) + (* Backward compat: ensure that [c] is well-typed. *) let typ = Typing.unsafe_type_of env sigma c in let typ = whd_all env sigma typ in match EConstr.kind sigma typ with @@ -1245,7 +1245,7 @@ let cut c = in if is_sort then let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in - (** Backward compat: normalize [c]. *) + (* Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in @@ -1498,8 +1498,8 @@ let simplest_elim c = default_elim false None (c,NoBindings) *) let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = - (** The evarmap of elimclause is assumed to be an extension of hypclause, so - we do not need to merge the universes coming from hypclause. *) + (* The evarmap of elimclause is assumed to be an extension of hypclause, so + we do not need to merge the universes coming from hypclause. *) try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> (* Set the hypothesis name in the message *) @@ -1909,7 +1909,7 @@ let exact_no_check c = let exact_check c = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - (** We do not need to normalize the goal because we just check convertibility *) + (* We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma, ct = Typing.type_of env sigma c in @@ -2021,7 +2021,7 @@ let clear_body ids = let check = try let check (env, sigma, seen) decl = - (** Do no recheck hypotheses that do not depend *) + (* Do no recheck hypotheses that do not depend *) let sigma = if not seen then sigma else if List.exists (fun id -> occur_var_in_decl env sigma id decl) ids then @@ -2848,7 +2848,7 @@ let generalize_dep ?(with_let=false) c = in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in - (** Check that the generalization is indeed well-typed *) + (* Check that the generalization is indeed well-typed *) let (evd, _) = Typing.type_of env evd cl'' in let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST @@ -3021,7 +3021,7 @@ let specialize (c,lbind) ipat = let unfold_body x = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> - (** We normalize the given hypothesis immediately. *) + (* We normalize the given hypothesis immediately. *) let env = Proofview.Goal.env gl in let xval = match Environ.lookup_named x env with | LocalAssum _ -> user_err ~hdr:"unfold_body" diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 03d2a17eee..e273891500 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -281,7 +281,7 @@ struct open TDnet let pat_of_constr c : term_pattern = - (** To each evar we associate a unique identifier. *) + (* To each evar we associate a unique identifier. *) let metas = ref Evar.Map.empty in let rec pat_of_constr c = match Constr.kind c with | Rel _ -> Term DRel @@ -378,7 +378,7 @@ struct let c_id = Opt.reduce (Ident.constr_of id) in let c_id = EConstr.of_constr c_id in let (ctx,wc) = - try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *) + try Termops.align_prod_letin Evd.empty whole_c c_id (* FIXME *) with Invalid_argument _ -> [],c_id in let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in try diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 226a19678f..4e80caa4cc 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -233,7 +233,7 @@ struct let rem = NSet.fold push next rem in aux rem seen | Some false -> - (** The path we took encountered x -> y but not the one in seen *) + (* The path we took encountered x -> y but not the one in seen *) if through then aux (NMap.add n true rem) (NMap.add n true seen) else aux rem seen | Some true -> aux rem seen @@ -357,7 +357,7 @@ let treat_coq_file chan = | None -> acc | Some file_str -> (canonize file_str, ".v") :: acc else acc - | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *) + | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *) in loop acc in diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index db2031c64b..e3dd32fb63 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -132,7 +132,7 @@ let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t) -(** The associated boolean is true if this is a root path. *) +(* The associated boolean is true if this is a root path. *) let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) let get_prefix p l = diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 6c4ea9afa1..0a32879764 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -176,7 +176,7 @@ let set_batch_mode opts = let add_compile opts verbose s = let opts = set_batch_mode opts in if not opts.glob_opt then Dumpglob.dump_to_dotglob (); - (** make the file name explicit; needed not to break up Coq loadpath stuff. *) + (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let s = let open Filename in if is_implicit s diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index edef741ca6..56622abc92 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -95,9 +95,9 @@ let init_color opts = if has_color then begin let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in match colors with - | None -> Topfmt.default_styles (); true (** Default colors *) - | Some "" -> false (** No color output *) - | Some s -> Topfmt.parse_color_config s; true (** Overwrite all colors *) + | None -> Topfmt.default_styles (); true (* Default colors *) + | Some "" -> false (* No color output *) + | Some s -> Topfmt.parse_color_config s; true (* Overwrite all colors *) end else false @@ -144,7 +144,7 @@ let init_gc () = * In this case, we put in place our preferred configuration. *) Gc.set { (Gc.get ()) with - Gc.minor_heap_size = 33554432; (** 4M *) + Gc.minor_heap_size = 33554432; (* 4M *) Gc.space_overhead = 120} (** Main init routine *) diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 3ca2a4ad6b..b5cc74b594 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -294,7 +294,7 @@ let traverse current t = let type_of_constant cb = cb.Declarations.const_type let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = - (** Only keep the transitive dependencies *) + (* Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse (label_of gr) t in let fold obj _ accu = match obj with | VarRef id -> diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 6a32960a9d..66e10f94cd 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -119,6 +119,7 @@ val vernac_monomorphic_flag : vernac_flag (** For the stm, do not use! *) val polymorphic_nowarn : bool attribute + (** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *) val universe_polymorphism_option_name : string list val is_universe_polymorphism : unit -> bool diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index fa1b8eeb3e..d9787bc73c 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -335,8 +335,8 @@ let build_beq_scheme mode kn = | Finite -> mkFix (((Array.make nb_ind 0),i),(names,types,cores)) | BiFinite -> - (** If the inductive type is not recursive, the fixpoint is not - used, so let's replace it with garbage *) + (* If the inductive type is not recursive, the fixpoint is + not used, so let's replace it with garbage *) let subst = List.init nb_ind (fun _ -> mkProp) in Vars.substl subst cores.(i) in diff --git a/vernac/class.ml b/vernac/class.ml index ab43d5c8ff..8374a5c84f 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -66,7 +66,7 @@ let explain_coercion_error g = function let check_reference_arity ref = let env = Global.env () in let c, _ = Typeops.type_of_global_in_context env ref in - if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then + if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (* FIXME *) then raise (CoercionError (NotAClass ref)) let check_arity = function @@ -260,7 +260,7 @@ let add_new_coercion_core coef stre poly source target isid = raise (CoercionError (NoSource source)) in check_source (Some cls); - if not (uniform_cond Evd.empty (** FIXME - for when possibly called with unresolved evars in the future *) + if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *) ctx lvs) then warn_uniform_inheritance coef; let clt = diff --git a/vernac/classes.ml b/vernac/classes.ml index d0cf1c6bee..370df615fc 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -373,7 +373,7 @@ let context poly l = | [] -> assert false | [_] -> Evd.const_univ_entry ~poly sigma | _::_::_ -> - (** TODO: explain this little belly dance *) + (* TODO: explain this little belly dance *) if Lib.sections_are_opened () then begin diff --git a/vernac/classes.mli b/vernac/classes.mli index bb70334342..eb6c0c92e1 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -27,22 +27,22 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit val declare_instance_constant : typeclass -> - Hints.hint_info_expr -> (** priority *) - bool -> (** globality *) - Impargs.manual_explicitation list -> (** implicits *) + Hints.hint_info_expr (** priority *) -> + bool (** globality *) -> + Impargs.manual_explicitation list (** implicits *) -> ?hook:(GlobRef.t -> unit) -> - Id.t -> (** name *) + Id.t (** name *) -> UState.universe_decl -> - bool -> (* polymorphic *) - Evd.evar_map -> (* Universes *) - Constr.t -> (** body *) - Constr.types -> (** type *) + bool (** polymorphic *) -> + Evd.evar_map (** Universes *) -> + Constr.t (** body *) -> + Constr.types (** type *) -> unit val new_instance : - ?abstract:bool -> (** Not abstract by default. *) - ?global:bool -> (** Not global by default. *) - ?refine:bool -> (** Allow refinement *) + ?abstract:bool (** Not abstract by default. *) -> + ?global:bool (** Not global by default. *) -> + ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index f4569ed3e2..338dfa5ef5 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -78,6 +78,7 @@ val interp_fixpoint : (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) + (** [Not used so far] *) val declare_fixpoint : locality -> polymorphic -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8b9cf7d269..4af6415a4d 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -265,7 +265,7 @@ let inductive_levels env evd poly arities inds = else minlev in let minlev = - (** Indices contribute. *) + (* Indices contribute. *) if indices_matter env && List.length ctx > 0 then ( let ilev = sign_level env evd ctx in Univ.sup ilev minlev) @@ -282,15 +282,15 @@ let inductive_levels env evd poly arities inds = let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then - (** Any product is allowed here. *) + (* Any product is allowed here. *) evd, arity :: arities - else (** If in a predicative sort, or asked to infer the type, - we take the max of: - - indices (if in indices-matter mode) - - constructors - - Type(1) if there is more than 1 constructor + else (* If in a predicative sort, or asked to infer the type, + we take the max of: + - indices (if in indices-matter mode) + - constructors + - Type(1) if there is more than 1 constructor *) - (** Constructors contribute. *) + (* Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then @@ -301,7 +301,7 @@ let inductive_levels env evd poly arities inds = in let evd = if len >= 2 && Univ.is_type0m_univ cu then - (** "Polymorphic" type constraint and more than one constructor, + (* "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd Set du @@ -510,7 +510,7 @@ let is_recursive mie = let rec is_recursive_constructor lift typ = match Constr.kind typ with | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || + not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || is_recursive_constructor (lift+1) rest | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest | _ -> false diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index f23085a538..9df8f7c341 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -39,8 +39,8 @@ val do_mutual_inductive : associated schemes *) type one_inductive_impls = - Impargs.manual_implicits (** for inds *)* - Impargs.manual_implicits list (** for constrs *) + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) val declare_mutual_inductive_with_eliminations : mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index e62ae99159..edce8e255c 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -211,7 +211,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let univs = Evd.check_univ_decl ~poly sigma decl in (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in - (** FIXME: include locality *) + (* FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 898de7b166..41057f8ab2 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -27,7 +27,7 @@ let warn_local_declaration = let get_locality id ~kind = function | Discharge -> - (** If a Let is defined outside a section, then we consider it as a local definition *) + (* If a Let is defined outside a section, then we consider it as a local definition *) warn_local_declaration (id,kind); true | Local -> true diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 6c7117b513..68d6db75ee 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -125,12 +125,12 @@ let display_eq ~flags env sigma t1 t2 = printed alike. *) let rec pr_explicit_aux env sigma t1 t2 = function | [] -> - (** no specified flags: default. *) + (* no specified flags: default. *) (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2)) | flags :: rem -> let equal = display_eq ~flags env sigma t1 t2 in if equal then - (** The two terms are the same from the user point of view *) + (* The two terms are the same from the user point of view *) pr_explicit_aux env sigma t1 t2 rem else let open Constrextern in @@ -142,12 +142,12 @@ let rec pr_explicit_aux env sigma t1 t2 = function let explicit_flags = let open Constrextern in - [ []; (** First, try with the current flags *) - [print_implicits]; (** Then with implicit *) - [print_universes]; (** Then with universes *) - [print_universes; print_implicits]; (** With universes AND implicits *) - [print_implicits; print_coercions; print_no_symbol]; (** Then more! *) - [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ] + [ []; (* First, try with the current flags *) + [print_implicits]; (* Then with implicit *) + [print_universes]; (* Then with universes *) + [print_universes; print_implicits]; (* With universes AND implicits *) + [print_implicits; print_coercions; print_no_symbol]; (* Then more! *) + [print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ] let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags @@ -328,7 +328,7 @@ let explain_actual_type env sigma j t reason = let env = make_all_name_different env sigma in let j = j_nf_betaiotaevar env sigma j in let t = Reductionops.nf_betaiota env sigma t in - (** Actually print *) + (* Actually print *) let pe = pr_ne_context_of (str "In environment") env sigma in let pc = pr_leconstr_env env sigma (Environ.j_val j) in let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in @@ -774,7 +774,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let (_, constraints) = Evd.extract_all_conv_pbs sigma in let tcs = Evd.get_typeclass_evars sigma in let undef = Evd.undefined_map sigma in - (** Only keep evars that are subject to resolution and members of the given + (* Only keep evars that are subject to resolution and members of the given component. *) let is_kept evk _ = match comp with | None -> Evar.Set.mem evk tcs @@ -1112,7 +1112,7 @@ let error_ill_formed_inductive env c v = let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env (Evd.from_env env) v in - let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in + let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (* FIXME *) 0 in str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ strbrk (if atomic then "it must be " else "its conclusion must be ") ++ diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 9bd095aa52..d29f66f81f 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -307,7 +307,7 @@ let warn_cannot_build_congruence = strbrk "Cannot build congruence scheme because eq is not found") let declare_congr_scheme ind = - if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (** FIXME *) then begin + if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with e when CErrors.noncritical e -> false diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 82434afbbd..dccd776fa8 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1467,7 +1467,7 @@ let add_notation_in_scope local df env c mods scope = notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); - (** Order is important here! *) + (* Order is important here! *) notobj_onlyparse = onlyparse; notobj_coercion = coe; notobj_onlyprint = sd.only_printing; @@ -1486,7 +1486,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ let level, i_typs, onlyprint = if not (is_numeral symbs) then begin let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in - (** If the only printing flag has been explicitly requested, put it back *) + (* If the only printing flag has been explicitly requested, put it back *) let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in let _,_,_,typs = sy.synext_level in Some sy.synext_level, typs, onlyprint @@ -1507,7 +1507,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); - (** Order is important here! *) + (* Order is important here! *) notobj_onlyparse = onlyparse; notobj_coercion = coe; notobj_onlyprint = onlyprint; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index f18227039f..6642d04c98 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -381,7 +381,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with + match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (* FIXME *) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> @@ -503,7 +503,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx @@ -649,7 +649,7 @@ let declare_obligation prg obl body ty uctx = const_entry_inline_code = false; const_entry_feedback = None; } in - (** ppedrot: seems legit to have obligations as local *) + (* ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in @@ -857,9 +857,9 @@ let obligation_terminator ?univ_hook name num guard auto pf = let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); - (** Declare the obligation ourselves and drop the hook *) + (* Declare the obligation ourselves and drop the hook *) let prg = get_info (ProgMap.find name !from_prg) in - (** Ensure universes are substituted properly in body and type *) + (* Ensure universes are substituted properly in body and type *) let body = EConstr.to_constr sigma (EConstr.of_constr body) in let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in let ctx = Evd.evar_universe_context sigma in @@ -885,14 +885,14 @@ let obligation_terminator ?univ_hook name num guard auto pf = let () = obls.(num) <- obl in let prg_ctx = if pi2 (prg.prg_kind) then (* Polymorphic *) - (** We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) + (* We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx else - (** The first obligation, if defined, - declares the univs of the constant, - each subsequent obligation declares its own additional - universes and constraints if any *) + (* The first obligation, if defined, + declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) if defined then UState.make (Global.universes ()) else ctx in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e7c1e29beb..8535585749 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -363,7 +363,7 @@ open Pputils match factorize l with | (xl,((c', t') as r))::l' when (c : bool) == c' && Pervasives.(=) t t' -> - (** FIXME: we need equality on constr_expr *) + (* FIXME: we need equality on constr_expr *) (idl@xl,r)::l' | l' -> (idl,(c,t))::l' diff --git a/vernac/record.ml b/vernac/record.ml index f6dbcb5291..ffd4f654c6 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -321,7 +321,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f ~proj_arg:i (Label.of_id fid) in - (** Already defined by declare_mind silently *) + (* Already defined by declare_mind silently *) let kn = Projection.Repr.constant p in Declare.definition_message fid; kn, mkProj (Projection.make p false,mkRel 1) diff --git a/vernac/search.ml b/vernac/search.ml index 1fac28358a..6610789626 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -172,8 +172,8 @@ let prioritize_search seq fn = (** Filters *) -(** This function tries to see whether the conclusion matches a pattern. *) -(** FIXME: this is quite dummy, we may find a more efficient algorithm. *) +(** This function tries to see whether the conclusion matches a pattern. + FIXME: this is quite dummy, we may find a more efficient algorithm. *) let rec pattern_filter pat ref env sigma typ = let typ = Termops.strip_outer_cast sigma typ in if Constr_matching.is_matching env sigma pat typ then true diff --git a/vernac/search.mli b/vernac/search.mli index 0dc82c1c3f..ecbb02bc68 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -49,16 +49,16 @@ val search_about : int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = - (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) | Name_Pattern of Str.regexp - (** Whether the object type satisfies a pattern *) + (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) | Type_Pattern of Pattern.constr_pattern - (** Whether some subtype of object type satisfies a pattern *) + (** Whether the object type satisfies a pattern *) | SubType_Pattern of Pattern.constr_pattern - (** Whether the object pertains to a module *) + (** Whether some subtype of object type satisfies a pattern *) | In_Module of Names.DirPath.t - (** Bypass the Search blacklist *) + (** Whether the object pertains to a module *) | Include_Blacklist + (** Bypass the Search blacklist *) type 'a coq_object = { coq_object_prefix : string list; diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 4bf76dae51..4065bb9c1f 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -222,20 +222,21 @@ let diff_tag_stack = ref [] (* global, just like std_ft *) (** Not thread-safe. We should put a lock somewhere if we print from different threads. Do we? *) let make_style_stack () = - (** Default tag is to reset everything *) + (* Default tag is to reset everything *) let style_stack = ref [] in let peek () = match !style_stack with - | [] -> default_style (** Anomalous case, but for robustness *) + | [] -> default_style (* Anomalous case, but for robustness *) | st :: _ -> st in let open_tag tag = let (tpfx, ttag) = split_tag tag in if tpfx = end_pfx then "" else let style = get_style ttag in - (** Merge the current settings and the style being pushed. This allows - restoring the previous settings correctly in a pop when both set the same - attribute. Example: current settings have red FG, the pushed style has - green FG. When popping the style, we should set red FG, not default FG. *) + (* Merge the current settings and the style being pushed. This + allows restoring the previous settings correctly in a pop + when both set the same attribute. Example: current settings + have red FG, the pushed style has green FG. When popping the + style, we should set red FG, not default FG. *) let style = Terminal.merge (peek ()) style in let diff = Terminal.diff (peek ()) style in style_stack := style :: !style_stack; @@ -247,7 +248,7 @@ let make_style_stack () = if tpfx = start_pfx then "" else begin if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []); match !style_stack with - | [] -> (** Something went wrong, we fallback *) + | [] -> (* Something went wrong, we fallback *) Terminal.eval default_style | cur :: rem -> style_stack := rem; if cur = (peek ()) then "" else diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f5d68a2199..3fa3681661 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -681,14 +681,14 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> None in if Option.has_some is_defclass then - (** Definitional class case *) + (* Definitional class case *) let (id, bl, c, l) = Option.get is_defclass in let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] else if List.for_all is_record indl then - (** Mutual record case *) + (* Mutual record case *) let check_kind ((_, _, _, kind, _), _) = match kind with | Variant -> user_err (str "The Variant keyword does not support syntax { ... }.") @@ -704,14 +704,14 @@ let vernac_inductive ~atts cum lo finite indl = let unpack ((id, bl, c, _, decl), _) = match decl with | RecordDecl (oc, fs) -> (id, bl, c, oc, fs) - | Constructors _ -> assert false (** ruled out above *) + | Constructors _ -> assert false (* ruled out above *) in let ((_, _, _, kind, _), _) = List.hd indl in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in vernac_record ~template udecl cum kind atts.polymorphic finite recordl else if List.for_all is_constructor indl then - (** Mutual inductive case *) + (* Mutual inductive case *) let check_kind ((_, _, _, kind, _), _) = match kind with | (Record | Structure) -> user_err (str "The Record keyword is for types defined using the syntax { ... }.") @@ -1992,7 +1992,7 @@ let vernac_search ~atts s gopt r = let vernac_locate = function | LocateAny {v=AN qid} -> print_located_qualid qid | LocateTerm {v=AN qid} -> print_located_term qid - | LocateAny {v=ByNotation (ntn, sc)} (** TODO : handle Ltac notations *) + | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *) | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = Pfedit.get_current_context () in Notation.locate_notation diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 1e6c40c829..417c9ebfbd 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -247,11 +247,11 @@ type vernac_argument_status = { } type extend_name = - (** Name of the vernac entry where the tactic is defined, typically found - after the VERNAC EXTEND statement in the source. *) + (* Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) string * - (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch - is given an offset, starting from zero. *) + (* Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) int type nonrec vernac_expr = diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 2541f73582..05687afd8b 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -42,8 +42,11 @@ and vernac_sideff_type = Names.Id.t list and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) + and solving_tac = bool (** a terminator *) + and anon_abstracting_tac = bool (** abstracting anonymously its result *) + and proof_block_name = string (** open type of delimiters *) type vernac_when = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 8b07be8b16..0d43eb1ee8 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -58,8 +58,11 @@ and vernac_sideff_type = Names.Id.t list and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) + and solving_tac = bool (** a terminator *) + and anon_abstracting_tac = bool (** abstracting anonymously its result *) + and proof_block_name = string (** open type of delimiters *) type vernac_when = @@ -86,7 +89,7 @@ type (_, _) ty_sig = ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig -type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml +type ty_ml = TyML : bool (* deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml (** Wrapper to dynamically extend vernacular commands. *) val vernac_extend : |