From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- CHANGES | 2 +- INSTALL.ide | 2 +- dev/doc/univpoly.txt | 2 +- dev/v8-syntax/memo-v8.tex | 2 +- doc/faq/FAQ.tex | 16 ++++++++-------- doc/refman/Universes.tex | 6 +++--- doc/tools/Translator.tex | 2 +- ide/coq.mli | 6 +++--- ide/coqide.ml | 4 ++-- ide/utf8_convert.mll | 2 +- ide/wg_ScriptView.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- kernel/nativecode.ml | 4 ++-- kernel/nativelambda.ml | 32 ++++++++++++++++---------------- lib/xml_parser.mli | 12 ++++++------ library/impargs.ml | 2 +- library/impargs.mli | 4 ++-- parsing/lexer.ml4 | 2 +- plugins/btauto/Algebra.v | 2 +- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/extraction/CHANGES | 6 +++--- plugins/extraction/mlutil.ml | 14 +++++++------- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_termops.mli | 4 ++-- plugins/funind/merge.ml | 2 +- plugins/micromega/mfourier.ml | 2 +- plugins/omega/coq_omega.ml | 6 +++--- plugins/romega/refl_omega.ml | 8 ++++---- pretyping/evarutil.ml | 2 +- pretyping/tacred.ml | 6 +++--- pretyping/termops.ml | 2 +- tactics/equality.ml | 4 ++-- tactics/equality.mli | 2 +- tactics/leminv.ml | 2 +- tactics/rewrite.ml | 2 +- test-suite/success/auto.v | 2 +- theories/Lists/List.v | 6 +++--- theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- toplevel/vernacentries.ml | 2 +- 40 files changed, 93 insertions(+), 93 deletions(-) diff --git a/CHANGES b/CHANGES index cf2bb49271..07d129a462 100644 --- a/CHANGES +++ b/CHANGES @@ -2180,7 +2180,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 13e741e340..6e41b2d051 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//.config/coq/coqiderc under Linux, or C:\Documents and Settings\\.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 9e243eead5..6a69c57934 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 8d116de26f..ae4b569b36 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 fbb866e875..2eebac39ac 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. @@ -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} @@ -1632,7 +1632,7 @@ 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/.config/coq/coqiderc| under Linux, or \\ \verb|C:\Documents and Settings\\.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 018d73908b..a03d5c7b20 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 instantantiate 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. @@ -202,7 +202,7 @@ 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. -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}). diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index 5f7b6dc951..ed1d336d9e 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/ide/coq.mli b/ide/coq.mli index a72c67b43e..2dc5ad3078 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 c0e2281258..f15e5fa34a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1125,10 +1125,10 @@ let build_ui () = ~accel:(prefs.modifier_for_navigation^"h");*) item "Previous" ~label:"_Previous" ~stock:`GO_BACK ~callback:Nav.previous_occ - ~tooltip:"Previous occurence" + ~tooltip:"Previous occurrence" ~accel:(prefs.modifier_for_navigation^"less"); item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ - ~tooltip:"Next occurence" + ~tooltip:"Next occurrence" ~accel:(prefs.modifier_for_navigation^"greater"); item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document ~tooltip:"Fully check the document" diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 621833ddea..4ebf9a62e1 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 8298d9954f..ae50b28377 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -139,7 +139,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 a3721af660..eee9289892 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/nativecode.ml b/kernel/nativecode.ml index 687b740f67..98b2d6d2e9 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 cb08b5058f..263befd213 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/lib/xml_parser.mli b/lib/xml_parser.mli index cefb4af897..87ef787770 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 + {!Xml.error_msg} tells you which error occurred 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 + location where the error occurred at.} + {li {!Xml.File_not_found} is raised when and 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 diff --git a/library/impargs.ml b/library/impargs.ml index 94f53219e7..d15a02fea2 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 1d3a73e94c..30f2e30f97 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 8e83929619..c6d5f3b925 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/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index bc5a390027..ee7341a4a2 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 714cd86341..1a90806476 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 fbcd01a15e..cf97ae3ab8 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 9fdb0205f5..6fc1195fba 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/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index bc7e6f8b09..e7732a5037 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 0f10636f0f..179e8fe8d9 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 69e055c23b..60c58730a3 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 88c1a78366..a36369d220 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 710a2394d3..aac9a7d315 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 8156e84114..95407c5ff1 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/evarutil.ml b/pretyping/evarutil.ml index 8ebb037c24..d3d6901b66 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -525,7 +525,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 8a5db90590..48911a5a9f 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/pretyping/termops.ml b/pretyping/termops.ml index 937471cf76..5a55d47fd1 100644 --- a/pretyping/termops.ml +++ b/pretyping/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/tactics/equality.ml b/tactics/equality.ml index c442178c10..5ed9ac2ba0 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 3e13ee570c..840ede7d9f 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/leminv.ml b/tactics/leminv.ml index efd6ded44c..42d22bc3c4 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 6bd65d0a21..0811708695 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 db3b19af51..aaa7b3a514 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 e0e5d94d82..0ace6938b9 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -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 4e28b5b905..f5e936cf01 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 6fdf0a2a5b..376620ddcd 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/vernacentries.ml b/toplevel/vernacentries.ml index 35730eea03..48100aa7fd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1359,7 +1359,7 @@ 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 -> -- cgit v1.2.3 From f617aeef08441e83b13f839ce767b840fddbcf7d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 14 Oct 2015 10:39:55 +0200 Subject: Fix some typos. --- doc/faq/FAQ.tex | 4 ++-- doc/refman/Universes.tex | 6 +++--- kernel/byterun/coq_interp.c | 2 +- lib/xml_parser.mli | 6 +++--- parsing/pcoq.ml4 | 6 +++--- theories/Lists/List.v | 2 +- 6 files changed, 13 insertions(+), 13 deletions(-) diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 2eebac39ac..48b61827d1 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -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 @@ -1625,7 +1625,7 @@ 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. diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index a03d5c7b20..cd8222269d 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -183,7 +183,7 @@ bound if it is an atomic universe (i.e. not an algebraic max()). \end{flushleft} The syntax has been extended to allow users to explicitly bind names to -universes and explicitly instantantiate polymorphic +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,7 +200,7 @@ 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 explicitly, giving their full instance: \begin{coq_example} @@ -209,7 +209,7 @@ 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/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 399fa843f1..1653c3b012 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1271,7 +1271,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/lib/xml_parser.mli b/lib/xml_parser.mli index 87ef787770..ac2eab352f 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -37,9 +37,9 @@ 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 occurred during parsing - and the {!Xml.error_pos} can be used to retreive the document + 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 and error occurred while + {li {!Xml.File_not_found} is raised when an error occurred while opening a file with the {!Xml.parse_file} function.} } *) @@ -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/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 797b031fe4..2e47e07a36 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/theories/Lists/List.v b/theories/Lists/List.v index 0ace6938b9..fe18686e21 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. -- cgit v1.2.3 From 4a1234459472c5fbb0d0467217972f247c054832 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 14 Oct 2015 10:44:44 +0200 Subject: Remove some unused variables. --- kernel/byterun/coq_interp.c | 2 -- kernel/byterun/coq_memory.c | 2 -- kernel/byterun/coq_values.c | 1 - 3 files changed, 5 deletions(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1653c3b012..33253ed93c 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++; @@ -1110,7 +1109,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 ) */ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 416e5e5329..c9bcdc32ff 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 007f61b27c..528babebfc 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); -- cgit v1.2.3 From bc1c530550e7d06655d541c21859321a2f84c260 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 14 Oct 2015 11:33:01 +0200 Subject: Make interpreter of PROJ simpler by not using the stack. --- kernel/byterun/coq_interp.c | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 33253ed93c..0553a5ed7e 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -883,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++); } -- cgit v1.2.3 From d024277d485e3b6a70c217be965063a66aeffefe Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Oct 2015 11:24:32 +0200 Subject: Fixing bug #4367: Wrong error message in unification. --- toplevel/himsg.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 7a3bcfba80..8efc36df72 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 -- cgit v1.2.3 From 043d67c93111328fdbc2d7afa1a84daf3d68a5cc Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 14 Oct 2015 13:41:00 +0200 Subject: Remove unused infos structure in VM. Became unused after c47b205206d832430fa80a3386be80149e281d33. --- kernel/vconv.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8af2efc588..2cbc102021 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 -> -- cgit v1.2.3 From f45a88ad054b88792ec8cc6631e4d4015fa95bab Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 14 Oct 2015 13:45:06 +0200 Subject: Remove -vm flag of coqtop. Used to replace the standard conversion by the VM. Not so useful, and implemented using a bunch of references inside and outside the kernel. --- kernel/vconv.ml | 11 ----------- kernel/vconv.mli | 2 -- toplevel/coqtop.ml | 9 --------- toplevel/vernacentries.ml | 9 --------- 4 files changed, 31 deletions(-) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2cbc102021..27e184ea3f 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -227,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 096d31ac81..1a29a4d518 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/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8925bbe299..72966a4add 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/vernacentries.ml b/toplevel/vernacentries.ml index 48100aa7fd..f1f87ca9b1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1346,15 +1346,6 @@ let _ = optread = Flags.is_universe_polymorphism; 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; -- cgit v1.2.3 From 0f74b3df6e64dc069e53c4afcd6f46129b211d09 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 14 Oct 2015 13:50:55 +0200 Subject: Remove reference to default conversion function inside the kernel. --- kernel/reduction.ml | 7 +------ kernel/reduction.mli | 1 - 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b09367dd92..68783780d3 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -738,14 +738,9 @@ let vm_conv cv_pb env t1 t2 = (* If compilation fails, fall-back to closure 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 l2r (fun _ -> None) env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) fconv cv_pb false (fun _->None) env t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6ced5c4985..90c008b19d 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 -- cgit v1.2.3 From 4b8155591be6e20505ee25f7199edcf44a638c7e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Oct 2015 14:38:22 +0200 Subject: Fixing evarmap implementation. --- pretyping/evd.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 3d912ca4ce..1107c2951e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -750,7 +750,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 *) -- cgit v1.2.3 From 36f669f769fa23eb897adfa0450875a3c0db3476 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Oct 2015 12:01:38 +0200 Subject: Exporting the original unprocessed hint in the hint running function. --- plugins/firstorder/sequent.ml | 1 + tactics/auto.ml | 1 + tactics/auto.mli | 4 ++-- tactics/class_tactics.ml | 2 ++ tactics/eauto.ml4 | 2 ++ tactics/hints.ml | 30 +++++++++++++++++------------- tactics/hints.mli | 5 +++-- 7 files changed, 28 insertions(+), 17 deletions(-) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 96c4eb01eb..a77af03dc1 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/tactics/auto.ml b/tactics/auto.ml index e5fdf6a7c2..72c28ce323 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -93,6 +93,7 @@ let unify_resolve_gen poly = function | 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 8dacc13629..6e2acf7f56 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 ed5b783f6c..36b60385d8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -141,6 +141,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 @@ -166,6 +167,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 b6b18719c0..09c5fa873f 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -118,6 +118,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 @@ -134,6 +135,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/hints.ml b/tactics/hints.ml index 9faa96a806..96c7d79ca5 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 e25b66b27b..af4d3d1f66 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 -- cgit v1.2.3 From db80daaf82a08a1475c65f7c82bffb63c7efd27a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 14 Oct 2015 16:40:53 +0200 Subject: Temporary fix: kernel conversion needs to ignore l2r flag. Stdlib does not compile when l2r flag is actually taken into account. We should investigate... --- kernel/reduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 68783780d3..ccea06c761 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -740,7 +740,7 @@ let vm_conv cv_pb env t1 t2 = let default_conv cv_pb ?(l2r=false) env t1 t2 = try - fconv cv_pb l2r (fun _ -> None) env t1 t2 + fconv cv_pb false (fun _ -> None) env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) fconv cv_pb false (fun _->None) env t1 t2 -- cgit v1.2.3 From 5b67ba8e1bbd92d4ef7e2adab13bd05e7b55bfd7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 15:57:19 +0200 Subject: Univs: inductives, remove unneeded test --- kernel/indtypes.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9c065101a3..5d7a0bbf00 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -285,11 +285,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 || (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 || (check_leq (universes env') infu defu) in let _ = (** Impredicative sort, always allow *) -- cgit v1.2.3 From 5009be2f117a5ef27733b7d6895503af91e9aa34 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 15:57:42 +0200 Subject: When typechecking a lemma statement, try to resolve typeclasses before failing for unresolved evars (regression). --- stm/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5cbe152b55..c49ddfd8ec 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -439,7 +439,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), -- cgit v1.2.3 From b8c681338cad546c397a1803c55183cc6526adfb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 16:39:09 +0200 Subject: Fix constr_matching when a match is found in the head of a case construct --- pretyping/constr_matching.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 19c85c9e27..121ab74885 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 -- cgit v1.2.3 From 26af31cb46c7baf92325dd22bf6ee33aaa2172d2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 18:17:42 +0200 Subject: Occur-check in evar_define was not strong enough. --- pretyping/evarsolve.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 754ad8f588..bbc4f1db29 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 -- cgit v1.2.3 From bf0499bc507d5a39c3d5e3bf1f69191339270729 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 18:18:01 +0200 Subject: Fix LemmaOverloading Do not normalize the type of a proof according to the final universes when keep_body_ucst_separate is true, otherwise the type might not be retypable in the initial context... --- proofs/proof_global.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3e06294e64..a0ead42ef3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -313,7 +313,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 -- cgit v1.2.3 From a895b2c0caf8ec9c0deb04b8dea890283bd7329d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Oct 2015 12:16:36 +0200 Subject: Fixing perfomance issue of auto hints induced by universes. Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand. --- dev/top_printers.ml | 2 +- tactics/auto.ml | 38 ++++++++++++++++++++++++++------------ 2 files changed, 27 insertions(+), 13 deletions(-) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f9f2e1b09e..059c812ad5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) +let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd)) let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) diff --git a/tactics/auto.ml b/tactics/auto.ml index 72c28ce323..617c491c35 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -72,21 +72,35 @@ 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 -- cgit v1.2.3 From 1d6c4f135d42a008b21d86d8ecd8b329405d8d7c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Oct 2015 18:51:47 +0200 Subject: Reverting modifications in dev/top_printers pushed mistakenly. --- dev/top_printers.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 059c812ad5..f9f2e1b09e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd)) +let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) -- cgit v1.2.3 From 7402a7788b6a73bd5c0cb9078823d48e6f01a357 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 15 Oct 2015 08:10:05 +0200 Subject: Fix detection of ties in oracle_order. This commit has no impact, since l2r is always false in practice due to the definition of default_conv. --- kernel/conv_oracle.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 3b01538b92..ec2c334b6f 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) -- cgit v1.2.3