diff options
35 files changed, 285 insertions, 313 deletions
diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 1648638555..862c54900f 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -58,7 +58,7 @@ jobs: displayName: 'Install system dependencies' env: HOMEBREW_NO_AUTO_UPDATE: "1" - HBCORE_DATE: "2019-06-18" + HBCORE_DATE: "2019-06-16" HBCORE_REF: "944a5b7d83e4b81c749d93831b514607bdd2b6a1" - script: | diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index dadb2bb8f1..ad22c394d8 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -181,9 +181,9 @@ ######################################################################## # SF ######################################################################## -: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}" -: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}" -: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}" +: "${sf_lf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz}" +: "${sf_plf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz}" +: "${sf_vfa_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz}" ######################################################################## # TLC diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index d1b95e6203..ac75240cfb 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -7,22 +7,20 @@ The |Coq| library single: Theories -The |Coq| library is structured into two parts: +The |Coq| library has two parts: - * **The initial library**: it contains elementary logical notions and - data-types. It constitutes the basic state of the system directly - available when running |Coq|; + * **The basic library**: 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 containing various - developments of |Coq| axiomatizations about sets, lists, sorting, - arithmetic, etc. This library comes with the system and its modules - are directly accessible through the ``Require`` command (see - Section :ref:`compiled-files`); + * **The 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`) -In addition, user-provided libraries or developments are provided by -|Coq| users' community. These libraries and developments are available -for download at http://coq.inria.fr (see -Section :ref:`userscontributions`). +There are also many libraries provided by |Coq| users' community. +These libraries and developments are available +for download at http://coq.inria.fr (see :ref:`userscontributions`). This chapter briefly reviews the |Coq| libraries whose contents can also be browsed at http://coq.inria.fr/stdlib. @@ -514,8 +512,8 @@ realizability interpretation. forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P. -Basic Arithmetics -~~~~~~~~~~~~~~~~~ +Basic Arithmetic +~~~~~~~~~~~~~~~~ The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and @@ -804,8 +802,8 @@ Notation Interpretation =============== =================== -Notations for integer arithmetics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Notations for integer arithmetic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. index:: single: Arithmetical notations @@ -822,7 +820,7 @@ Notations for integer arithmetics The following table describes the syntax of expressions -for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. +for integer arithmetic. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. @@ -866,7 +864,7 @@ Notations for real numbers This is provided by requiring and opening the module ``Reals`` and opening scope ``R_scope``. This set of notations is very similar to -the notation for integer arithmetics. The inverse function was added. +the notation for integer arithmetic. The inverse function was added. =============== =================== Notation Interpretation diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c93984661e..acf68e9fd2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2443,12 +2443,19 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement dedicated, efficient, rules to reduce the applications of these primitive operations. -These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to -types and functions of a :g:`Uint63` module. Said module is not produced by +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq. +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). + Bidirectionality hints ---------------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 38f6714f46..91dfa34494 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -44,78 +44,91 @@ Lexical conventions =================== Blanks - Space, newline and horizontal tabulation are considered as blanks. + Space, newline and horizontal tab are considered blanks. Blanks are ignored but they separate tokens. Comments - Comments in Coq are enclosed between ``(*`` and ``*)``, and can be nested. - They can contain any character. However, :token:`string` literals must be + Comments are enclosed between ``(*`` and ``*)``. They can be nested. + They can contain any character. However, embedded :token:`string` literals must be correctly closed. Comments are treated as blanks. -Identifiers and access identifiers +Identifiers and field identifiers Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and - ``'``, that do not start with a digit or ``'``. That is, they are - recognized by the following lexical class: + ``'``, that do not start with a digit or ``'``. That is, they are + recognized by the following grammar (except that the string ``_`` is reserved; + it is not a valid identifier): .. productionlist:: coq - first_letter : a..z ∣ A..Z ∣ _ ∣ unicode-letter - subsequent_letter : a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicode-letter ∣ unicode-id-part ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] - access_ident : .`ident` + field : .`ident` + first_letter : a..z ∣ A..Z ∣ _ ∣ `unicode_letter` + subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part` All characters are meaningful. In particular, identifiers are case-sensitive. - The entry ``unicode-letter`` non-exhaustively includes Latin, + :production:`unicode_letter` non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like - symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` + symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. - Access identifiers, written :token:`access_ident`, are identifiers prefixed by - `.` (dot) without blank. They are used in the syntax of qualified - identifiers. + Field identifiers, written :token:`field`, are identifiers prefixed by + `.` (dot) with no blank between the dot and the identifier. They are used in + the syntax of qualified identifiers. Numerals - Numerals are sequences of digits with a potential fractional part - and exponent. Integers are numerals without fractional nor exponent - part and optionally preceded by a minus sign. Underscores ``_`` can - be used as comments in numerals. + Numerals are sequences of digits with an optional fractional part + and exponent, optionally preceded by a minus sign. :token:`int` is an integer; + a numeral without fractional or exponent parts. :token:`num` is a non-negative + integer. Underscores embedded in the digits are ignored, for example + ``1_000_000`` is the same as ``1000000``. .. productionlist:: coq - digit : 0..9 + numeral : `num`[. `num`][`exp`[`sign`]`num`] + int : [-]`num` num : `digit`…`digit` - integer : [-]`num` - dot : . + digit : 0..9 exp : e | E sign : + | - - numeral : `num`[`dot` `num`][`exp`[`sign`]`num`] Strings - Strings are delimited by ``"`` (double quote), and enclose a sequence of - any characters different from ``"`` or the sequence ``""`` to denote the - double quote character. In grammars, the entry for quoted strings is - :production:`string`. + Strings begin and end with ``"`` (double quote). Use ``""`` to represent + a double quote character within a string. In the grammar, strings are + identified with :production:`string`. Keywords - The following identifiers are reserved keywords, and cannot be - employed otherwise:: - - _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod return - SProp Prop Set Type then using where with - -Special tokens - The following sequences of characters are special tokens:: - - ! % & && ( () ) * + ++ , - -> . .( .. - / /\ : :: :< := :> ; < <- <-> <: <= <> = - => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |- - || } ~ #[ - - Lexical ambiguities are resolved according to the “longest match” - rule: when a sequence of non alphanumerical characters can be - decomposed into several different ways, then the first token is the - longest possible one (among all tokens defined at this moment), and so - on. + The following character sequences are reserved keywords that cannot be + used as identifiers:: + + _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop + SProp Set Theorem Type Variable as at by cofix discriminated else + end exists exists2 fix for forall fun if in lazymatch let match + multimatch return then using where with + + Note that plugins may define additional keywords when they are loaded. + +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 basic library (see :ref:`thecoqlibrary`) and are normallly + loaded automatically at startup time. + + Here are the character sequences that Coq directly defines as tokens + without using :cmd:`Notation` (omitting 25 specialized tokens that begin with + ``#int63_``):: + + ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + . .( .. ... / : ::= := :> :>> ; < <+ <- <: + <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn + `( `{ { {| | |- || } + + When multiple tokens match the beginning of a sequence of characters, + the longest matching token is used. + Occasionally you may need to insert spaces to separate tokens. For example, + if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and + ``~~`` generate different tokens, whereas if `~~` is not defined, then the + two inputs are equivalent. .. _term: @@ -164,7 +177,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : ( `name` [: `term`] := `term` ) : ' `pattern` name : `ident` | _ - qualid : `ident` | `qualid` `access_ident` + qualid : `ident` | `qualid` `field` sort : SProp | Prop | Set | Type fix_bodies : `fix_body` : `fix_body` with `fix_body` with … with `fix_body` for `ident` diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index efb5df720a..7d6171285e 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -88,8 +88,6 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. -The "information" button is described in Section :ref:`try-tactics-automatically`. - The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. @@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -.. _try-tactics-automatically: - -Trying tactics automatically ------------------------------- - -The menu Try Tactics provides some features for automatically trying -to solve the current goal using simple tactics. If such a tactic -succeeds in solving the goal, then its text is automatically inserted -into the script. There is finally a combination of these tactics, -called the *proof wizard* which will try each of them in turn. This -wizard is also available as a tool button (the "information" button). The set of -tactics tried by the wizard is customizable in the preferences. - -These tactics are general ones, in particular they do not refer to -particular hypotheses. You may also try specific tactics related to -the goal or one of the hypotheses, by clicking with the right mouse -button on the goal or the considered hypothesis. This is the -“contextual menu on goals” feature, that may be disabled in the -preferences if undesirable. - - Proof folding ------------------ @@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -The `Tactics Wizard` section allows defining the set of tactics that -should be tried, in sequence, to solve the current goal. - -The last section is for miscellaneous boolean settings, such as the -“contextual menu on goals” feature presented in the section -:ref:`Try tactics automatically <try-tactics-automatically>`. - Notice that these settings are saved in the file `.coqiderc` of your home directory. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 46f9826e41..362c3da6cb 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -31,10 +31,10 @@ Syntax The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this -chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, +chapter: entries :token:`num`, :token:`int`, :token:`ident` :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` -represent respectively the natural and integer numbers, the authorized -identificators and qualified names, Coq terms and patterns and all the atomic +represent respectively natural and integer numbers, +identifiers, qualified names, Coq terms, patterns and the atomic tactics described in Chapter :ref:`tactics`. The syntax of :production:`cpattern` is @@ -141,10 +141,10 @@ mode but it can also be used in toplevel definitions as shown below. : `atom` atom : `qualid` : () - : `integer` + : `int` : ( `ltac_expr` ) component : `string` | `qualid` - message_token : `string` | `ident` | `integer` + message_token : `string` | `ident` | `int` tacarg : `qualid` : () : ltac : `atom` @@ -159,11 +159,11 @@ mode but it can also be used in toplevel definitions as shown below. match_rule : `cpattern` => `ltac_expr` : context [`ident`] [ `cpattern` ] => `ltac_expr` : _ => `ltac_expr` - test : `integer` = `integer` - : `integer` (< | <= | > | >=) `integer` + test : `int` = `int` + : `int` (< | <= | > | >=) `int` selector : [`ident`] - : `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `int` + : (`int` | `int` - `int`), ..., (`int` | `int` - `int`) toplevel_selector : `selector` : all : par diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3036648b08..ceaa2775bf 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `integer` + : `int` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -670,7 +670,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } + ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -719,7 +719,7 @@ The following scopes are built-in. + parses a Ltac2 expression at the next level and return it as is. -- :n:`tactic(n = @integer)`: +- :n:`tactic(n = @int)`: + parses a Ltac2 expression at the provided level :n:`n` and return it as is. @@ -760,7 +760,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..774732825a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b25104ddb9..46175e37ed 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 9f0a1942f9..eb86bab37e 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1020,6 +1020,37 @@ let apply_edit_file g edits = in List.rev (List.concat (List.map traverse prod)) + (* get the special tokens in the grammar *) +let print_special_tokens g = + let rec traverse set = function + | Sterm s -> + let c = s.[0] in + if (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') then set + else StringSet.add s set + | Snterm s -> set + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse set sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse (traverse set sym) sep + | Sparen sym_list -> traverse_prod set sym_list + | Sprod sym_list_list -> traverse_prods set sym_list_list + | Sedit _ + | Sedit2 _ -> set + and traverse_prod set prod = List.fold_left traverse set prod + and traverse_prods set prods = List.fold_left traverse_prod set prods + in + let spec_toks = List.fold_left (fun set b -> + let nt, prods = b in + traverse_prods set prods) + StringSet.empty (NTMap.bindings !g.map) + in + Printf.printf "Special tokens:"; + StringSet.iter (fun t -> Printf.printf " %s" t) spec_toks; + Printf.printf "\n\n" + (* get the transitive closure of a non-terminal excluding "stops" symbols. Preserve ordering to the extent possible *) (* todo: at the moment, the code doesn't use the ordering; consider switching to using @@ -1099,8 +1130,9 @@ let print_chunks g out fmt () = (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) -let start_symbols = ["vernac_toplevel"; "tactic_mode"] -let tokens = [ "BULLET"; "FIELD"; "IDENT"; "NUMERAL"; "STRING" ] (* don't report as undefined *) +let start_symbols = ["vernac_toplevel"] +(* don't report tokens as undefined *) +let tokens = [ "bullet"; "field"; "ident"; "int"; "num"; "numeral"; "string" ] let report_bad_nts g file = let rec get_nts refd defd bindings = @@ -1468,6 +1500,8 @@ let process_grammar args = print_in_order out g `MLG !g.order StringSet.empty; close_out out; finish_with_file (dir "fullGrammar") args.verify; + if args.verbose then + print_special_tokens g; if not args.fullGrammar then begin (* do shared edits *) diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 54a592a04d..6bcf3b438f 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -7,7 +7,6 @@ ; (gtk_accel_path "<Actions>/Templates/Template Program Lemma" "") (gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Primary>l") ; (gtk_accel_path "<Actions>/Templates/Template Fact" "") -(gtk_accel_path "<Actions>/Tactics/auto" "<Primary><Control>a") ; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "") ; (gtk_accel_path "<Actions>/Help/About Coq" "") ; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") @@ -19,7 +18,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "") ; (gtk_accel_path "<Actions>/Templates/Template Write State" "") ; (gtk_accel_path "<Actions>/Export/Export to" "") -(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk") ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "") ; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "") ; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c") @@ -50,7 +48,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic left" "") (gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u") -(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Primary><Control>ampersand") ; (gtk_accel_path "<Actions>/Templates/Template Infix" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "") @@ -149,7 +146,6 @@ (gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Primary>t") ; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion--clear" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic unfold" "") -; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic red in" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <- -- in" "") ; (gtk_accel_path "<Actions>/Templates/Template Hint Extern" "") @@ -187,7 +183,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "") ; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "") -(gtk_accel_path "<Actions>/Tactics/Wizard" "<Primary><Control>dollar") ; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "") ; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "") ; (gtk_accel_path "<Actions>/File/Revert all buffers" "") @@ -228,7 +223,6 @@ ; (gtk_accel_path "<Actions>/Export/Html" "") ; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "") -(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i") ; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "") ; (gtk_accel_path "<Actions>/Queries/Queries" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "") @@ -289,7 +283,6 @@ ; (gtk_accel_path "<Actions>/Templates/Template Add Field" "") ; (gtk_accel_path "<Actions>/Templates/Template Require Export" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "") -(gtk_accel_path "<Actions>/Tactics/omega" "<Primary><Control>o") ; (gtk_accel_path "<Actions>/Tactics/Tactic split" "") ; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q") (gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e") @@ -328,7 +321,6 @@ ; (gtk_accel_path "<Actions>/Edit/Edit" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "") ; (gtk_accel_path "<Actions>/Templates/Template C" "") -(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s") ; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template A" "") ; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "") @@ -360,13 +352,11 @@ ; (gtk_accel_path "<Actions>/File/File" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "") -(gtk_accel_path "<Actions>/Tactics/trivial" "<Primary><Control>v") ; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "") ; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "") -(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e") ; (gtk_accel_path "<Actions>/File/Open" "<Primary>o") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "") ; (gtk_accel_path "<Actions>/Templates/Template Hint" "") diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 566654218d..d52f038f1f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -137,7 +137,6 @@ class type ops = object method go_to_insert : unit task method go_to_mark : GText.mark -> unit task - method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task @@ -806,48 +805,6 @@ object(self) else Coq.seq (self#backtrack_to_iter ~move_insert:false point) (Coq.lift (fun () -> Sentence.tag_on_insert buffer))) - method tactic_wizard l = - let insert_phrase phrase tag = - let stop = self#get_start_of_input in - let phrase' = if stop#starts_line then phrase else "\n"^phrase in - buffer#insert ~iter:stop phrase'; - Sentence.tag_on_insert buffer; - let start = self#get_start_of_input in - buffer#move_mark ~where:stop (`NAME "start_of_input"); - buffer#apply_tag tag ~start ~stop; - if self#get_insert#compare stop <= 0 then - buffer#place_cursor ~where:stop; - let sentence = - mk_sentence - ~start:(`MARK (buffer#create_mark start)) - ~stop:(`MARK (buffer#create_mark stop)) - [] in - Doc.push document sentence; - messages#default_route#clear; - self#show_goals - in - let display_error (loc, s) = - messages#default_route#add (Ideutils.validate s) in - let try_phrase phrase stop more = - let action = log "Sending to coq now" in - let route_id = 0 in - let query = Coq.query (route_id,(phrase,Stateid.dummy)) in - let next = function - | Fail (_, l, str) -> (* FIXME: check *) - display_error (l, str); - messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase)); - more - | Good () -> stop Tags.Script.processed - in - Coq.bind (Coq.seq action query) next - in - let rec loop l = match l with - | [] -> Coq.return () - | p :: l' -> - try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l') - in - loop l - method handle_reset_initial = let action () = (* clear the stack *) diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 83ad8c15dc..1e8d87bb15 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -15,7 +15,6 @@ class type ops = object method go_to_insert : unit task method go_to_mark : GText.mark -> unit task - method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task diff --git a/ide/coqide.ml b/ide/coqide.ml index 8d95dcee27..2c9f116cc3 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -603,9 +603,6 @@ module Nav = struct let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document) end -let tactic_wizard_callback l _ = - send_to_coq (fun sn -> sn.coqops#tactic_wizard l) - let printopts_callback opts v = let b = v#get_active in let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in @@ -1106,25 +1103,8 @@ let build_ui () = ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); ] end; - let tacitem s sc = - item s ~label:("_"^s) - ~accel:(modifier_for_tactics#get^sc) - ~callback:(tactic_wizard_callback [s]) - in menu tactics_menu [ - item "Try Tactics" ~label:"_Try Tactics"; - item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO - ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar") - ~callback:(tactic_wizard_callback automatic_tactics#get); - tacitem "auto" "a"; - tacitem "auto with *" "asterisk"; - tacitem "eauto" "e"; - tacitem "eauto with *" "ampersand"; - tacitem "intuition" "i"; - tacitem "omega" "o"; - tacitem "simpl" "s"; - tacitem "tauto" "p"; - tacitem "trivial" "v"; + item "Tactics" ~label:"_Tactics"; ]; alpha_items tactics_menu "Tactic" Coq_commands.tactics; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index d4a339f4f5..452808490d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -100,18 +100,7 @@ let init () = \n <menuitem action='Previous' />\ \n <menuitem action='Next' />\ \n </menu>\ -\n <menu action='Try Tactics'>\ -\n <menuitem action='auto' />\ -\n <menuitem action='auto with *' />\ -\n <menuitem action='eauto' />\ -\n <menuitem action='eauto with *' />\ -\n <menuitem action='intuition' />\ -\n <menuitem action='omega' />\ -\n <menuitem action='simpl' />\ -\n <menuitem action='tauto' />\ -\n <menuitem action='trivial' />\ -\n <menuitem action='Wizard' />\ -\n <separator />\ +\n <menu action='Tactics'>\ \n %s\ \n </menu>\ \n <menu action='Templates'>\ @@ -173,7 +162,6 @@ let init () = \n <toolitem action='Interrupt' />\ \n <toolitem action='Previous' />\ \n <toolitem action='Next' />\ -\n <toolitem action='Wizard' />\ \n</toolbar>\ \n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") diff --git a/ide/preferences.ml b/ide/preferences.ml index ea0495bb19..bf9fe8922a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -938,16 +938,6 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in -(* - let automatic_tactics = - strings - ~f:automatic_tactics#set - ~add:(fun () -> ["<edit me>"]) - "Wizard tactics to try in order" - automatic_tactics#get - - in -*) let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in @@ -1008,10 +998,6 @@ let configure ?(apply=(fun () -> ())) parent = Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse]); -(* - Section("Tactics Wizard", None, - [automatic_tactics]); -*) Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation; diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 93632da110..5542716af2 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -37,6 +37,8 @@ val mul : t -> t -> t val div : t -> t -> t val rem : t -> t -> t +val diveucl : t -> t -> t * t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t @@ -57,3 +59,13 @@ val head0 : t -> t val tail0 : t -> t val is_uint63 : Obj.t -> bool + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +val addc : t -> t -> t carry +val addcarryc : t -> t -> t carry +val subc : t -> t -> t carry +val subcarryc : t -> t -> t carry diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml index 20b2f58496..d6b077a9f5 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_amd64_63.ml @@ -82,6 +82,8 @@ let div (x : int) (y : int) = let rem (x : int) (y : int) = if y = 0 then 0 else Int64.to_int (Int64.rem (to_uint64 x) (to_uint64 y)) +let diveucl x y = (div x y, rem x y) + let addmuldiv p x y = l_or (l_sl x p) (l_sr y (uint_size - p)) @@ -225,3 +227,24 @@ let tail0 x = let is_uint63 t = Obj.is_int t [@@ocaml.inline always] + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = x + y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = x + y + 1 in + if le r x then C1 r else C0 r + +let subc x y = + let r = x - y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = x - y - 1 in + if lt y x then C0 r else C1 r diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml index c3279779e1..2a3fc75ec1 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_i386_31.ml @@ -83,6 +83,8 @@ let div x y = let rem x y = if y = 0L then 0L else Int64.rem x y +let diveucl x y = (div x y, rem x y) + let addmuldiv p x y = l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) @@ -191,6 +193,27 @@ let is_uint63 t = Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag && le (Obj.magic t) maxuint63 +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = add x y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = addcarry x y in + if le r x then C1 r else C0 r + +let subc x y = + let r = sub x y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = subcarry x y in + if lt y x then C0 r else C1 r + (* Register all exported functions so that they can be called from C code *) let () = diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v new file mode 100644 index 0000000000..a2ee602313 --- /dev/null +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extraction to OCaml of native 63-bit machine integers. *) + +From Coq Require Int63 Extraction. + +(** Basic data types used by some primitive operators. *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. +Extract Inductive comparison => int [ "0" "(-1)" "1" ]. +Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ]. + +(** Primitive types and operators. *) +Extract Constant Int63.int => "Uint63.t". +Extraction Inline Int63.int. +(* Otherwise, the name conflicts with the primitive OCaml type [int] *) + +Extract Constant Int63.lsl => "Uint63.l_sl". +Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Int63.land => "Uint63.l_and". +Extract Constant Int63.lor => "Uint63.l_or". +Extract Constant Int63.lxor => "Uint63.l_xor". + +Extract Constant Int63.add => "Uint63.add". +Extract Constant Int63.sub => "Uint63.sub". +Extract Constant Int63.mul => "Uint63.mul". +Extract Constant Int63.mulc => "Uint63.mulc". +Extract Constant Int63.div => "Uint63.div". +Extract Constant Int63.mod => "Uint63.rem". + +Extract Constant Int63.eqb => "Uint63.equal". +Extract Constant Int63.ltb => "Uint63.lt". +Extract Constant Int63.leb => "Uint63.le". + +Extract Constant Int63.addc => "Uint63.addc". +Extract Constant Int63.addcarryc => "Uint63.addcarryc". +Extract Constant Int63.subc => "Uint63.subc". +Extract Constant Int63.subcarryc => "Uint63.subcarryc". + +Extract Constant Int63.diveucl => "Uint63.diveucl". +Extract Constant Int63.diveucl_21 => "Uint63.div21". +Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". + +Extract Constant Int63.compare => "Uint63.compare". + +Extract Constant Int63.head0 => "Uint63.head0". +Extract Constant Int63.tail0 => "Uint63.tail0". diff --git a/stm/stm.ml b/stm/stm.ml index d5e6e6fd8b..69dbebbc57 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1073,7 +1073,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = *) let is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in @@ -1216,8 +1216,6 @@ end = struct (* {{{ *) match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid - | VernacBackTo id -> - Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8750a64ccc..5af576dad2 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -193,7 +193,7 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBackTo _ | VernacRestart -> VtMeta + | VernacRestart -> VtMeta (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff ([], VtNow) diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 9bb16b97e2..c81ba02230 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -812,14 +812,6 @@ Proof. eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. Qed. -Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. -Proof. - apply to_Z_inj. - rewrite -> add_spec, !lsl_spec, add_spec. - rewrite -> Zmult_mod_idemp_l, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. -Qed. - (* LSL *) Lemma lsl0 i: 0 << i = 0%int63. Proof. @@ -1119,7 +1111,7 @@ Proof. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, - <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr. + <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsl_add_distr. rewrite (bit_split (x lor y)), lor_spec. intros Heq. assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 5ed60b0a0f..2428fc495d 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -178,7 +178,7 @@ Proof. change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0. Qed. -Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. +Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. @@ -186,12 +186,16 @@ Proof. ring. Qed. -Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. +#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4. + +Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. now rewrite sin_shift, cos_neg, cos_PI4. Qed. +#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4. + Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. Proof with trivial. apply Rsqr_inj... diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e49b1c0c07..2673995a86 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -383,7 +383,7 @@ let rec vernac_loop ~state = try let input = top_buffer.tokens in match read_sentence ~state input with - | Some (VernacBacktrack(bid,_,_)) -> + | Some (VernacBackTo bid) -> let bid = Stateid.of_int bid in let doc, res = Stm.edit_at ~doc:state.doc bid in assert (res = `NewTip); diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index fed337ab03..1a1537113e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -17,7 +17,7 @@ open Vernacexpr (* Vernaculars specific to the toplevel *) type vernac_toplevel = - | VernacBacktrack of int * int * int + | VernacBackTo of int | VernacDrop | VernacQuit | VernacControl of vernac_control @@ -54,8 +54,8 @@ GRAMMAR EXTEND Gram vernac_toplevel: FIRST [ [ IDENT "Drop"; "." -> { Some VernacDrop } | IDENT "Quit"; "." -> { Some VernacQuit } - | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> - { Some (VernacBacktrack (n,m,p)) } + | IDENT "BackTo"; n = natural; "." -> + { Some (VernacBackTo n) } (* show a goal for the specified proof state *) | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 65db4401d9..664010c917 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -80,9 +80,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - let minductive_message = function | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (Id.print x ++ str " is defined") @@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite - (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 97f930c0a1..285be8cd51 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -10,7 +10,6 @@ open Names open Entries -open Libnames open Vernacexpr open Constrexpr @@ -33,12 +32,20 @@ val do_mutual_inductive -> Declarations.recursivity_kind -> unit +(** User-interface API *) + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : Names.inductive -> string list list + (************************************************************************) -(** Internal API *) +(** Internal API, exported for Record *) (************************************************************************) -(** Exported for Record and Funind *) - (** Registering a mutual inductive definition together with its associated schemes *) @@ -55,41 +62,3 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) - -(** Exported for Funind *) - -(** Extracting the semantical components out of the raw syntax of mutual - inductive declarations *) - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_arity : constr_expr; - ind_lc : (Id.t * constr_expr) list -} - -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - -val extract_mutual_inductive_declaration_components : - (one_inductive_expr * decl_notation list) list -> - structured_inductive_expr * (*coercions:*) qualid list * decl_notation list - -(** Typing mutual inductive definitions *) -val interp_mutual_inductive - : template:bool option - -> universe_decl_expr option - -> structured_inductive_expr - -> decl_notation list - -> cumulative:bool - -> poly:bool - -> private_ind:bool - -> Declarations.recursivity_kind - -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list - -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - a known inductive type. *) - -val make_cases : Names.inductive -> string list list diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 15f9e0328c..ad5d98669d 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1141,7 +1141,6 @@ GRAMMAR EXTEND Gram | IDENT "Reset"; id = identref -> { VernacResetName id } | IDENT "Back" -> { VernacBack 1 } | IDENT "Back"; n = natural -> { VernacBack n } - | IDENT "BackTo"; n = natural -> { VernacBackTo n } (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e25118e0a8..0eb0b1b6f6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -669,8 +669,6 @@ let string_of_definition_object_kind = let open Decls in function return ( if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i ) - | VernacBackTo i -> - return (keyword "BackTo" ++ pr_intarg i) (* State management *) | VernacWriteState s -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c048c7d83..9af8d8b67c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2298,7 +2298,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacAbort _ -> anomaly (str "type_vernac") (* Syntax *) @@ -2630,7 +2629,6 @@ and interp_expr ?proof ~atts ~st c = | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 6f09d9a39b..0968632c2d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -359,7 +359,6 @@ type nonrec vernac_expr = | VernacResetName of lident | VernacResetInitial | VernacBack of int - | VernacBackTo of int (* Commands *) | VernacCreateHintDb of string * bool diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 1dd8164ebc..747998c6cc 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -32,7 +32,6 @@ let rec has_Fail v = v |> CAst.with_val (function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBackTo _ | VernacBack _ -> true | _ -> false |