diff options
83 files changed, 738 insertions, 427 deletions
diff --git a/checker/check.ml b/checker/check.ml index 31bfebc3d5..6d307b3c5e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -263,6 +263,7 @@ let raw_intern_library f = type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } module Dyn = Dyn.Make () @@ -345,6 +346,7 @@ let intern_from_file ~intern_mode (dir, f) = let () = close_in ch in let ch = open_in_bin f in let () = close_in ch in + let () = System.check_caml_version ~caml:sd.md_ocaml ~file:f in if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); diff --git a/checker/values.ml b/checker/values.ml index 76e3ab0d45..cce0ce7203 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -435,7 +435,7 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) let v_libsum = - Tuple ("summary", [|v_dp;v_deps|]) + Tuple ("summary", [|v_dp;v_deps;String|]) let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh new file mode 100644 index 0000000000..50eaf0b109 --- /dev/null +++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then + + elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst new file mode 100644 index 0000000000..e1fcfb78c4 --- /dev/null +++ b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst @@ -0,0 +1,4 @@ +- **Added:** + Abbreviations support arguments occurring both in term and binder position + (`#8808 <https://github.com/coq/coq/pull/8808>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst new file mode 100644 index 0000000000..055006d3b4 --- /dev/null +++ b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is + indirectly dependent in the goal; the incompatibility can generally + be fixed by first clearing the hypotheses causing an indirect + dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` + instead; similarly, :tacn:`subst` has no more effect on such variables + (`#12146 <https://github.com/coq/coq/pull/12146>`_, + by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; + fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). diff --git a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst new file mode 100644 index 0000000000..dc438f151e --- /dev/null +++ b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Loss of location of some tactic errors + (`#12223 <https://github.com/coq/coq/pull/12223>`_, + by Hugo Herbelin; fixes + `#12152 <https://github.com/coq/coq/pull/12152>`_ and + `#12255 <https://github.com/coq/coq/pull/12255>`_). diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst new file mode 100644 index 0000000000..0dd0fed4e2 --- /dev/null +++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 <https://github.com/coq/coq/pull/11503>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst new file mode 100644 index 0000000000..5ab2941446 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst @@ -0,0 +1,9 @@ +- **Deprecated:** + Option :flag:`Hide Obligations` has been deprecated + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). + +- **Removed:** + Deprecated option ``Shrink Obligations`` has been removed + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst index 7c10d261a7..42e5eb96eb 100644 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -1,5 +1,5 @@ - **Added:** - Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` (`#12008 <https://github.com/coq/coq/pull/12008>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst new file mode 100644 index 0000000000..6a4070a82e --- /dev/null +++ b/doc/changelog/10-standard-library/12162-bool-leb.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 52862dea47..b5618c5721 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -342,17 +342,11 @@ optional tactic is replaced by the default one if not specified. .. flag:: Hide Obligations + .. deprecated:: 8.12 + Controls whether obligations appearing in the term should be hidden as implicit arguments of the special - constantProgram.Tactics.obligation. - -.. flag:: Shrink Obligations - - .. deprecated:: 8.7 - - This flag (on by default) controls whether obligations should have - their context minimized to the set of variables used in the proof of - the obligation, to avoid unnecessary dependencies. + constant ``Program.Tactics.obligation``. The module :g:`Coq.Program.Tactics` defines the default tactic for solving obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index acdd4408ed..899173a83a 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -9,11 +9,11 @@ The |Coq| library The |Coq| library has two parts: - * **The basic library**: definitions and theorems for + * The :gdef:`prelude`: definitions and theorems for the most commonly used elementary logical notions and data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries with + * The :gdef:`standard library`: general-purpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the ``Require`` command (see :ref:`compiled-files`) @@ -28,8 +28,8 @@ also be browsed at http://coq.inria.fr/stdlib/. -The basic library ------------------ +The prelude +----------- This section lists the basic notions and results which are directly available in the standard |Coq| system. Most of these constructions diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9473cc5a15..aa93b4d21f 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -130,30 +130,37 @@ Strings identified with :production:`string`. Keywords - The following character sequences are reserved keywords that cannot be - used as identifiers:: + The following character sequences are keywords defined in the main Coq grammar + that cannot be used as identifiers (even when starting Coq with the `-noinit` + command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop - SProp Set Theorem Type Variable as at cofix discriminated else end + SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with - Note that notations and plugins may define additional keywords. + The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: -Other tokens - The set of - tokens defined at any given time can vary because the :cmd:`Notation` - command can define new tokens. A :cmd:`Require` command may load more notation definitions, - while the end of a :cmd:`Section` may remove notations. Some notations - are defined in the standard library (see :ref:`thecoqlibrary`) and are generally - loaded automatically at startup time. + IF by exists exists2 using + + Note that loading additional modules or plugins may expand the set of reserved + keywords. - Here are the character sequences that |Coq| directly defines as tokens - without using :cmd:`Notation`:: +Other tokens + The following character sequences are tokens defined in the main Coq grammar + (even when starting Coq with the `-noinit` command-line flag):: - ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: - <<: <= = => > >-> >= ? @ @{ [ [= ] _ - `( `{ { {| | |- || } + <<: <= = => > >-> >= ? @ @{ [ ] _ + `( `{ { {| | } + + The following character sequences are tokens defined in notations or plugins + loaded in the :term:`prelude`:: + + ** [= |- || -> + + Note that loading additional modules or plugins may expand the set of defined + tokens. When multiple tokens match the beginning of a sequence of characters, the longest matching token is used. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ca167c8b4b..d4ceffac9f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -202,14 +202,8 @@ and ``coqtop``, unless stated otherwise: See the :ref:`note above <interleave-command-line>` regarding the order of command-line options. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. -:-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option - implies -batch (exit just after argument parsing). It is available only - for `coqtop`, as this behavior is the purpose of ``coqc``. -:-compile-verbose *file.v*: Deprecated. Use ``coqc -verbose``. Same as -compile but also output the - content of *file.v* as it is compiled. :-verbose: Output the content of the input file as it is compiled. - This option is available for ``coqc`` only; it is the counterpart of - -compile-verbose. + This option is available for ``coqc`` only. :-vos: Indicate |Coq| to skip the processing of opaque proofs (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b184311bef..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,6 +57,8 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: + - The grammar reserves the token ``||``. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. .. example:: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..1e35160205 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,25 +213,63 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. + + .. example:: Dynamic nature of mutable cells + + .. coqtop:: all + + Ltac2 mutable x := true. + Ltac2 y := x. + Ltac2 Eval y. + Ltac2 Set x := false. + Ltac2 Eval y. + + .. example:: Interaction with recursive calls + + + .. coqtop:: all + + Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. + Ltac2 Set f := fun b => + match b with true => 1 | _ => f true end. + Ltac2 Eval (f false). + Ltac2 Set f as oldf := fun b => + match b with true => 2 | _ => oldf false end. + Ltac2 Eval (f false). + + In the definition, the `f` in the body is resolved statically + because the definition is marked recursive. In the first re-definition, + the `f` in the body is resolved dynamically. This is witnessed by + the second re-definition. + Reduction ~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index bc2168411b..127e4c6dbe 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -36,6 +36,18 @@ language will be described in Chapter :ref:`ltac`. Common elements of tactics -------------------------- +Reserved keywords +~~~~~~~~~~~~~~~~~ + +The tactics described in this chapter reserve the following keywords:: + + by using + +Thus, these keywords cannot be used as identifiers. It also declares +the following character sequences as tokens:: + + ** [= |- + .. _invocation-of-tactics: Invocation of tactics @@ -2832,6 +2844,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also unfolded and cleared. + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + .. note:: + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the first one is used. @@ -2845,9 +2862,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: subst - This applies subst repeatedly from top to bottom to all identifiers of the + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. .. flag:: Regular Subst Tactic @@ -2873,6 +2892,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. hypotheses, which without the flag it may break. default. + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + .. tacn:: stepl @term :name: stepl diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ea5ad79a80..c5ec636d5f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -618,6 +618,41 @@ the next command fails because p does not bind in the instance of n. Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). +Notations with expressions used both as binder and term ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +It is possible to use parameters of the notation both in term and +binding position. Here is an example: + +.. coqtop:: in + + Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. + Notation "▢_ n P" := (force n (fun n => P)) + (at level 0, n ident, P at level 9, format "▢_ n P"). + +.. coqtop:: all + + Check exists p, ▢_p (p >= 1). + +More generally, the parameter can be a pattern, as in the following +variant: + +.. coqtop:: in reset + + Definition force2 q (P:nat*nat -> Prop) := + (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + + Notation "▢_ p P" := (force2 p (fun p => P)) + (at level 0, p pattern at level 0, P at level 9, format "▢_ p P"). + +.. coqtop:: all + + Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2). + +This support is experimental. For instance, the notation is used for +printing only if the occurrence of the parameter in term position +comes in the right-hand side before the occurrence in binding position. + .. _RecursiveNotations: Notations with recursive patterns @@ -1383,6 +1418,17 @@ Abbreviations exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments. + Like for notations, it is possible to bind binders in + abbreviations. Here is an example: + + .. coqtop:: in reset + + Definition force2 q (P:nat*nat -> Prop) := + (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + + Notation F p P := (force2 p (fun p => P)). + Check exists x y, F (x,y) (x >= 1 /\ y >= 2). + .. _numeral-notations: Numeral notations diff --git a/engine/termops.ml b/engine/termops.ml index 6d779e6a35..c51e753d46 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -803,23 +803,29 @@ let occur_evar sigma n c = let occur_in_global env id constr = let vars = vars_of_global env constr in - if Id.Set.mem id vars then raise Occur + Id.Set.mem id vars let occur_var env sigma id c = let rec occur_rec c = match EConstr.destRef sigma c with - | gr, _ -> occur_in_global env id gr + | gr, _ -> if occur_in_global env id gr then raise Occur | exception DestKO -> EConstr.iter sigma occur_rec c in try occur_rec c; false with Occur -> true +exception OccurInGlobal of GlobRef.t + +let occur_var_indirectly env sigma id c = + let var = GlobRef.VarRef id in + let rec occur_rec c = + match EConstr.destRef sigma c with + | gr, _ -> if not (GlobRef.equal gr var) && occur_in_global env id gr then raise (OccurInGlobal gr) + | exception DestKO -> EConstr.iter sigma occur_rec c + in + try occur_rec c; None with OccurInGlobal gr -> Some gr + let occur_var_in_decl env sigma hyp decl = - let open NamedDecl in - match decl with - | LocalAssum (_,typ) -> occur_var env sigma hyp typ - | LocalDef (_, body, typ) -> - occur_var env sigma hyp typ || - occur_var env sigma hyp body + NamedDecl.exists (occur_var env sigma hyp) decl let local_occur_var sigma id c = let rec occur c = match EConstr.kind sigma c with @@ -828,6 +834,9 @@ let local_occur_var sigma id c = in try occur c; false with Occur -> true +let local_occur_var_in_decl sigma hyp decl = + NamedDecl.exists (local_occur_var sigma hyp) decl + (* returns the list of free debruijn indices in a term *) let free_rels sigma m = diff --git a/engine/termops.mli b/engine/termops.mli index 4e77aa9b3b..709fa361a9 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool +val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool +val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool val free_rels : Evd.evar_map -> constr -> Int.Set.t diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f82783f47d..9d0552817f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -976,10 +976,6 @@ let split_by_type_pat ?loc ids subst = assert (terms = [] && termlists = []); subst -let make_subst ids l = - let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in - List.fold_left2 fold Id.Map.empty ids l - let intern_notation intern env ntnvars loc ntn fullargs = (* Adjust to parsing of { } *) let ntn,fullargs = contract_curly_brackets ntn fullargs in @@ -1113,8 +1109,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in check_no_explicitation args1; - let terms = make_subst ids (List.map fst args1) in - let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in + let subst = split_by_type ids (List.map fst args1,[],[],[]) in let infos = (Id.Map.empty, env) in let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.loc in @@ -1624,8 +1619,8 @@ let drop_notations_pattern looked_for genv = let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; let pats1,pats2 = List.chop nvars pats in - let subst = make_subst vars pats1 in - let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in + let subst = split_by_type_pat vars (pats1,[]) in + let idspl1 = List.map (in_not false qid.loc scopes subst []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) | _ -> raise Not_found diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 7184f5ea29..bd3e234a91 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Pp open CErrors open Names @@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -type syndef_interpretation = (Id.t * subscopes) list * notation_constr - -(* Coercions to the general format of notation that also supports - variables bound to list of expressions *) -let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) -let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) - let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = let syndef = - { syndef_pattern = in_pat pat; + { syndef_pattern = pat; syndef_onlyparsing = onlyparsing; syndef_deprecation = deprecation; } @@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition = let search_syntactic_definition ?loc kn = let syndef = KNmap.find kn !syntax_table in - let def = out_pat syndef.syndef_pattern in Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; - def + syndef.syndef_pattern let search_filtered_syntactic_definition ?loc filter kn = let syndef = KNmap.find kn !syntax_table in - let def = out_pat syndef.syndef_pattern in - let res = filter def in + let res = filter syndef.syndef_pattern in if Option.has_some res then Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 8b323462a1..66a3132f2a 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,12 +13,10 @@ open Notation_term (** Syntactic definitions. *) -type syndef_interpretation = (Id.t * subscopes) list * notation_constr - val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> - onlyparsing:bool -> syndef_interpretation -> unit + onlyparsing:bool -> interpretation -> unit -val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation val search_filtered_syntactic_definition : ?loc:Loc.t -> - (syndef_interpretation -> 'a option) -> KerName.t -> 'a option + (interpretation -> 'a option) -> KerName.t -> 'a option diff --git a/lib/system.ml b/lib/system.ml index 4e98651d6e..e25f758865 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -168,6 +168,15 @@ let try_remove filename = let error_corrupted file s = CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") +let check_caml_version ~caml:s ~file:f = + if not (String.equal Coq_config.caml_version s) then + CErrors.user_err (str ("The file " ^ f ^ " was compiled with OCaml") ++ + spc () ++ str s ++ spc () ++ str "while this instance of Coq was compiled \ + with OCaml" ++ spc() ++ str Coq_config.caml_version ++ str "." ++ spc () ++ + str "Coq object files need to be compiled with the same OCaml toolchain to \ + be compatible.") + else () + let input_binary_int f ch = try input_binary_int ch with diff --git a/lib/system.mli b/lib/system.mli index 4a8c35b6ea..1e2f519327 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -88,6 +88,8 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val marshal_out : out_channel -> 'a -> unit val marshal_in : string -> in_channel -> 'a +val check_caml_version : caml:string -> file:string -> unit + (** {6 Time stamps.} *) type time diff --git a/man/coq-tex.1 b/man/coq-tex.1 index 7e0a2f81e2..e4cea24c55 100644 --- a/man/coq-tex.1 +++ b/man/coq-tex.1 @@ -1,4 +1,4 @@ -.TH COQ-TEX 1 "29 March 1995" +.TH COQ-TEX 1 .SH NAME coq-tex \- Process Coq phrases embedded in LaTeX files @@ -66,7 +66,7 @@ with `.v.tex' appended. The files produced by .B coq-tex -can be directly processed by LaTeX. +can be directly processed by LaTeX. Both the Coq phrases and the toplevel output are typeset in typewriter font. @@ -86,7 +86,7 @@ folding is performed on the Coq input text. Cause the file .IR coq-image to be executed to evaluate the Coq phrases. By default, -this is the command +this is the command .IR coqtop without specifying any path which is used to evaluate the Coq phrases. .TP diff --git a/man/coq_makefile.1 b/man/coq_makefile.1 index b5de6d367d..0f5912a4bb 100644 --- a/man/coq_makefile.1 +++ b/man/coq_makefile.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coq_makefile \- The Coq Proof Assistant makefile generator diff --git a/man/coqc.1 b/man/coqc.1 index 1e597afd99..a7be343fa0 100644 --- a/man/coqc.1 +++ b/man/coqc.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coqc \- The Coq Proof Assistant compiler @@ -19,14 +19,14 @@ is the batch compiler for the Coq Proof Assistant. The options are basically the same as coqtop(1). .IR file.v \& is the vernacular file to compile. -.IR file \& +.IR file \& must be formed only with the characters `a` to `Z`, `0`-`9` or `_` and must begin with a letter. The compiler produces an object file .IR file.vo \&. -For interactive use of Coq, see +For interactive use of Coq, see .BR coqtop(1). @@ -35,7 +35,7 @@ For interactive use of Coq, see .B coqc is a script that simply runs .B coqtop -with option +with option .B \-compile it accepts the same options as .B coqtop. diff --git a/man/coqchk.1 b/man/coqchk.1 index f9241c0d47..2f9e1fd84d 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "July 7, 201" +.TH COQ 1 .SH NAME coqchk \- The Coq Proof Checker compiled libraries verifier @@ -29,7 +29,7 @@ short or qualified logical name, or by their filename. .TP .BI \-I \ dir, \ \-\-include \ dir -add directory +add directory .I dir in the include path diff --git a/man/coqdep.1 b/man/coqdep.1 index 0770ce88c8..b0d9606969 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "28 March 1995" "Coq tools" +.TH COQ 1 .SH NAME coqdep \- Compute inter-module dependencies for Coq and Caml programs @@ -31,13 +31,13 @@ When a directory is given as argument, it is recursively looked at. Dependencies of Coq modules are computed by looking at .IR Require \& commands (Require, Require Export, Require Import), -.IR Declare \& -.IR ML \& +.IR Declare \& +.IR ML \& .IR Module \& commands and .IR Load \& commands. Dependencies relative to modules from the Coq library are not -printed except if +printed except if .BR \-boot \& is given. @@ -51,27 +51,27 @@ directives and the dot notation .TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. -.TP +.TP .BI \-I/\-Q/\-R \ options Have the same effects on load path and modules names as for other coq commands (coqtop, coqc). -.TP +.TP .BI \-coqlib \ directory Indicates where is the Coq library. The default value has been determined at installation time, and therefore this option should not be used under normal circumstances. -.TP +.TP .BI \-exclude-dir \ dir Skips subdirectory .IR dir \ during .BR -R/-Q \ search. -.TP +.TP .B \-sort Output the given file name ordered by dependencies. .TP .B \-vos Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode) -.TP +.TP .B \-boot For coq developers, prints dependencies over coq library files (omitted by default). @@ -106,7 +106,7 @@ Consider the files (in the same directory): where .TP -.BI \+ +.BI \+ D.ml contains the commands `open A', `open B' and `type t = C.t' ; .TP .BI \+ diff --git a/man/coqdoc.1 b/man/coqdoc.1 index 8d71a8746d..e8a58611f0 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -1,4 +1,4 @@ -.TH coqdoc 1 "April, 2006" +.TH coqdoc 1 .SH NAME coqdoc \- A documentation tool for the Coq proof assistant @@ -47,12 +47,12 @@ Select a TeXmacs output. Redirect the output to stdout .TP .BI \-o \ file, \-\-output \ file -Redirect the output into the file +Redirect the output into the file .I file. .TP .BI \-d \ dir, \ \-\-directory \ dir -Output files into directory -.I dir +Output files into directory +.I dir instead of current directory (option \-d does not change the filename specified with option \-o, if any). .TP @@ -102,7 +102,7 @@ Generate one page for each category and each letter in the index, together with a top page index.html. .SS Table of contents option - + .TP .B \-toc, \ \-\-table\-of\-contents Insert a table of contents. For a LATEX output, it inserts a @@ -136,7 +136,7 @@ Set the base path where the Coq files are installed, especially style files coqd .BI \-R \ dir \ coqdir Map physical directory dir to Coq logical directory coqdir (similarly to Coq option \-R). -.B Note: +.B Note: option \-R only has effect on the files following it on the command line, so you will probably need to put this option first. @@ -155,26 +155,26 @@ Light mode. Suppress proofs (as with \-g) and the following commands: * Require * Transparent / Opaque * Implicit Argument / Implicits - * Section / Variable / Hypothesis / End + * Section / Variable / Hypothesis / End The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). .SS Language options - + Default behavior is to assume ASCII 7 bits input files. -.TP +.TP .B \-latin1, \ \-\-latin1 Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1 \-\-charset iso\-8859\-1. -.TP +.TP .B \-utf8, \ \-\-utf8 Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/. -.TP +.TP .BI \-\-inputenc \ string Give a LATEX input encoding, as an option to LATEX package inputenc. @@ -187,4 +187,3 @@ Specify the HTML character set, to be inserted in the HTML header. .I The Coq Reference Manual from http://coq.inria.fr/ - diff --git a/man/coqide.1 b/man/coqide.1 index c1af046019..267f8a8d4b 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -1,4 +1,4 @@ -.TH COQIDE 1 "July 16, 2004" +.TH COQIDE 1 .SH NAME coqide \- The Coq Proof Assistant graphical interface @@ -17,7 +17,7 @@ is a gtk graphical interface for the Coq proof assistant. For command-line-oriented use of Coq, see .BR coqtop (1) -; for batch-oriented use of Coq, see +; for batch-oriented use of Coq, see .BR coqc (1). diff --git a/man/coqtop.1 b/man/coqtop.1 index e799bc7748..74380f9679 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "October 11, 2006" +.TH COQ 1 .SH NAME coqtop \- The Coq Proof Assistant toplevel system @@ -17,7 +17,7 @@ is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. -For batch-oriented use of Coq, see +For batch-oriented use of Coq, see .BR coqc(1). @@ -29,12 +29,12 @@ Help. Will give you the complete list of options accepted by coqtop. .TP .BI \-I \ dir, \ \-\-include \ dir -add directory +add directory .I dir in the include path .TP -.BI \-R \ dir\ coqdir +.BI \-R \ dir\ coqdir recursively map physical .I dir to logical @@ -67,7 +67,7 @@ load Coq file (Load filename.) .TP -.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename +.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename load verbosely Coq file .I filename.v (Load Verbose filename.) diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1 index ad1a358c32..4ef317749d 100644 --- a/man/coqtop.byte.1 +++ b/man/coqtop.byte.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coqtop.byte \- The bytecode Coq toplevel @@ -31,5 +31,3 @@ and The Coq Reference Manual. .I The Coq web site: http://coq.inria.fr - - diff --git a/man/coqtop.opt.1 b/man/coqtop.opt.1 index 17c763da33..fc097a2ecf 100644 --- a/man/coqtop.opt.1 +++ b/man/coqtop.opt.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coqtop.opt \- The native-code Coq toplevel @@ -31,5 +31,3 @@ and The Coq Reference Manual. .I The Coq web site: http://coq.inria.fr - - diff --git a/man/coqwc.1 b/man/coqwc.1 index eee37f3d1f..344b1fecc5 100644 --- a/man/coqwc.1 +++ b/man/coqwc.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "16 March 2004" "Coq tools" +.TH COQ 1 .SH NAME coqwc \- print the number of specification, proof and comment lines in diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 963f029766..c19dd00b38 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -26,16 +26,6 @@ open Pcoq.Constr (* TODO: avoid this redefinition without an extra dep to Notation_ops *) let ldots_var = Id.of_string ".." -let constr_kw = - [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; - "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "SProp"; "Prop"; "Set"; "Type"; - ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>"; - ".("; "()"; "`{"; "`("; "@{"; "{|"; - "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ] - -let _ = List.iter CLexer.add_keyword constr_kw - let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 7cabd850ad..cc59b2175b 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -15,10 +15,6 @@ open Libnames open Pcoq.Prim -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"] -let _ = List.iter CLexer.add_keyword prim_kw - - let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string ?loc s = diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0c305d09e8..c485c38009 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) | SymAx c -> @@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic = app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHEN injt (proof_tac prf)))) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = @@ -508,11 +506,9 @@ let f_equal = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = - try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match EConstr.kind sigma concl with diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0f0341f123..81e745b714 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -54,16 +54,23 @@ END { +let pr_search_strategy_name _prc _prlc _prt = function + | Dfs -> Pp.str "dfs" + | Bfs -> Pp.str "bfs" + let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" + | Some s -> pr_search_strategy_name _prc _prlc _prt s | None -> Pp.mt () } +ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name } +| [ "bfs" ] -> { Bfs } +| [ "dfs" ] -> { Dfs } +END + ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } -| [ "(bfs)" ] -> { Some Bfs } -| [ "(dfs)" ] -> { Some Dfs } +| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s } | [ ] -> { None } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index aef5f645f4..0e661543db 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 6a158bde17..e51b1f051d 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -30,9 +30,6 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] -let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw - let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 5ae0b2efd7..6d350ade8d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -162,17 +162,27 @@ let catching_error call_trace fail (e, info) = fail located_exc end -let catch_error call_trace f x = +let update_loc ?loc (e, info) = + (e, Option.cata (Loc.add_loc info) info loc) + +let catch_error ?loc call_trace f x = try f x with e when CErrors.noncritical e -> let e = Exninfo.capture e in + let e = update_loc ?loc e in catching_error call_trace Exninfo.iraise e -let wrap_error tac k = - if is_traced () then Proofview.tclORELSE tac k else tac +let catch_error_loc ?loc tac = + Proofview.tclOR tac (fun exn -> + let (e, info) = update_loc ?loc exn in + Proofview.tclZERO ~info e) + +let wrap_error ?loc tac k = + if is_traced () then Proofview.tclORELSE tac k + else catch_error_loc ?loc tac -let catch_error_tac call_trace tac = - wrap_error +let catch_error_tac ?loc call_trace tac = + wrap_error ?loc tac (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) @@ -535,9 +545,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = ltac_idents = constrvars.idents; ltac_genargs = ist.lfun; } in - let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in + let loc = loc_of_glob_constr term in + let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in let (evd,c) = - catch_error trace (understand_ltac flags env sigma vars kind) term + catch_error ?loc trace (understand_ltac flags env sigma vars kind) term in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess @@ -1059,7 +1070,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let call = LtacAtomCall t in let trace = push_trace(loc,call) ist in Profile_ltac.do_profile "eval_tactic:2" trace - (catch_error_tac trace (interp_atomic ist t)) + (catch_error_tac ?loc trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) | TacId s -> @@ -1149,7 +1160,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with ; poly ; extra = TacStore.set ist.extra f_trace trace } in val_interp ist alias.Tacenv.alias_body >>= fun v -> - Ftactic.lift (tactic_of_value ist v) + Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v)) in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> @@ -1175,7 +1186,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in let tac args = let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in - Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) + Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist)) in Ftactic.run args tac @@ -1278,7 +1289,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace [] } in Profile_ltac.do_profile "interp_app" trace ~count_call:false - (catch_error_tac trace (val_interp ist body)) >>= fun v -> + (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 633cdbd735..e7c75e029e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - try (* find_ring_strucure can raise an exception *) - let rl = make_args_list sigma rl t in - let evdref = ref sigma in - let e = find_ring_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in - let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + let rl = make_args_list sigma rl t in + let evdref = ref sigma in + let e = find_ring_structure env sigma rl in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in + let lH = carg (make_hyp_list env evdref lH) in + let ring = ltac_ring_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) end (***********************************************************************) @@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - try - let rl = make_args_list sigma rl t in - let evdref = ref sigma in - let e = find_field_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in - let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + let rl = make_args_list sigma rl t in + let evdref = ref sigma in + let e = find_field_structure env sigma rl in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in + let lH = carg (make_hyp_list env evdref lH) in + let field = ltac_field_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) end diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c7110d7a91..e77c5082dd 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -614,7 +614,7 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf = let set_names env sigma n brty = let open EConstr in let (ctxt,cl) = decompose_prod_n_assum sigma n brty in - EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt) + Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -631,11 +631,12 @@ let type_case_branches_with_names env sigma indspec p c = let nparams = mib.mind_nparams in let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in + let lbrty = Array.map EConstr.of_constr lbrty in (* Build case type *) let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then - (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty) + (set_pattern_names env sigma (fst ind) lbrty, conclty) else (lbrty, conclty) (* Type of Case predicates *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index ab69629595..2bec86599e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,7 +194,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : - env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> EConstr.types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 37d54a4eea..08178052bf 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -321,10 +321,6 @@ let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = clenv_unify CUMUL ~flags (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv -let old_clenv_unique_resolver ?flags clenv gl = - let concl = Goal.V82.concl clenv.evd (sig_it gl) in - clenv_unique_resolver_gen ?flags clenv concl - let clenv_unique_resolver ?flags clenv gl = let concl = Proofview.Goal.concl gl in clenv_unique_resolver_gen ?flags clenv concl diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 1adfdb885a..4279ab4768 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -63,9 +63,6 @@ val clenv_unify : ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv (** unifies the concl of the goal with the type of the clenv *) -val old_clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv - val clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 695e103082..c5e341c720 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -13,7 +13,6 @@ open Constr open Termops open Evd open EConstr -open Refiner open Logic open Reduction open Clenv diff --git a/proofs/logic.ml b/proofs/logic.ml index 406e71aafc..c7a1c32e7c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -28,16 +28,14 @@ module NamedDecl = Context.Named.Declaration type refiner_error = (* Errors raised by the refiner *) - | BadType of constr * constr * constr + | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * Evd.evar_map * refiner_error @@ -73,13 +71,11 @@ let catchable_exception = function let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) -(* Tells if the refiner should check that the submitted rules do not - produce invalid subgoals *) -let check = ref false -let with_check = Flags.with_option check +(* The check flag tells if the refiner should check that the submitted rules do + not produce invalid subgoals *) -let check_typability env sigma c = - if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma +let check_typability ~check env sigma c = + if check then fst (type_of env sigma (EConstr.of_constr c)) else sigma (************************************************************************) (************************************************************************) @@ -316,9 +312,9 @@ let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then raise (RefinerError (env, sigma, NonLinearProof c)) -let check_conv_leq_goal env sigma arg ty conclty = - if !check then - let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in +let check_conv_leq_goal ~check env sigma arg ty conclty = + if check then + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) conclty in match ans with | Some evm -> evm | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) @@ -334,28 +330,27 @@ let meta_free_prefix sigma a = in a with Stop acc -> Array.rev_of_list acc -let goal_type_of env sigma c = - if !check then +let goal_type_of ~check env sigma c = + if check then let (sigma,t) = type_of env sigma (EConstr.of_constr c) in (sigma, EConstr.Unsafe.to_constr t) else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) -let rec mk_refgoals sigma goal goalacc conclty trm = - let env = Goal.V82.env sigma goal in - let hyps = Goal.V82.hyps sigma goal in +let rec mk_refgoals ~check env sigma goalacc conclty trm = + let hyps = Environ.named_context_val env in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in - if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then + if (not check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in let t'ty = EConstr.Unsafe.to_constr t'ty in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else match kind trm with | Meta _ -> - let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in - if !check && occur_meta sigma conclty then + let conclty = nf_betaiota env sigma conclty in + if check && occur_meta sigma conclty then raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in @@ -363,9 +358,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> - let sigma = check_typability env sigma ty in - let sigma = check_conv_leq_goal env sigma trm ty conclty in - let res = mk_refgoals sigma goal goalacc ty t in + let sigma = check_typability ~check env sigma ty in + let sigma = check_conv_leq_goal ~check env sigma trm ty conclty in + let res = mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t in (* we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin @@ -388,24 +383,24 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let ty = EConstr.Unsafe.to_constr ty in goalacc, ty, sigma, f else - mk_hdgoals sigma goal goalacc f + mk_hdgoals ~check env sigma goalacc f in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in - let sigma = check_conv_leq_goal env sigma trm conclty' conclty in + let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in + let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in + let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in + let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -416,28 +411,27 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm."); - let (sigma, t'ty) = goal_type_of env sigma trm in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + let (sigma, t'ty) = goal_type_of ~check env sigma trm in + let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) (* Same as mkREFGOALS but without knowing the type of the term. Therefore, * Metas should be casted. *) -and mk_hdgoals sigma goal goalacc trm = - let env = Goal.V82.env sigma goal in - let hyps = Goal.V82.hyps sigma goal in +and mk_hdgoals ~check env sigma goalacc trm = + let hyps = Environ.named_context_val env in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> - let sigma = check_typability env sigma ty in + let sigma = check_typability ~check env sigma ty in let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> - let sigma = check_typability env sigma ty in - mk_refgoals sigma goal goalacc ty t + let sigma = check_typability ~check env sigma ty in + mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t | App (f,l) -> let (acc',hdty,sigma,applicand) = @@ -445,15 +439,15 @@ and mk_hdgoals sigma goal goalacc trm = then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) - else mk_hdgoals sigma goal goalacc f + else mk_hdgoals ~check env sigma goalacc f in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in + let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -462,21 +456,21 @@ and mk_hdgoals sigma goal goalacc trm = (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | _ -> - if !check && occur_meta sigma (EConstr.of_constr trm) then + if check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta."); - let (sigma, ty) = goal_type_of env sigma trm in + let (sigma, ty) = goal_type_of env ~check sigma trm in goalacc, ty, sigma, trm -and mk_arggoals sigma goal goalacc funty allargs = +and mk_arggoals ~check env sigma goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = whd_all env sigma (EConstr.of_constr funty) in let t = EConstr.Unsafe.to_constr t in let rec collapse t = match kind t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) @@ -485,19 +479,17 @@ and mk_arggoals sigma goal goalacc funty allargs = let t = collapse t in match kind t with | Prod (_, c1, b) -> - let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in + let (acc, hargty, sigma, arg) = mk_refgoals ~check env sigma goalacc (EConstr.of_constr c1) harg in (acc, subst1 harg b, sigma), arg | _ -> - let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs -and mk_casegoals sigma goal goalacc p c = - let env = Goal.V82.env sigma goal in - let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in +and mk_casegoals ~check env sigma goalacc p c = + let (acc',ct,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let ct = EConstr.of_constr ct in - let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in + let (acc'',pt,sigma,p') = mk_hdgoals ~check env sigma acc' p in let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals.") in @@ -505,20 +497,19 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') -and treat_case sigma goal ci lbrty lf acc' = +and treat_case ~check env sigma ci lbrty lf acc' = let rec strip_outer_cast c = match kind c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c in let decompose_app_vect c = match kind c with | App (f,cl) -> (f, cl) | _ -> (c,[||]) in - let env = Goal.V82.env sigma goal in Array.fold_left3 (fun (lacc,sigma,bacc) ty fi l -> if isMeta (strip_outer_cast fi) then (* Support for non-eta-let-expanded Meta as found in *) (* destruct/case with an non eta-let expanded elimination scheme *) - let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in + let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in r,s,(fi'::bacc) else (* Deal with a branch in expanded form of the form @@ -539,14 +530,14 @@ and treat_case sigma goal ci lbrty lf acc' = if isMeta head then begin assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); let head' = lift (-n) head in - let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in + let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in (r,s,fi'::bacc) end else (* Supposed to be meta-free *) - let sigma, t'ty = goal_type_of env sigma fi in - let sigma = check_conv_leq_goal env sigma fi t'ty ty in + let sigma, t'ty = goal_type_of ~check env sigma fi in + let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags @@ -574,18 +565,18 @@ let convert_hyp ~check ~reorder env sigma d = (************************************************************************) (* Primitive tactics are handled here *) -let prim_refiner r sigma goal = - let env = Goal.V82.env sigma goal in - let cl = Goal.V82.concl sigma goal in - let cl = EConstr.Unsafe.to_constr cl in +let refiner ~check r = + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let st = Proofview.Goal.state gl in + let cl = Proofview.Goal.concl gl in check_meta_variables env sigma r; - let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in - let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in - (sgl, sigma) - -let prim_refiner ~check r sigma goal = - if check then - with_check (prim_refiner r sigma) goal - else - prim_refiner r sigma goal + let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in + let map gl = Proofview.goal_with_state gl st in + let sgl = List.rev_map map sgl in + let sigma = Goal.V82.partial_solution env sigma (Proofview.Goal.goal gl) (EConstr.of_constr oterm) in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS sgl + end diff --git a/proofs/logic.mli b/proofs/logic.mli index ef8b2731b2..9dc75000a1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -26,23 +26,21 @@ open Evd (** The primitive refiner. *) -val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map +val refiner : check:bool -> constr -> unit Proofview.tactic (** {6 Refiner errors. } *) type refiner_error = (*i Errors raised by the refiner i*) - | BadType of constr * constr * constr + | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (*i Errors raised by the tactics i*) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * evar_map * refiner_error diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 29a47c5acd..874bab277d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -12,7 +12,6 @@ open Pp open CErrors open Util open Evd -open Logic type tactic = Proofview.V82.tac @@ -26,18 +25,7 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let refiner ~check pr goal_sigma = - let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in - { it = sgl; sigma = sigma'; } - -(* Profiling refiner *) -let refiner ~check = - if Flags.profile then - let refiner_key = CProfile.declare_profile "refiner" in - CProfile.profile2 refiner_key (refiner ~check) - else refiner ~check - -let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c) +let refiner = Logic.refiner (*********************) (* Tacticals *) diff --git a/tactics/equality.ml b/tactics/equality.ml index e1d34af13e..b92a65d767 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1707,12 +1707,42 @@ let is_eq_x gl x d = with Constr_matching.PatternMatchingFailure -> () +exception FoundDepInGlobal of Id.t option * GlobRef.t + +let test_non_indirectly_dependent_section_variable gl x = + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + List.iter (fun decl -> + NamedDecl.iter_constr (fun c -> + match occur_var_indirectly env sigma x c with + | Some gr -> raise (FoundDepInGlobal (Some (NamedDecl.get_id decl), gr)) + | None -> ()) decl) hyps; + match occur_var_indirectly env sigma x concl with + | Some gr -> raise (FoundDepInGlobal (None, gr)) + | None -> () + +let check_non_indirectly_dependent_section_variable gl x = + try test_non_indirectly_dependent_section_variable gl x + with FoundDepInGlobal (pos,gr) -> + let where = match pos with + | Some id -> str "hypothesis " ++ Id.print id + | None -> str "the conclusion of the goal" in + user_err ~hdr:"Subst" + (strbrk "Section variable " ++ Id.print x ++ + strbrk " occurs implicitly in global declaration " ++ Printer.pr_global gr ++ + strbrk " present in " ++ where ++ strbrk ".") + +let is_non_indirectly_dependent_section_variable gl z = + try test_non_indirectly_dependent_section_variable gl z; true + with FoundDepInGlobal (pos,gr) -> false + (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -1721,7 +1751,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) - && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps + && List.exists (fun y -> local_occur_var_in_decl sigma y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in (dest,id::deps,(id_dest,id)::allhyps) @@ -1730,7 +1760,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = hyps (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) - let depconcl = occur_var env sigma x concl in + let depconcl = local_occur_var sigma x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then @@ -1761,6 +1791,8 @@ let subst_one_var dep_proof_ok x = (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in + if is_section_variable x then + check_non_indirectly_dependent_section_variable gl x; subst_one dep_proof_ok x res end @@ -1794,53 +1826,37 @@ let subst_all ?(flags=default_subst_tactic_flags) () = if !regular_subst_tactic then - (* First step: find hypotheses to treat in linear time *) - let find_equations gl = - let env = Proofview.Goal.env gl in - let sigma = project gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let select_equation_name decl = + (* Find hypotheses to treat in linear time *) + let process hyp = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = project gl in + let c = pf_get_hyp hyp gl |> NamedDecl.get_type in try - let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in + let lbeq,u,(_,x,y) = pf_apply find_eq_data_decompose gl c in let u = EInstance.kind sigma u in let eq = Constr.mkRef (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with - | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) - | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) + | Var x, Var y when Id.equal x y -> + Proofview.tclUNIT () + | Var x', _ when not (Termops.local_occur_var sigma x' y) && + not (is_evaluable env (EvalVarRef x')) && + is_non_indirectly_dependent_section_variable gl x' -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (Termops.local_occur_var sigma y' x) && + not (is_evaluable env (EvalVarRef y')) && + is_non_indirectly_dependent_section_variable gl y' -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> - None - with Constr_matching.PatternMatchingFailure -> None + Proofview.tclUNIT () + with Constr_matching.PatternMatchingFailure -> + Proofview.tclUNIT () + end in - let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter select_equation_name hyps) - in - - (* Second step: treat equations *) - let process hyp = Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let env = Proofview.Goal.env gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let c = pf_get_hyp hyp gl |> NamedDecl.get_type in - let _,_,(_,x,y) = find_eq_data_decompose c in - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else - match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) -> - subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) -> - subst_one flags.rewrite_dependent_proof y' (hyp,x,false) - | _ -> - Proofview.tclUNIT () + tclMAP process (List.rev (List.map NamedDecl.get_id (Proofview.Goal.hyps gl))) end - in - Proofview.Goal.enter begin fun gl -> - let ids = find_equations gl in - tclMAP process ids - end else diff --git a/test-suite/bugs/closed/bug_10812.v b/test-suite/bugs/closed/bug_10812.v new file mode 100644 index 0000000000..68f3814781 --- /dev/null +++ b/test-suite/bugs/closed/bug_10812.v @@ -0,0 +1,28 @@ +(* subst with indirectly dependent section variables *) + +Section A. + +Variable a:nat. +Definition b := a. + +Goal a=1 -> a+a=1 -> b=1. +intros. +Fail subst a. (* was working; we make it failing *) +rewrite H in H0. +discriminate. +Qed. + +Goal a=1 -> a+a=1 -> b=1. +intros. +subst. (* should not apply to a *) +rewrite H in H0. +discriminate. +Qed. + +Goal forall t, a=t -> b=t. +intros. +subst. +reflexivity. +Qed. + +End A. diff --git a/test-suite/bugs/closed/bug_7903.v b/test-suite/bugs/closed/bug_7903.v index 55c7ee99a7..18e1884ca7 100644 --- a/test-suite/bugs/closed/bug_7903.v +++ b/test-suite/bugs/closed/bug_7903.v @@ -1,4 +1,4 @@ (* Slightly improving interpretation of Ltac subterms in notations *) Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). -Check bar x (x + x). +Check fun x => bar x (x + x). diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v new file mode 100644 index 0000000000..14232e8578 --- /dev/null +++ b/test-suite/bugs/closed/bug_9583.v @@ -0,0 +1,7 @@ +(* Was causing a stack overflow before #11613 *) +Declare Custom Entry bla. +Notation "[ t ]" := (t) (at level 0, t custom bla at level 0). +Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0). +Notation "t" := (t) (in custom bla at level 0, t constr at level 9). +Notation "0" := (0) (in custom bla at level 0). +Check fun x => [ ] x [ ]. diff --git a/test-suite/bugs/closed/bug_9679.v b/test-suite/bugs/closed/bug_9679.v new file mode 100644 index 0000000000..24e69d23f9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9679.v @@ -0,0 +1,6 @@ +(* Was raising an anomaly *) +Notation "'[#' ] f '|' x .. z '=n>' b" := + (fun x => .. (fun z => f b) ..) + (at level 201, x binder, z binder, + format "'[ ' [# ] '[' f | ']' x .. z =n> '[' b ']' ']'" + ). diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index e1c20a2059..7b3a460c8c 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -15,6 +15,39 @@ Fail foo (). constructor. Qed. + +(** Bindings are dynamic *) + +Ltac2 Type rec nat := [O | S (nat)]. + +Ltac2 rec nat_eq n m := + match n with + | O => match m with | O => true | S _ => false end + | S n => match m with | O => false | S m => nat_eq n m end + end. + +Ltac2 Type exn ::= [ Assertion_failed ]. + +Ltac2 assert_eq n m := + match nat_eq n m with + | true => () + | false => Control.throw Assertion_failed end. + +Ltac2 mutable x := O. +Ltac2 y := x. +Ltac2 Eval (assert_eq y O). +Ltac2 Set x := (S O). +Ltac2 Eval (assert_eq y (S O)). + +Ltac2 mutable quw := fun (n : nat) => O. +Ltac2 Set quw := fun n => + match n with + | O => O + | S n => S (S (quw n)) + end. + +Ltac2 Eval (quw (S (S O))). + (** Not the right type *) Fail Ltac2 Set foo := 0. @@ -25,10 +58,46 @@ Fail Ltac2 Set bar := fun _ => (). (** Subtype check *) -Ltac2 mutable rec f x := f x. +Ltac2 rec h x := h x. +Ltac2 mutable f x := h x. Fail Ltac2 Set f := fun x => x. Ltac2 mutable g x := x. +Ltac2 Set g := h. + +(** Rebinding with old values *) + + + +Ltac2 mutable qux n := S n. + +Ltac2 Set qux as self := fun n => self (self n). + +Ltac2 Eval assert_eq (qux O) (S (S O)). + +Ltac2 mutable quz := O. + +Ltac2 Set quz as self := S self. + +Ltac2 Eval (assert_eq quz (S O)). + +Ltac2 rec addn n := + match n with + | O => fun m => m + | S n => fun m => S (addn n m) + + end. +Ltac2 mutable rec quy n := + match n with + | O => S O + | S n => S (quy n) + end. -Ltac2 Set g := f. +Ltac2 Set quy as self := fun n => + match n with + | O => O + | S n => addn (self n) (quy n) + end. +Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))). +Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))). diff --git a/test-suite/output/ErrorLocation_12152_1.out b/test-suite/output/ErrorLocation_12152_1.out new file mode 100644 index 0000000000..b7b600d53d --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-7: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v new file mode 100644 index 0000000000..e63ab1cd48 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intro H; auto. diff --git a/test-suite/output/ErrorLocation_12152_2.out b/test-suite/output/ErrorLocation_12152_2.out new file mode 100644 index 0000000000..bdfd0a050f --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-8: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v new file mode 100644 index 0000000000..5df6bec939 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intros H; auto. diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out new file mode 100644 index 0000000000..ed5e183427 --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 0-16: +Error: Ltac variable x is bound to i > 0 which cannot be coerced to +an evaluable reference. + diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v new file mode 100644 index 0000000000..347424b2fc --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.v @@ -0,0 +1,4 @@ +Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. +Definition i := O. +Goal False. +can_unfold (i>0). diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f48eaac4c9..9cb019ca56 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -111,3 +111,11 @@ Warning: The format modifier is irrelevant for only parsing rules. File "stdin", line 280, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] +fun x : nat => U (S x) + : nat -> nat +V tt + : unit * (unit -> unit) +fun x : nat => V x + : forall x : nat, nat * (?T -> ?T) +where +?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4d4b37a8b2..b3270d4f92 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -280,3 +280,13 @@ Notation "###" := 0 (at level 0, only parsing, format "###"). Reserved Notation "##" (at level 0, only parsing, format "##"). End N. + +Module O. + +Notation U t := (match t with 0 => 0 | S t => t | _ => 0 end). +Check fun x => U (S x). +Notation V t := (t,fun t => t). +Check V tt. +Check fun x : nat => V x. + +End O. diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v index 676b97878f..032fcaac6d 100644 --- a/test-suite/success/shrink_obligations.v +++ b/test-suite/success/shrink_obligations.v @@ -2,8 +2,6 @@ Require Program. Obligation Tactic := idtac. -Set Shrink Obligations. - Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit := let bar : {r | n < r} := _ in let qux : {r | p < r} := _ in diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 57cc8c4e90..d70978fabe 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -82,34 +82,39 @@ Qed. (** * Order on booleans *) (************************) -Definition leb (b1 b2:bool) := +#[ local ] Definition le (b1 b2:bool) := match b1 with | true => b2 = true | false => True end. -Hint Unfold leb: bool. +Hint Unfold le: bool. -Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true. +Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true. Proof. destr_bool; intuition. Qed. -Definition ltb (b1 b2:bool) := +#[deprecated(since="8.12",note="Use Bool.le instead.")] +Notation leb := le (only parsing). +#[deprecated(since="8.12",note="Use Bool.le_implb instead.")] +Notation leb_implb := le_implb (only parsing). + +#[ local ] Definition lt (b1 b2:bool) := match b1 with | true => False | false => b2 = true end. -Hint Unfold ltb: bool. +Hint Unfold lt: bool. -Definition compareb (b1 b2 : bool) := +#[ local ] Definition compare (b1 b2 : bool) := match b1, b2 with | false, true => Lt | true, false => Gt | _, _ => Eq end. -Lemma compareb_spec : forall b1 b2, - CompareSpec (b1 = b2) (ltb b1 b2) (ltb b2 b1) (compareb b1 b2). +Lemma compare_spec : forall b1 b2, + CompareSpec (b1 = b2) (lt b1 b2) (lt b2 b1) (compare b1 b2). Proof. destr_bool; auto. Qed. @@ -935,8 +940,8 @@ Defined. (** Notations *) Module BoolNotations. -Infix "<=" := leb : bool_scope. -Infix "<" := ltb : bool_scope. -Infix "?=" := compareb (at level 70) : bool_scope. +Infix "<=" := le : bool_scope. +Infix "<" := lt : bool_scope. +Infix "?=" := compare (at level 70) : bool_scope. Infix "=?" := eqb (at level 70) : bool_scope. End BoolNotations. diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v index 61aab607a9..aaa7321bfc 100644 --- a/theories/Bool/BoolOrder.v +++ b/theories/Bool/BoolOrder.v @@ -14,69 +14,65 @@ Require Export Bool. Require Import Orders. - -Local Notation le := Bool.leb. -Local Notation lt := Bool.ltb. -Local Notation compare := Bool.compareb. -Local Notation compare_spec := Bool.compareb_spec. +Import BoolNotations. (** * Order [le] *) -Lemma le_refl : forall b, le b b. +Lemma le_refl : forall b, b <= b. Proof. destr_bool. Qed. Lemma le_trans : forall b1 b2 b3, - le b1 b2 -> le b2 b3 -> le b1 b3. + b1 <= b2 -> b2 <= b3 -> b1 <= b3. Proof. destr_bool. Qed. -Lemma le_true : forall b, le b true. +Lemma le_true : forall b, b <= true. Proof. destr_bool. Qed. -Lemma false_le : forall b, le false b. +Lemma false_le : forall b, false <= b. Proof. intros; constructor. Qed. -Instance le_compat : Proper (eq ==> eq ==> iff) le. +Instance le_compat : Proper (eq ==> eq ==> iff) Bool.le. Proof. intuition. Qed. (** * Strict order [lt] *) -Lemma lt_irrefl : forall b, ~ lt b b. +Lemma lt_irrefl : forall b, ~ b < b. Proof. destr_bool; auto. Qed. Lemma lt_trans : forall b1 b2 b3, - lt b1 b2 -> lt b2 b3 -> lt b1 b3. + b1 < b2 -> b2 < b3 -> b1 < b3. Proof. destr_bool; auto. Qed. -Instance lt_compat : Proper (eq ==> eq ==> iff) lt. +Instance lt_compat : Proper (eq ==> eq ==> iff) Bool.lt. Proof. intuition. Qed. -Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }. +Lemma lt_trichotomy : forall b1 b2, { b1 < b2 } + { b1 = b2 } + { b2 < b1 }. Proof. destr_bool; auto. Qed. -Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1. +Lemma lt_total : forall b1 b2, b1 < b2 \/ b1 = b2 \/ b2 < b1. Proof. destr_bool; auto. Qed. -Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2. +Lemma lt_le_incl : forall b1 b2, b1 < b2 -> b1 <= b2. Proof. destr_bool; auto. Qed. -Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }. +Lemma le_lteq_dec : forall b1 b2, b1 <= b2 -> { b1 < b2 } + { b1 = b2 }. Proof. destr_bool; auto. Qed. -Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2. +Lemma le_lteq : forall b1 b2, b1 <= b2 <-> b1 < b2 \/ b1 = b2. Proof. destr_bool; intuition. Qed. (** * Order structures *) (* Class structure *) -Instance le_preorder : PreOrder le. +Instance le_preorder : PreOrder Bool.le. Proof. split. - intros b; apply le_refl. - intros b1 b2 b3; apply le_trans. Qed. -Instance lt_strorder : StrictOrder lt. +Instance lt_strorder : StrictOrder Bool.lt. Proof. split. - intros b; apply lt_irrefl. @@ -88,13 +84,13 @@ Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. Definition t := bool. Definition eq := @eq bool. Definition eq_equiv := @eq_equivalence bool. - Definition lt := lt. + Definition lt := Bool.lt. Definition lt_strorder := lt_strorder. Definition lt_compat := lt_compat. - Definition le := le. + Definition le := Bool.le. Definition le_lteq := le_lteq. Definition lt_total := lt_total. - Definition compare := compare. + Definition compare := Bool.compare. Definition compare_spec := compare_spec. Definition eq_dec := bool_dec. Definition eq_refl := @eq_Reflexive bool. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 31e8cf463e..474b417e8e 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -44,18 +44,18 @@ Definition In (s:uniset) (a:A) : Prop := charac s a = true. Hint Unfold In : core. (** uniset inclusion *) -Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). +Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a). Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. Hint Unfold seq : core. -Lemma leb_refl : forall b:bool, leb b b. +Lemma le_refl : forall b, Bool.le b b. Proof. destruct b; simpl; auto. Qed. -Hint Resolve leb_refl : core. +Hint Resolve le_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 1dd9285412..026cf32ceb 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -273,8 +273,8 @@ Proof. exact Permutation_length. Qed. -Instance Permutation_Forall (P : A -> Prop) : - Proper ((@Permutation A) ==> Basics.impl) (Forall P). +Global Instance Permutation_Forall (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Forall P) | 10. Proof. intros l1 l2 HP. induction HP; intro HF; auto. @@ -283,8 +283,8 @@ Proof. inversion_clear HF2; auto. Qed. -Instance Permutation_Exists (P : A -> Prop) : - Proper ((@Permutation A) ==> Basics.impl) (Exists P). +Global Instance Permutation_Exists (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Exists P) | 10. Proof. intros l1 l2 HP. induction HP; intro HF; auto. @@ -581,8 +581,8 @@ Proof. now contradiction (Hf x). Qed. -Instance Permutation_flat_map (g : A -> list B) : - Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g). +Global Instance Permutation_flat_map (g : A -> list B) : + Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g) | 10. Proof. intros l1; induction l1; intros l2 HP. - now apply Permutation_nil in HP; subst. @@ -773,7 +773,7 @@ Qed. End Permutation_alt. -Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum. +Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum | 10. Proof. intros l1 l2 HP; induction HP; simpl; intuition. - rewrite 2 (Nat.add_comm x). @@ -781,7 +781,7 @@ Proof. - now transitivity (list_sum l'). Qed. -Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max. +Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max | 10. Proof. intros l1 l2 HP; induction HP; simpl; intuition. - rewrite 2 (Nat.max_comm x). @@ -806,7 +806,7 @@ Proof. now apply (perm_t_trans IHHP2). Qed. -Instance Permutation_transp_equiv : Equivalence Permutation_transp. +Global Instance Permutation_transp_equiv : Equivalence Permutation_transp | 100. Proof. split. - intros l; apply perm_t_refl. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 13c4d667a0..8979170026 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -289,7 +289,7 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_mut: - [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ] + [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ] ; tac2typ_knd: [ [ t = tac2type -> { CTydDef (Some t) } diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 28e877491e..987cd8c1b8 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -336,7 +336,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics = if isrec then inline_rec_tactic tactics else tactics in let map ({loc;v=id}, e) = - let (e, t) = intern ~strict:true e in + let (e, t) = intern ~strict:true [] e in let () = if not (is_value e) then user_err ?loc (str "Tactic definition must be a syntactical value") @@ -728,19 +728,26 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with type redefinition = { redef_kn : ltac_constant; redef_body : glb_tacexpr; + redef_old : Id.t option; } let perform_redefinition (_, redef) = let kn = redef.redef_kn in let data = Tac2env.interp_global kn in - let data = { data with Tac2env.gdata_expr = redef.redef_body } in + let body = match redef.redef_old with + | None -> redef.redef_body + | Some id -> + (* Rebind the old value with a let-binding *) + GTacLet (false, [Name id, data.Tac2env.gdata_expr], redef.redef_body) + in + let data = { data with Tac2env.gdata_expr = body } in Tac2env.define_global kn data let subst_redefinition (subst, redef) = let kn = Mod_subst.subst_kn subst redef.redef_kn in let body = Tac2intern.subst_expr subst redef.redef_body in if kn == redef.redef_kn && body == redef.redef_body then redef - else { redef_kn = kn; redef_body = body } + else { redef_kn = kn; redef_body = body; redef_old = redef.redef_old } let classify_redefinition o = Substitute o @@ -751,7 +758,7 @@ let inTac2Redefinition : redefinition -> obj = subst_function = subst_redefinition; classify_function = classify_redefinition } -let register_redefinition ?(local = false) qid e = +let register_redefinition ?(local = false) qid old e = let kn = try Tac2env.locate_ltac qid with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown tactic " ++ pr_qualid qid) @@ -766,7 +773,11 @@ let register_redefinition ?(local = false) qid e = if not (data.Tac2env.gdata_mutable) then user_err ?loc:qid.CAst.loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable") in - let (e, t) = intern ~strict:true e in + let ctx = match old with + | None -> [] + | Some { CAst.v = id } -> [id, data.Tac2env.gdata_type] + in + let (e, t) = intern ~strict:true ctx e in let () = if not (is_value e) then user_err ?loc:qid.CAst.loc (str "Tactic definition must be a syntactical value") @@ -777,15 +788,17 @@ let register_redefinition ?(local = false) qid e = user_err ?loc:qid.CAst.loc (str "Type " ++ pr_glbtype name (snd t) ++ str " is not a subtype of " ++ pr_glbtype name (snd data.Tac2env.gdata_type)) in + let old = Option.map (fun { CAst.v = id } -> id) old in let def = { redef_kn = kn; redef_body = e; + redef_old = old; } in Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = let env = Global.env () in - let (e, ty) = Tac2intern.intern ~strict:false e in + let (e, ty) = Tac2intern.intern ~strict:false [] e in let v = Tac2interp.interp Tac2interp.empty_environment e in let selector, proof = match pstate with @@ -818,7 +831,7 @@ let register_struct ?local str = match str with | StrTyp (isrec, t) -> register_type ?local isrec t | StrPrm (id, t, ml) -> register_primitive ?local id t ml | StrSyn (tok, lev, e) -> register_notation ?local tok lev e -| StrMut (qid, e) -> register_redefinition ?local qid e +| StrMut (qid, old, e) -> register_redefinition ?local qid old e (** Toplevel exception *) @@ -913,7 +926,7 @@ let solve ~pstate default tac = let call ~pstate ~default e = let loc = e.loc in - let (e, t) = intern ~strict:false e in + let (e, t) = intern ~strict:false [] e in let () = check_unit ?loc t in let tac = Tac2interp.interp Tac2interp.empty_environment e in solve ~pstate default (Proofview.tclIGNORE tac) diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index a95d8cc49f..548655f561 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -168,7 +168,7 @@ type strexpr = (** External definition *) | StrSyn of sexpr list * int option * raw_tacexpr (** Syntactic extensions *) -| StrMut of qualid * raw_tacexpr +| StrMut of qualid * Names.lident option * raw_tacexpr (** Redefinition of mutable globals *) (** {5 Dynamic semantics} *) diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index a4f385d432..797f72702d 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -396,11 +396,13 @@ let is_pure_constructor kn = let rec is_value = function | GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true -| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false +| GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false | GTacCst (Tuple _, _, el) -> List.for_all is_value el | GTacCst (_, _, []) -> true | GTacOpn (_, el) -> List.for_all is_value el | GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el +| GTacLet (false, bnd, e) -> + is_value e && List.for_all (fun (_, e) -> is_value e) bnd | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ | GTacWth _ -> false @@ -458,6 +460,10 @@ let monomorphic (t : UF.elt glb_typexpr) : mix_type_scheme = let subst id = GTypVar (GVar id) in (0, subst_type subst t) +let polymorphic ((n, t) : type_scheme) : mix_type_scheme = + let subst id = GTypVar (LVar id) in + (n, subst_type subst t) + let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" (fun () -> strbrk "The following expression should have type unit.") @@ -1138,9 +1144,13 @@ let normalize env (count, vars) (t : UF.elt glb_typexpr) = in subst_type subst t -let intern ~strict e = +type context = (Id.t * type_scheme) list + +let intern ~strict ctx e = let env = empty_env () in let env = if strict then env else { env with env_str = false } in + let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in + let env = List.fold_left fold env ctx in let (e, t) = intern_rec env e in let count = ref 0 in let vars = ref UF.Map.empty in diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli index 8b09ecbcf7..ed251d6201 100644 --- a/user-contrib/Ltac2/tac2intern.mli +++ b/user-contrib/Ltac2/tac2intern.mli @@ -12,7 +12,9 @@ open Names open Mod_subst open Tac2expr -val intern : strict:bool -> raw_tacexpr -> glb_tacexpr * type_scheme +type context = (Id.t * type_scheme) list + +val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef val intern_open_type : raw_typexpr -> type_scheme diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml index 54f2da0621..ed783afce7 100644 --- a/user-contrib/Ltac2/tac2interp.ml +++ b/user-contrib/Ltac2/tac2interp.ml @@ -86,7 +86,7 @@ let rec interp (ist : environment) = function | GTacVar id -> return (get_var ist id) | GTacRef kn -> let data = get_ref ist kn in - return (eval_pure (Some kn) data) + return (eval_pure Id.Map.empty (Some kn) data) | GTacFun (ids, e) -> let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in let f = interp_app cls in @@ -187,26 +187,41 @@ and interp_set ist e p r = let () = Valexpr.set_field e p r in return (Valexpr.make_int 0) -and eval_pure kn = function +and eval_pure bnd kn = function +| GTacVar id -> Id.Map.get id bnd | GTacAtm (AtmInt n) -> Valexpr.make_int n | GTacRef kn -> let { Tac2env.gdata_expr = e } = try Tac2env.interp_global kn with Not_found -> assert false in - eval_pure (Some kn) e + eval_pure bnd (Some kn) e | GTacFun (na, e) -> - let cls = { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e } in + let cls = { clos_ref = kn; clos_env = bnd; clos_var = na; clos_exp = e } in let f = interp_app cls in Tac2ffi.of_closure f | GTacCst (_, n, []) -> Valexpr.make_int n -| GTacCst (_, n, el) -> Valexpr.make_block n (Array.map_of_list eval_unnamed el) -| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, Array.map_of_list eval_unnamed el) -| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _ +| GTacCst (_, n, el) -> Valexpr.make_block n (eval_pure_args bnd el) +| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, eval_pure_args bnd el) +| GTacLet (isrec, vals, body) -> + let () = assert (not isrec) in + let fold accu (na, e) = match na with + | Anonymous -> + (* No need to evaluate, we know this is a value *) + accu + | Name id -> + let v = eval_pure bnd None e in + Id.Map.add id v accu + in + let bnd = List.fold_left fold bnd vals in + eval_pure bnd kn body +| GTacAtm (AtmStr _) | GTacSet _ | GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ -> anomaly (Pp.str "Term is not a syntactical value") -and eval_unnamed e = eval_pure None e +and eval_pure_args bnd args = + let map e = eval_pure bnd None e in + Array.map_of_list map args (** Cross-boundary hacks. *) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index ab11472dec..9ea54f5d8f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -111,11 +111,6 @@ open ProgramDecl (* Saving an obligation *) -let get_shrink_obligations = - Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) - ~key:["Shrink"; "Obligations"] - ~value:true - (* XXX: Is this the right place for this? *) let it_mkLambda_or_LetIn_or_clean t ctx = let open Context.Rel.Declaration in @@ -190,7 +185,7 @@ let add_hint local prg cst = (* true = hide obligations *) let get_hide_obligations = Goptions.declare_bool_option_and_ref - ~depr:false + ~depr:true ~key:["Hide"; "Obligations"] ~value:false @@ -203,7 +198,7 @@ let declare_obligation prg obl body ty uctx = let opaque = (not force) && opaque in let poly = prg.prg_poly in let ctx, body, ty, args = - if get_shrink_obligations () && not poly then shrink_body body ty + if not poly then shrink_body body ty else ([], body, ty, [||]) in let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 058fa691ee..80a4de472c 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -97,7 +97,7 @@ GRAMMAR EXTEND Gram | IDENT "Guarded" -> { VernacCheckGuard } (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; - id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] -> + id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] -> { VernacCreateHintDb (id, b) } | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> { VernacRemoveHints (dbnames, ids) } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 049c3a0844..42259cee10 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,9 +30,6 @@ open Pcoq.Module open Pvernac.Vernac_ open Attributes -let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw - (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 41f2ab9c63..9d67ce3757 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function (* Refiner errors *) let explain_refiner_bad_type env sigma arg ty conclty = - let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in + let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in str "Refiner was given an argument" ++ brk(1,1) ++ pr_lconstr_env env sigma arg ++ spc () ++ str "of type" ++ brk(1,1) ++ pm ++ spc () ++ @@ -1112,16 +1112,9 @@ let explain_refiner_cannot_apply env sigma t harg = pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ pr_lconstr_env env sigma harg ++ str "." -let explain_refiner_not_well_typed env sigma c = - str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed." - let explain_intro_needs_product () = str "Introduction tactics needs products." -let explain_does_not_occur_in env sigma c hyp = - str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ - str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." - let explain_non_linear_proof env sigma c = str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++ spc () ++ str "because a metavariable has several occurrences." @@ -1137,9 +1130,7 @@ let explain_refiner_error env sigma = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg - | NotWellTyped c -> explain_refiner_not_well_typed env sigma c | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp | NonLinearProof c -> explain_non_linear_proof env sigma c | MetaInType c -> explain_meta_in_type env sigma c | NoSuchHyp id -> explain_no_such_hyp id diff --git a/vernac/library.ml b/vernac/library.ml index 85db501e84..c30331b221 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -89,6 +89,7 @@ type library_disk = { type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } (*s Modules loaded in memory contain the following informations. They are @@ -251,6 +252,7 @@ let intern_from_file f = let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in ObjFile.close_in ch; + System.check_caml_version ~caml:lsd.md_ocaml ~file:f; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in @@ -401,6 +403,7 @@ let load_library_todo f = let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in ObjFile.close_in ch; + System.check_caml_version ~caml:s0.md_ocaml ~file:f; if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); @@ -486,6 +489,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); + md_ocaml = Coq_config.caml_version; } in let md = { md_compiled = cenv; diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 3b9c771b93..32affd562f 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1073,12 +1073,12 @@ let make_internalization_vars recvars mainvars typs = let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in maintyps @ extratyps -let make_interpretation_type isrec isonlybinding = function +let make_interpretation_type isrec isonlybinding default_if_binding = function (* Parsed as constr list *) | ETConstr (_,None,_) when isrec -> NtnTypeConstrList - (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *) + (* Parsed as constr, but interpreted as a binder *) | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk) - | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent) + | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr default_if_binding) (* Parsed as constr, interpreted as constr *) | ETConstr (_,None,_) -> NtnTypeConstr (* Others *) @@ -1096,7 +1096,9 @@ let subentry_of_constr_prod_entry = function | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel | _ -> InConstrEntrySomeLevel -let make_interpretation_vars recvars allvars typs = +let make_interpretation_vars + (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent) + recvars allvars typs = let eq_subscope (sc1, l1) (sc2, l2) = Option.equal String.equal sc1 sc2 && List.equal String.equal l1 l2 @@ -1113,7 +1115,7 @@ let make_interpretation_vars recvars allvars typs = Id.Map.mapi (fun x (isonlybinding, sc) -> let typ = Id.List.assoc x typs in ((subentry_of_constr_prod_entry typ,sc), - make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars + make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding default_if_binding typ)) mainvars let check_rule_productivity l = if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then @@ -1792,8 +1794,8 @@ let try_interp_name_alias = function | _ -> raise Not_found let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } = - let vars,reversibility,pat = - try [], APrioriReversible, NRef (try_interp_name_alias (vars,c)) + let acvars,pat,reversibility = + try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible with Not_found -> let fold accu id = Id.Map.add id NtnInternTypeAny accu in let i_vars = List.fold_left fold Id.Map.empty vars in @@ -1801,10 +1803,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; } in - let nvars, pat, reversibility = interp_notation_constr env nenv c in - let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in - List.map map vars, reversibility, pat + interp_notation_constr env nenv c in + let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in + let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in + let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) |