diff options
64 files changed, 187 insertions, 203 deletions
@@ -2187,7 +2187,7 @@ Changes from V7.3.1 to V7.4 Symbolic notations - Introduction of a notion of scope gathering notations in a consistent set; - a notation sets has been developped for nat, Z and R (undocumented) + a notation sets has been developed for nat, Z and R (undocumented) - New command "Notation" for declaring notations simultaneously for parsing and printing (see chap 10 of the reference manual) - Declarations with only implicit arguments now handled (e.g. the diff --git a/INSTALL.ide b/INSTALL.ide index 13e741e34..6e41b2d05 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -119,5 +119,5 @@ TROUBLESHOOTING rid of the problem is to edit by hand your coqiderc (either /home/<user>/.config/coq/coqiderc under Linux, or C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows) - and replace any occurence of MOD4 by MOD1. + and replace any occurrence of MOD4 by MOD1. diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index 9e243eead..6a69c5793 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -167,7 +167,7 @@ kernel/univ.ml was modified. The new API forces every universe to be declared before it is mentionned in any constraint. This forces to declare every universe to be >= Set or > Set. Every universe variable introduced during elaboration is >= Set. Every _global_ universe is now -declared explicitely > Set, _after_ typechecking the definition. In +declared explicitly > Set, _after_ typechecking the definition. In polymorphic definitions Type@{i} ranges over Set and any other universe j. However, at instantiation time for polymorphic references, one can try to instantiate a universe parameter with Prop as well, if the diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex index 8d116de26..ae4b569b3 100644 --- a/dev/v8-syntax/memo-v8.tex +++ b/dev/v8-syntax/memo-v8.tex @@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching. \subsection{Occurrences} To avoid ambiguity between a numeric literal and the optionnal -occurence numbers of this term, the occurence numbers are put after +occurrence numbers of this term, the occurrence numbers are put after the term itself. This applies to tactic \TERM{pattern} and also \TERM{unfold} \begin{transbox} diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index fbb866e87..48b61827d 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -228,7 +228,7 @@ kernel is intentionally small to limit the risk of conceptual or accidental implementation bugs. \item[The Objective Caml compiler] The {\Coq} kernel is written using the Objective Caml language but it uses only the most standard features -(no object, no label ...), so that it is highly unprobable that an +(no object, no label ...), so that it is highly improbable that an Objective Caml bug breaks the consistency of {\Coq} without breaking all other kinds of features of {\Coq} or of other software compiled with Objective Caml. @@ -710,7 +710,7 @@ There are also ``simple enough'' propositions for which you can prove the equality without requiring any extra axioms. This is typically the case for propositions defined deterministically as a first-order inductive predicate on decidable sets. See for instance in question -\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of +\ref{le-uniqueness} an axiom-free proof of the uniqueness of the proofs of the proposition {\tt le m n} (less or equal on {\tt nat}). % It is an ongoing work of research to natively include proof @@ -1497,7 +1497,7 @@ while {\assert} is. \Question{What can I do if \Coq can not infer some implicit argument ?} -You can state explicitely what this implicit argument is. See \ref{implicit}. +You can state explicitly what this implicit argument is. See \ref{implicit}. \Question{How can I explicit some implicit argument ?}\label{implicit} @@ -1625,14 +1625,14 @@ Fail Definition max (n p : nat) := if n <= p then p else n. As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a statement that belongs to the mathematical world. There are many ways to prove such a proposition, either by some computation, or using some already -proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy, +proven theorems. For instance, proving $3-2 \leq 2^{45503}$ is very easy, using some theorems on arithmetical operations. If you compute both numbers before comparing them, you risk to use a lot of time and space. On the contrary, a function for computing the greatest of two natural numbers is an algorithm which, called on two natural numbers -$n$ and $p$, determines wether $n\leq p$ or $p < n$. +$n$ and $p$, determines whether $n\leq p$ or $p < n$. Such a function is a \emph{decision procedure} for the inequality of \texttt{nat}. The possibility of writing such a procedure comes directly from de decidability of the order $\leq$ on natural numbers. @@ -1706,7 +1706,7 @@ immediate, whereas one can't wait for the result of This is normal. Your definition is a simple recursive function which returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified -function}, i.e. a complex object, able not only to tell wether $n\leq p$ +function}, i.e. a complex object, able not only to tell whether $n\leq p$ or $p<n$, but also of building a complete proof of the correct inequality. What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min} and \texttt{max} is the building of a huge proof term. @@ -2404,8 +2404,8 @@ You can use {\tt coqdoc}. \Question{How can I generate some dependency graph from my development?} -You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002. -This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/). +You can use the tool \verb|coqgraph| developed by Philippe Audebaud in 2002. +This tool transforms dependencies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/). \Question{How can I cite some {\Coq} in my latex document?} @@ -2539,7 +2539,7 @@ modifiers keys available through GTK. The straightest way to get rid of the problem is to edit by hand your coqiderc (either \verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\ \verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) - and replace any occurence of \texttt{MOD4} by \texttt{MOD1}. +and replace any occurrence of \texttt{MOD4} by \texttt{MOD1}. @@ -2638,7 +2638,7 @@ existential variable which eventually got erased by some computation. You may backtrack to the faulty occurrence of {\eauto} or {\eapply} and give the missing argument an explicit value. Alternatively, you can use the commands \texttt{Show Existentials.} and -\texttt{Existential.} to display and instantiate the remainig +\texttt{Existential.} to display and instantiate the remaining existential variables. diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 018d73908..cd8222269 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -182,8 +182,8 @@ bound if it is an atomic universe (i.e. not an algebraic max()). experimental and is likely to change in future versions. \end{flushleft} -The syntax has been extended to allow users to explicitely bind names to -universes and explicitely instantantiate polymorphic +The syntax has been extended to allow users to explicitly bind names to +universes and explicitly instantiate polymorphic definitions. Currently, binding is implicit at the first occurrence of a universe name. For example, i and j below are introduced by the annotations attached to Types. @@ -200,16 +200,16 @@ we are using $A : Type@{i} <= Type@{j}$, hence the generated constraint. Note that the names here are not bound in the final definition, they just allow to specify locally what relations should hold. In the term and in general in proof mode, universe names -introduced in the types can be refered to in terms. +introduced in the types can be referred to in terms. -Definitions can also be instantiated explicitely, giving their full instance: +Definitions can also be instantiated explicitly, giving their full instance: \begin{coq_example} Check (pidentity@{Set}). Check (le@{i j}). \end{coq_example} User-named universes are considered rigid for unification and are never -miminimized. +minimized. Finally, two commands allow to name \emph{global} universes and constraints. diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index 5f7b6dc95..ed1d336d9 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -419,7 +419,7 @@ the hypotheses), or a comma-separated list of either hypothesis name, or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences can be specified after every hypothesis after the {\TERM{at}} keyword. {\em concl} is either empty or \TERM{*}, and can be followed -by occurences. +by occurrences. \begin{transbox} \TRANS{in Goal}{in |- *} diff --git a/engine/evd.ml b/engine/evd.ml index 64aad8082..79e73bda5 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -766,7 +766,7 @@ let cmap f evd = { evd with metas = Metamap.map (map_clb f) evd.metas; defn_evars = EvMap.map (map_evar_info f) evd.defn_evars; - undf_evars = EvMap.map (map_evar_info f) evd.defn_evars + undf_evars = EvMap.map (map_evar_info f) evd.undf_evars } (* spiwack: deprecated *) diff --git a/engine/termops.ml b/engine/termops.ml index 937471cf7..5a55d47fd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -561,7 +561,7 @@ let free_rels m = in frec 1 Int.Set.empty m -(* collects all metavar occurences, in left-to-right order, preserving +(* collects all metavar occurrences, in left-to-right order, preserving * repetitions and all. *) let collect_metas c = diff --git a/ide/coq.mli b/ide/coq.mli index a72c67b43..2dc5ad307 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -16,7 +16,7 @@ type coqtop Liveness management of coqtop is automatic. Whenever a coqtop dies abruptly, this module is responsible for relaunching the whole process. The reset handler set through [set_reset_handler] will be called after such an - abrupt failure. It is also called when explicitely requesting coqtop to + abrupt failure. It is also called when explicitly requesting coqtop to reset. *) type 'a task @@ -29,7 +29,7 @@ type 'a task ([is_computing] will answer [true]), and any other task submission will be rejected by [try_grab]. - Any exception occuring within the task will trigger a coqtop reset. + Any exception occurring within the task will trigger a coqtop reset. Beware, because of the GTK scheduler, you never know when a task will actually be executed. If you need to sequentialize imperative actions, you @@ -43,7 +43,7 @@ val bind : 'a task -> ('a -> 'b task) -> 'b task (** Monadic binding of tasks *) val lift : (unit -> 'a) -> 'a task -(** Return the impertative computation waiting to be processed. *) +(** Return the imperative computation waiting to be processed. *) val seq : unit task -> 'a task -> 'a task (** Sequential composition *) diff --git a/ide/coqide.ml b/ide/coqide.ml index e591f205f..5fdb4a2a4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1059,8 +1059,8 @@ let build_ui () = ("Hide", "_Hide", `MISSING_IMAGE, ~callback:(fun _ -> let sess = notebook#current_term in toggle_proof_visibility sess.buffer sess.analyzed_view#get_insert), "Hide proof", "h"); *) - ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurence", "less"); - ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurence", "greater"); + ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurrence", "less"); + ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurrence", "greater"); ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); ] end; diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 621833dde..4ebf9a62e 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -12,7 +12,7 @@ } -(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *) +(* Replace all occurrences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *) let digit = ['0'-'9''A'-'Z''a'-'z'] let short = digit digit digit digit diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 14cbf92eb..b672e016b 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -141,7 +141,7 @@ object(self) (** We don't care about atomicity. Return: 1. `OK when there was no error, `FAIL otherwise - 2. `NOOP if no write occured, `WRITE otherwise + 2. `NOOP if no write occurred, `WRITE otherwise *) method private process_action = function | Insert ins -> diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index a3721af66..eee928989 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -28,7 +28,7 @@ val free_vars_of_binders : ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list (** Returns the generalizable free ids in left-to-right - order with the location of their first occurence *) + order with the location of their first occurrence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> glob_constr -> (Id.t * Loc.t) list diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 399fa843f..0553a5ed7 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -844,7 +844,6 @@ value coq_interprete } Instruct(SETFIELD1){ - int i, j, size, size_aux; print_instr("SETFIELD1"); caml_modify(&Field(accu, 1),*sp); sp++; @@ -884,19 +883,17 @@ value coq_interprete Instruct(PROJ){ print_instr("PROJ"); if (Is_accu (accu)) { + value block; /* Skip over the index of projected field */ pc++; - /* Save the argument on the stack */ - *--sp = accu; /* Create atom */ - Alloc_small(accu, 2, ATOM_PROJ_TAG); - Field(accu, 0) = Field(coq_global_data, *pc); - Field(accu, 1) = sp[0]; - sp[0] = accu; + Alloc_small(block, 2, ATOM_PROJ_TAG); + Field(block, 0) = Field(coq_global_data, *pc); + Field(block, 1) = accu; /* Create accumulator */ Alloc_small(accu, 2, Accu_tag); Code_val(accu) = accumulate; - Field(accu,1) = *sp++; + Field(accu, 1) = block; } else { accu = Field(accu, *pc++); } @@ -1110,7 +1107,6 @@ value coq_interprete /* returns the sum plus one with a carry */ uint32_t s; s = (uint32_t)accu + (uint32_t)*sp++ + 1; - value block; if( (uint32_t)s <= (uint32_t)accu ) { /* carry */ Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */ @@ -1271,7 +1267,7 @@ value coq_interprete Instruct (COMPAREINT31) { /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ - /* assumes Inudctive _ : _ := Eq | Lt | Gt */ + /* assumes Inductive _ : _ := Eq | Lt | Gt */ print_instr("COMPAREINT31"); if ((uint32_t)accu == (uint32_t)*sp) { accu = 1; /* 2*0+1 */ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 416e5e532..c9bcdc32f 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -103,7 +103,6 @@ static int coq_vm_initialized = 0; value init_coq_vm(value unit) /* ML */ { - int i; if (coq_vm_initialized == 1) { fprintf(stderr,"already open \n");fflush(stderr);} else { @@ -135,7 +134,6 @@ void realloc_coq_stack(asize_t required_space) { asize_t size; value * new_low, * new_high, * new_sp; - value * p; size = coq_stack_high - coq_stack_low; do { size *= 2; diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 007f61b27..528babebf 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -21,7 +21,6 @@ value coq_kind_of_closure(value v) { opcode_t * c; - int res; int is_app = 0; c = Code_val(v); if (Is_instruction(c, GRAB)) return Val_int(0); diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 3b01538b9..ec2c334b6 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -82,12 +82,17 @@ let fold_strategy f { var_opacity; cst_opacity; } accu = let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate) (* Unfold the first constant only if it is "more transparent" than the - second one. In case of tie, expand the second one. *) + second one. In case of tie, use the recommended default. *) let oracle_order f o l2r k1 k2 = match get_strategy o f k1, get_strategy o f k2 with - | Expand, _ -> true - | Level n1, Opaque -> true - | Level n1, Level n2 -> n1 < n2 - | _ -> l2r (* use recommended default *) + | Expand, Expand -> l2r + | Expand, (Opaque | Level _) -> true + | (Opaque | Level _), Expand -> false + | Opaque, Opaque -> l2r + | Level _, Opaque -> true + | Opaque, Level _ -> false + | Level n1, Level n2 -> + if Int.equal n1 n2 then l2r + else n1 < n2 let get_strategy o = get_strategy o (fun x -> x) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 155ad7987..697f482c4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -290,11 +290,7 @@ let typecheck_inductive env mie = let full_polymorphic () = let defu = Term.univ_of_sort def_level in let is_natural = - type_in_type env || (UGraph.check_leq (universes env') infu defu && - not (is_type0m_univ defu && not is_unit) - (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *) - - ) + type_in_type env || (UGraph.check_leq (universes env') infu defu) in let _ = (** Impredicative sort, always allow *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 687b740f6..98b2d6d2e 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -481,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 = in Array.equal eq_branch br1 br2 -(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *) +(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *) let rec hash_mllambda gn n env t = match t with | MLlocal ln -> combinesmall 1 (LNmap.find ln env) @@ -979,7 +979,7 @@ let compile_prim decl cond paux = let args = Array.map opt_prim_aux args in app_prim (Coq_primitive(op,None)) args (* - TODO: check if this inling was useful + TODO: check if this inlining was useful begin match op with | Int31lt -> if Sys.word_size = 64 then diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index cb08b5058..263befd21 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -277,7 +277,7 @@ and reduce_lapp substf lids body substa largs = | [], _::_ -> simplify_app substf body substa (Array.of_list largs) -(* [occurence kind k lam]: +(* [occurrence kind k lam]: If [kind] is [true] return [true] if the variable [k] does not appear in [lam], return [false] if the variable appear one time and not under a lambda, a fixpoint, a cofixpoint; else raise Not_found. @@ -285,7 +285,7 @@ and reduce_lapp substf lids body substa largs = else raise [Not_found] *) -let rec occurence k kind lam = +let rec occurrence k kind lam = match lam with | Lrel (_,n) -> if Int.equal n k then @@ -294,35 +294,35 @@ let rec occurence k kind lam = | Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind | Lprod(dom, codom) -> - occurence k (occurence k kind dom) codom + occurrence k (occurrence k kind dom) codom | Llam(ids,body) -> - let _ = occurence (k+Array.length ids) false body in kind + let _ = occurrence (k+Array.length ids) false body in kind | Llet(_,def,body) -> - occurence (k+1) (occurence k kind def) body + occurrence (k+1) (occurrence k kind def) body | Lapp(f, args) -> - occurence_args k (occurence k kind f) args + occurrence_args k (occurrence k kind f) args | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) -> - occurence_args k kind args + occurrence_args k kind args | Lcase(_,t,a,br) -> - let kind = occurence k (occurence k kind t) a in + let kind = occurrence k (occurrence k kind t) a in let r = ref kind in Array.iter (fun (_,ids,c) -> - r := occurence (k+Array.length ids) kind c && !r) br; + r := occurrence (k+Array.length ids) kind c && !r) br; !r | Lif (t, bt, bf) -> - let kind = occurence k kind t in - kind && occurence k kind bt && occurence k kind bf + let kind = occurrence k kind t in + kind && occurrence k kind bt && occurrence k kind bf | Lfix(_,(ids,ltypes,lbodies)) | Lcofix(_,(ids,ltypes,lbodies)) -> - let kind = occurence_args k kind ltypes in - let _ = occurence_args (k+Array.length ids) false lbodies in + let kind = occurrence_args k kind ltypes in + let _ = occurrence_args (k+Array.length ids) false lbodies in kind -and occurence_args k kind args = - Array.fold_left (occurence k) kind args +and occurrence_args k kind args = + Array.fold_left (occurrence k) kind args let occur_once lam = - try let _ = occurence 1 true lam in true + try let _ = occurrence 1 true lam in true with Not_found -> false (* [remove_let lam] remove let expression in [lam] if the variable is *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 29c6009ce..6e1c3c5b7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -733,14 +733,9 @@ let vm_conv cv_pb env t1 t2 = Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); fconv cv_pb false (fun _->None) env t1 t2 - -let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None)) - -let set_default_conv f = default_conv := f - let default_conv cv_pb ?(l2r=false) env t1 t2 = try - !default_conv ~l2r cv_pb env t1 t2 + fconv cv_pb false (fun _ -> None) env t1 t2 with Not_found | Invalid_argument _ -> Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion"); fconv cv_pb false (fun _->None) env t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index a22f3730e..2c1c0ec05 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -93,7 +93,6 @@ val set_nat_conv : (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function -val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8af2efc58..27e184ea3 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -40,8 +40,6 @@ let conv_vect fconv vect1 vect2 cu = !rcu else raise NotConvertible -let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) - let rec conv_val env pb k v1 v2 cu = if v1 == v2 then cu else conv_whd env pb k (whd_val v1) (whd_val v2) cu @@ -219,7 +217,6 @@ and conv_eq_vect env vt1 vt2 cu = else raise NotConvertible let vconv pb env t1 t2 = - infos := create_clos_infos betaiotazeta env; let _cu = try conv_eq env pb t1 t2 (universes env) with NotConvertible -> @@ -230,14 +227,3 @@ let vconv pb env t1 t2 = in () let _ = Reduction.set_vm_conv vconv - -let use_vm = ref false - -let set_use_vm b = - use_vm := b; - if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb) - else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb) - -let use_vm _ = !use_vm - - diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 096d31ac8..1a29a4d51 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,8 +12,6 @@ open Reduction (********************************************************************** s conversion functions *) -val use_vm : unit -> bool -val set_use_vm : bool -> unit val vconv : conv_pb -> types conversion_function val val_of_constr : env -> constr -> values diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index cefb4af89..ac2eab352 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -36,10 +36,10 @@ type t (** Several exceptions can be raised when parsing an Xml document : {ul {li {!Xml.Error} is raised when an xml parsing error occurs. the - {!Xml.error_msg} tells you which error occured during parsing - and the {!Xml.error_pos} can be used to retreive the document - location where the error occured at.} - {li {!Xml.File_not_found} is raised when and error occured while + {!Xml.error_msg} tells you which error occurred during parsing + and the {!Xml.error_pos} can be used to retrieve the document + location where the error occurred at.} + {li {!Xml.File_not_found} is raised when an error occurred while opening a file with the {!Xml.parse_file} function.} } *) @@ -71,13 +71,13 @@ val error : error -> string (** Get the Xml error message as a string. *) val error_msg : error_msg -> string -(** Get the line the error occured at. *) +(** Get the line the error occurred at. *) val line : error_pos -> int -(** Get the relative character range (in current line) the error occured at.*) +(** Get the relative character range (in current line) the error occurred at.*) val range : error_pos -> int * int -(** Get the absolute character range the error occured at. *) +(** Get the absolute character range the error occurred at. *) val abs_range : error_pos -> int * int val pos : Lexing.lexbuf -> error_pos @@ -98,7 +98,7 @@ val make : source -> t in the original Xmllight)}. *) val check_eof : t -> bool -> unit -(** Once the parser is configurated, you can run the parser on a any kind +(** Once the parser is configured, you can run the parser on a any kind of xml document source to parse its contents into an Xml data structure. When [do_not_canonicalize] is set, the XML document is given as diff --git a/library/impargs.ml b/library/impargs.ml index 94f53219e..d15a02fea 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -104,7 +104,7 @@ let set_maximality imps b = inferable following a rigid path (useful to know how to print a partial application) -- [Manual] means the argument has been explicitely set as implicit. +- [Manual] means the argument has been explicitly set as implicit. We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. diff --git a/library/impargs.mli b/library/impargs.mli index 1d3a73e94..30f2e30f9 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -59,8 +59,8 @@ type implicit_explanation = inferable following a rigid path (useful to know how to print a partial application) *) | Manual - (** means the argument has been explicitely set as implicit. *) - + (** means the argument has been explicitly set as implicit. *) + (** We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 8e8392961..c6d5f3b92 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -70,7 +70,7 @@ let ttree_remove ttree str = remove ttree 0 -(* Errors occuring while lexing (explained as "Lexer error: ...") *) +(* Errors occurring while lexing (explained as "Lexer error: ...") *) module Error = struct diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 797b031fe..2e47e07a3 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -298,7 +298,7 @@ module Prim = struct let gec_gen x = make_gen_entry uprim x - (* Entries that can be refered via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen (rawwit wit_pre_ident) "preident" let ident = gec_gen (rawwit wit_ident) "ident" @@ -334,7 +334,7 @@ module Constr = struct let gec_constr = make_gen_entry uconstr (rawwit wit_constr) - (* Entries that can be refered via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Gram.entry table *) let constr = gec_constr "constr" let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr @@ -367,7 +367,7 @@ module Tactic = (* Main entry for extensions *) let simple_tactic = Gram.entry_create "tactic:simple_tactic" - (* Entries that can be refered via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = make_gen_entry utactic (rawwit wit_open_constr) "open_constr" diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index bc5a39002..ee7341a4a 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -283,7 +283,7 @@ end. (** Quotienting a polynomial by the relation X_i^2 ~ X_i *) -(* Remove the multiple occurences of monomials x_k *) +(* Remove the multiple occurrences of monomials x_k *) Fixpoint reduce_aux k p := match p with diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index f8ddd5f80..d8c5b8a95 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -212,7 +212,7 @@ let close_previous_case pts = Proof.is_done pts then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") + Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...") | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus () | _ -> error "Not inside a proof per cases or induction." diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index fbcd01a15..cf97ae3ab 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -193,7 +193,7 @@ beginning of files. Possible clashes are dealt with. in extracted code. -* A few constants are explicitely declared to be inlined in extracted code. +* A few constants are explicitly declared to be inlined in extracted code. For the moment there are: Wf.Acc_rec Wf.Acc_rect @@ -234,12 +234,12 @@ Those two commands enable a precise control of what is inlined and what is not. Print Extraction Inline. -Sum up the current state of the table recording the custom inlings +Sum up the current state of the table recording the custom inlinings (Extraction (No)Inline). Reset Extraction Inline. -Put the table recording the custom inlings back to empty. +Put the table recording the custom inlinings back to empty. As a consequence, there is no more need for options inside the commands of extraction: diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 9fdb0205f..6fc1195fb 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -490,8 +490,8 @@ let ast_occurs_itvl k k' t = ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false with Found -> true -(* Number of occurences of [Rel 1] in [t], with special treatment of match: - occurences in different branches aren't added, but we rather use max. *) +(* Number of occurrences of [Rel 1] in [t], with special treatment of match: + occurrences in different branches aren't added, but we rather use max. *) let nb_occur_match = let rec nb k = function @@ -851,7 +851,7 @@ let factor_branches o typ br = else Some (br_factor, br_set) end -(*s If all branches are functions, try to permut the case and the functions. *) +(*s If all branches are functions, try to permute the case and the functions. *) let rec merge_ids ids ids' = match ids,ids' with | [],l -> l @@ -1127,7 +1127,7 @@ let term_expunge s (ids,c) = MLlam (Dummy, ast_lift 1 c) else named_lams ids c -(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and +(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and purge the args of [MLrel r] corresponding to a [dummy_name]. It makes eta-expansion if needed. *) @@ -1351,10 +1351,10 @@ let is_not_strict t = We expand small terms with at least one non-strict variable (i.e. a variable that may not be evaluated). - Futhermore we don't expand fixpoints. + Furthermore we don't expand fixpoints. - Moreover, as mentionned by X. Leroy (bug #2241), - inling a constant from inside an opaque module might + Moreover, as mentioned by X. Leroy (bug #2241), + inlining a constant from inside an opaque module might break types. To avoid that, we require below that both [r] and its body are globally visible. This isn't fully satisfactory, since [r] might not be visible (functor), diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 96c4eb01e..a77af03dc 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -212,6 +212,7 @@ let extend_with_auto_hints l seq gl= match repr_hint p_a_t.code with Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> + let (c, _, _) = c in (try let gr = global_of_constr c in let typ=(pf_unsafe_type_of gl c) in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index bc7e6f8b0..e7732a503 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -379,7 +379,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list = (** [finduction id filter g] tries to apply functional induction on - an occurence of function [id] in the conclusion of goal [g]. If + an occurrence of function [id] in the conclusion of goal [g]. If [id]=[None] then calls to any function are selected. In any case [heuristic] is used to select the most pertinent occurrence. *) let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 0f10636f0..179e8fe8d 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -6,7 +6,7 @@ open Misctypes val get_pattern_id : cases_pattern -> Id.t list (* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. - [pat] must not contain occurences of anonymous pattern + [pat] must not contain occurrences of anonymous pattern *) val pattern_to_term : cases_pattern -> glob_constr @@ -64,7 +64,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr (* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. the result does not share variables with [avoid]. This function create - a fresh variable for each occurence of the anonymous pattern. + a fresh variable for each occurrence of the anonymous pattern. Also returns a mapping from old variables to new ones and the concatenation of [avoid] with the variables appearing in the result. diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 69e055c23..60c58730a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs - [ind1] and [ind2]. identifiers occuring in both arrays [args1] and + [ind1] and [ind2]. identifiers occurring in both arrays [args1] and [args2] are considered linked (i.e. are the same variable) in the new graph. diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 024720449..0261d7349 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -23,7 +23,7 @@ struct - None , Some v -> \]-oo,v\] - Some v, None -> \[v,+oo\[ - Some v, Some v' -> \[v,v'\] - Intervals needs to be explicitely normalised. + Intervals needs to be explicitly normalised. *) type who = Left | Right diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 710a2394d..aac9a7d31 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -539,7 +539,7 @@ let context operation path (t : constr) = in loop 1 path t -let occurence path (t : constr) = +let occurrence path (t : constr) = let rec loop p0 t = match (p0,kind_of_term t) with | (p, Cast (c,_,_)) -> loop p c | ([], _) -> t @@ -555,7 +555,7 @@ let occurence path (t : constr) = | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term | (p, _) -> - failwith ("occurence " ^ string_of_int(List.length p)) + failwith ("occurrence " ^ string_of_int(List.length p)) in loop path t @@ -660,7 +660,7 @@ let clever_rewrite_gen_nat p result (t,args) = let clever_rewrite p vpath t gl = let full = pf_concl gl in let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in - let vargs = List.map (fun p -> occurence p occ) vpath in + let vargs = List.map (fun p -> occurrence p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in exact (applist(t',[mkNewMeta()])) gl diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 8156e8411..95407c5ff 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -44,7 +44,7 @@ let occ_step_eq s1 s2 = match s1, s2 with (* chemin identifiant une proposition sous forme du nom de l'hypothèse et d'une liste de pas à partir de la racine de l'hypothèse *) -type occurence = {o_hyp : Names.Id.t; o_path : occ_path} +type occurrence = {o_hyp : Names.Id.t; o_path : occ_path} (* \subsection{refiable formulas} *) type oformula = @@ -81,7 +81,7 @@ and oequation = { e_left: oformula; (* formule brute gauche *) e_right: oformula; (* formule brute droite *) e_trace: Term.constr; (* tactique de normalisation *) - e_origin: occurence; (* l'hypothèse dont vient le terme *) + e_origin: occurrence; (* l'hypothèse dont vient le terme *) e_negated: bool; (* vrai si apparait en position nié après normalisation *) e_depends: direction list; (* liste des points de disjonction dont @@ -111,7 +111,7 @@ type environment = { real_indices : (int,int) Hashtbl.t; mutable cnt_connectors : int; equations : (int,oequation) Hashtbl.t; - constructors : (int, occurence) Hashtbl.t + constructors : (int, occurrence) Hashtbl.t } (* \subsection{Solution tree} @@ -136,7 +136,7 @@ type solution_tree = chemins pour extraire des equations ou d'hypothèses *) type context_content = - CCHyp of occurence + CCHyp of occurrence | CCEqua of int (* \section{Specific utility functions to handle base types} *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 19c85c9e2..121ab7488 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -415,8 +415,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = try_aux sub mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function - | [] -> assert false - | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + | _ -> assert false in let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 754ad8f58..bbc4f1db2 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1484,7 +1484,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = if occur_meta body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) - if occur_evar evk body then raise (OccurCheckIn (evd',body)); + if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in (* Cannot strictly type instantiations since the unification algorithm diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 5ae989b78..1c3ae9ad9 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -520,7 +520,7 @@ let rec check_and_clear_in_constr env evdref err ids c = let clear_hyps_in_evi_main env evdref hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in - the contexts of the evars occuring in evi *) + the contexts of the evars occurring in evi *) let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in let nhyps = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8a5db9059..48911a5a9 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1011,8 +1011,8 @@ let contextually byhead occs f env sigma t = snd (e_contextually byhead occs f' env sigma t) (* linear bindings (following pretty-printer) of the value of name in c. - * n is the number of the next occurence of name. - * ol is the occurence list to find. *) + * n is the number of the next occurrence of name. + * ol is the occurrence list to find. *) let match_constr_evaluable_ref sigma c evref = match kind_of_term c, evref with @@ -1061,7 +1061,7 @@ let is_projection env = function (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. - * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. + * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences. * Performs a betaiota reduction after unfolding. *) let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 96c80f263..5c6ed3396 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -316,7 +316,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = if poly || now then let make_body t (c, eff) = let open Universes in - let body = c and typ = nf t in + let body = c in + let typ = + if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then + nf t + else t + in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 33db349c8..d26af04ba 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -447,7 +447,7 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - check_evars_are_solved env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); let ids = List.map pi1 ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/tactics/auto.ml b/tactics/auto.ml index e5fdf6a7c..617c491c3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -72,27 +72,42 @@ let auto_flags_of_state st = (* Try unification with the precompiled clause, then use registered Apply *) -let unify_resolve_nodelta poly (c,clenv) = +let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.nf_enter begin fun gl -> - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in - let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags:auto_unif_flags clenv' gl) gl in - Clenvtac.clenv_refine false 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 = Proofview.Goal.sigma 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 *) + let (_, _, ctx) = c in + let clenv = + if poly then + (** Refresh the instance of the hint *) + let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let map c = Vars.subst_univs_level_constr subst c in + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in + (** FIXME: We're being inefficient here because we substitute the whole + evar map instead of just its metas, which are the only ones + mentioning the old universes. *) + Clenv.map_clenv map clenv + else + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + { clenv with evd = evd ; env = Proofview.Goal.env gl } + in + let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in + Clenvtac.clenv_refine false clenv end -let unify_resolve poly flags (c,clenv) = - Proofview.Goal.nf_enter begin fun gl -> - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in - let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv' gl) gl in - Clenvtac.clenv_refine false clenv'' - end +let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h let unify_resolve_gen poly = function | None -> unify_resolve_nodelta poly | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = + let (c, _, _) = c in let ctx, c' = if poly then let evd', subst = Evd.refresh_undefined_universes clenv.evd in diff --git a/tactics/auto.mli b/tactics/auto.mli index 8dacc1362..6e2acf7f5 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -26,9 +26,9 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> unit Proofview.tactic +val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic -val unify_resolve : polymorphic -> Unification.unify_flags -> (constr * clausenv) -> unit Proofview.tactic +val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ca0a74fee..c30957a67 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -154,6 +154,7 @@ let progress_evars t = let e_give_exact flags poly (c,clenv) gl = + let (c, _, _) = c in let c, gl = if poly then let clenv', subst = Clenv.refresh_undefined_univs clenv in @@ -179,6 +180,7 @@ let unify_resolve poly flags (c,clenv) gls = (Clenvtac.clenv_refine false ~with_classes:false clenv') gls let clenv_of_prods poly nprods (c, clenv) gls = + let (c, _, _) = c in if poly || Int.equal nprods 0 then Some clenv else let ty = pf_unsafe_type_of gls c in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index f39d71462..1a84161e4 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -126,6 +126,7 @@ open Unification let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) let unify_e_resolve poly flags (c,clenv) gls = + let (c, _, _) = c in let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv else clenv, Univ.empty_level_subst in let clenv' = connect_clenv gls clenv' in @@ -142,6 +143,7 @@ let hintmap_of hdc concl = (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) let e_exact poly flags (c,clenv) = + let (c, _, _) = c in let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv else clenv, Univ.empty_level_subst diff --git a/tactics/equality.ml b/tactics/equality.ml index 4c48003b9..a74d555dd 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -88,7 +88,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *) type orientation = bool type conditions = - | Naive (* Only try the first occurence of the lemma (default) *) + | Naive (* Only try the first occurrence of the lemma (default) *) | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) @@ -1577,7 +1577,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *) exception FoundHyp of (Id.t * constr * bool) -(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *) +(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *) let is_eq_x gl x (id,_,c) = try let c = pf_nf_evar gl c in diff --git a/tactics/equality.mli b/tactics/equality.mli index 3e13ee570..840ede7d9 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -23,7 +23,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *) type orientation = bool type conditions = - | Naive (* Only try the first occurence of the lemma (default) *) + | Naive (* Only try the first occurrence of the lemma (default) *) | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 9faa96a80..96c7d79ca 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -97,7 +97,9 @@ type 'a with_uid = { uid : KerName.t; } -type hint = (constr * clausenv) hint_ast with_uid +type raw_hint = constr * types * Univ.universe_context_set + +type hint = (raw_hint * clausenv) hint_ast with_uid type 'a with_metadata = { pri : int; (* A number lower is higher priority *) @@ -110,7 +112,7 @@ type 'a with_metadata = { type full_hint = hint with_metadata type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata + raw_hint hint_ast with_uid with_metadata type import_level = [ `LAX | `WARN | `STRICT ] @@ -267,7 +269,7 @@ let strip_params env c = | _ -> c let instantiate_hint env sigma p = - let mk_clenv c cty ctx = + let mk_clenv (c, cty, ctx) = let sigma = Evd.merge_context_set univ_flexible sigma ctx in let cl = mk_clenv_from_env env sigma None (c,cty) in {cl with templval = @@ -275,11 +277,11 @@ let instantiate_hint env sigma p = env = empty_env} in let code = match p.code.obj with - | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx) - | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx) - | Res_pf_THEN_trivial_fail (c, cty, ctx) -> - Res_pf_THEN_trivial_fail (c, mk_clenv c cty ctx) - | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx) + | Res_pf c -> Res_pf (c, mk_clenv c) + | ERes_pf c -> ERes_pf (c, mk_clenv c) + | Res_pf_THEN_trivial_fail c -> + Res_pf_THEN_trivial_fail (c, mk_clenv c) + | Give_exact c -> Give_exact (c, mk_clenv c) | Unfold_nth e -> Unfold_nth e | Extern t -> Extern t in @@ -1205,12 +1207,14 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) +let pr_hint_elt (c, _, _) = pr_constr c + let pr_hint h = match h.obj with - | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c) - | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c) - | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c) - | Res_pf_THEN_trivial_fail (c,clenv) -> - (str"apply " ++ pr_constr c ++ str" ; trivial") + | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c) + | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c) + | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c) + | Res_pf_THEN_trivial_fail (c, _) -> + (str"apply " ++ pr_hint_elt c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> let env = diff --git a/tactics/hints.mli b/tactics/hints.mli index e25b66b27..af4d3d1f6 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -37,6 +37,7 @@ type 'a hint_ast = | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) type hint +type raw_hint = constr * types * Univ.universe_context_set type hints_path_atom = | PathHints of global_reference list @@ -199,11 +200,11 @@ val make_extern : -> hint_entry val run_hint : hint -> - ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic + ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic (** This function is for backward compatibility only, not to use in newly written code. *) -val repr_hint : hint -> (constr * clausenv) hint_ast +val repr_hint : hint -> (raw_hint * clausenv) hint_ast val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t diff --git a/tactics/leminv.ml b/tactics/leminv.ml index efd6ded44..42d22bc3c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -124,7 +124,7 @@ let rec add_prods_sign env sigma t = add_prods_sign (push_named (id,Some c1,t1) env) sigma b' | _ -> (env,t) -(* [dep_option] indicates wether the inversion lemma is dependent or not. +(* [dep_option] indicates whether the inversion lemma is dependent or not. If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H) where P:(x_bar:T_bar)(H:(I x_bar))[sort]. diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 6bd65d0a2..081170869 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1386,7 +1386,7 @@ module Strategies = end -(** The strategy for a single rewrite, dealing with occurences. *) +(** The strategy for a single rewrite, dealing with occurrences. *) (** A dummy initial clauseenv to avoid generating initial evars before even finding a first application of the rewriting lemma, in setoid_rewrite diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index db3b19af5..aaa7b3a51 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -1,6 +1,6 @@ (* Wish #2154 by E. van der Weegen *) -(* auto was not using f_equal-style lemmas with metavariables occuring +(* auto was not using f_equal-style lemmas with metavariables occurring only in the type of an evar of the concl, but not directly in the concl itself *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 2437184a9..45306caf0 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -69,7 +69,7 @@ Section Facts. Variable A : Type. - (** *** Genereric facts *) + (** *** Generic facts *) (** Discrimination *) Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. @@ -622,9 +622,9 @@ Section Elts. Qed. - (****************************************) - (** ** Counting occurences of a element *) - (****************************************) + (******************************************) + (** ** Counting occurrences of an element *) + (******************************************) Fixpoint count_occ (l : list A) (x : A) : nat := match l with diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 4e28b5b90..f5e936cf0 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -19,7 +19,7 @@ Require Export DoubleType. arithmetic. In fact it is more general than that. The only reason for this use of 31 is the underlying mecanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, - 63-bit integers is now just a matter of replacing every occurences + 63-bit integers is now just a matter of replacing every occurrences of 31 by 63. This is actually made possible by the use of dependently-typed n-ary constructions for the inductive type [int31], its constructor [I31] and any pattern matching on it. diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 6fdf0a2a5..376620ddc 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -15,7 +15,7 @@ Require Import List. (** * Generic dependently-typed operators about [n]-ary functions *) (** The type of [n]-ary function: [nfun A n B] is - [A -> ... -> A -> B] with [n] occurences of [A] in this type. *) + [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *) Fixpoint nfun A n B := match n with diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 66f1ecd78..4852a6d33 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -233,13 +233,6 @@ let compile_files () = compile_file vf) (List.rev l) -(*s options for the virtual machine *) - -let use_vm = ref false - -let set_vm_opt () = - Vconv.set_use_vm !use_vm - (** Options for proof general *) let set_emacs () = @@ -547,7 +540,6 @@ let parse_args arglist = |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) |"-verbose-compat-notations" -> verb_compat_ntn := true - |"-vm" -> use_vm := true |"-where" -> print_where := true (* Deprecated options *) @@ -607,7 +599,6 @@ let init arglist = if_verbose print_header (); inputstate (); Mltop.init_known_plugins (); - set_vm_opt (); engage (); (* Be careful to set these variables after the inputstate *) Syntax_def.set_verbose_compat_notations !verb_compat_ntn; diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 7a3bcfba8..8efc36df7 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -783,7 +783,7 @@ let explain_pretype_error env sigma err = let {uj_val = c; uj_type = actty} = j in let (env, c, actty, expty), e = contract3' env c actty t e in let j = {uj_val = c; uj_type = actty} in - explain_actual_type env sigma j t (Some e) + explain_actual_type env sigma j expty (Some e) | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp | VarNotFound id -> explain_var_not_found env id diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8efe3614e..fc0e5beaa 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1347,19 +1347,10 @@ let _ = optwrite = Flags.make_universe_polymorphism } let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of virtual machine inside the kernel"; - optkey = ["Virtual";"Machine"]; - optread = (fun () -> Vconv.use_vm ()); - optwrite = (fun b -> Vconv.set_use_vm b) } - -let _ = declare_int_option { optsync = true; optdepr = false; - optname = "the level of inling duging functor application"; + optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> |