diff options
115 files changed, 1609 insertions, 215 deletions
diff --git a/.travis.yml b/.travis.yml index 81f50af0a0..270bdcaede 100644 --- a/.travis.yml +++ b/.travis.yml @@ -27,6 +27,8 @@ env: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" + - TEST_TARGET="ci-bedrock-src" + - TEST_TARGET="ci-bedrock-facade" - TEST_TARGET="ci-color" - TEST_TARGET="ci-compcert" - TEST_TARGET="ci-coquelicot" @@ -34,6 +36,7 @@ env: - TEST_TARGET="ci-fiat-crypto" - TEST_TARGET="ci-fiat-parsers" - TEST_TARGET="ci-flocq" + - TEST_TARGET="ci-formal-topology" - TEST_TARGET="ci-hott" - TEST_TARGET="ci-iris-coq" - TEST_TARGET="ci-math-classes" @@ -52,7 +52,8 @@ FIND_VCS_CLAUSE:='(' \ -name '.bzr' -o \ -name 'debian' -o \ -name "$${GIT_DIR}" -o \ - -name '_build' \ + -name '_build' -o \ + -name '_build_ci' \ ')' -prune -o define find diff --git a/Makefile.ci b/Makefile.ci index b055ada8e5..0136852180 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,11 +1,10 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ - ci-unimath ci-vst + ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade ci-formal-topology .PHONY: $(CI_TARGETS) # Generic rule, we use make to easy travis integraton with mixed rules $(CI_TARGETS): ci-%: ./dev/ci/ci-$*.sh - diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 27f79e7963..9ccaaa7cbb 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -530,7 +530,7 @@ let check_positivity env_ar mind params nrecp inds = let check_inductive env kn mib = Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) - let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in + let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 336ce9d8f1..1dfade261f 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -95,6 +95,24 @@ : ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} ######################################################################## +# bedrock_src +######################################################################## +: ${bedrock_src_CI_BRANCH:=master} +: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git} + +######################################################################## +# bedrock_facade +######################################################################## +: ${bedrock_facade_CI_BRANCH:=master} +: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git} + +######################################################################## +# formal-topology +######################################################################## +: ${formal_topology_CI_BRANCH:=ci} +: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} + +######################################################################## # CoLoR ######################################################################## : ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} @@ -109,4 +127,3 @@ ######################################################################## : ${tlc_CI_BRANCH:=master} : ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} - diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh new file mode 100755 index 0000000000..95cfa3073f --- /dev/null +++ b/dev/ci/ci-bedrock-facade.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade + +git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR} + +( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade ) diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh new file mode 100755 index 0000000000..532611d4b3 --- /dev/null +++ b/dev/ci/ci-bedrock-src.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src + +git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR} + +( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 93d39aab07..c6df45a1d4 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -7,4 +7,4 @@ fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} -( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} ) +( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} lite ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index c62aa1d859..d8460bc70c 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} -( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh new file mode 100755 index 0000000000..ecb36349fb --- /dev/null +++ b/dev/ci/ci-formal-topology.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes + +Corn_CI_DIR=${CI_BUILD_DIR}/corn + +formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology + +# Setup Math-Classes + +git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} + +( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup Corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup formal-topology + +git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} + +( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md new file mode 100644 index 0000000000..2ff82c6888 --- /dev/null +++ b/dev/doc/xml-protocol.md @@ -0,0 +1,745 @@ +#Coq XML Protocol for Coq 8.6# + +This document is based on documentation originally written by CJ Bell +for his [vscoq](https://github.com/siegebell/vscoq/) project. + +Here, the aim is to provide a "hands on" description of the XML +protocol that coqtop and IDEs use to communicate. The protocol first appeared +with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming +versions of Proof General. + +A somewhat out-of-date description of the async state machine is +[documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). +OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). + +# CHANGES +## Changes from 8.5: + * In several places, flat text wrapped in <string> tags now appears as structured text inside <richpp> tags + * The "errormsg" feedback has been replaced by a "message" feedback which contains + <feedback\_content> tag, with a message_level attribute of "error" + +* [Commands](#commands) + - [About](#command-about) + - [Add](#command-add) + - [EditAt](#command-editAt) + - [Init](#command-init) + - [Goal](#command-goal) + - [Status](#command-status) + - [Query](#command-query) + - [Evars](#command-evars) + - [Hints](#command-hints) + - [Search](#command-search) + - [GetOptions](#command-getoptions) + - [SetOptions](#command-setoptions) + - [MkCases](#command-mkcases) + - [StopWorker](#command-stopworker) + - [PrintAst](#command-printast) + - [Annotate](#command-annotate) +* [Feedback messages](#feedback) + - [Added Axiom](#feedback-addedaxiom) + - [Processing](#feedback-processing) + - [Processed](#feedback-processed) + - [Incomplete](#feedback-incomplete) + - [Complete](#feedback-complete) + - [GlobRef](#feedback-globref) + - [Error](#feedback-error) + - [InProgress](#feedback-inprogress) + - [WorkerStatus](#feedback-workerstatus) + - [File Dependencies](#feedback-filedependencies) + - [File Loaded](#feedback-fileloaded) + - [Message](#feedback-message) + - [Custom](#feedback-custom) + +Sentences: each command sent to Coqtop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF). +Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity." +In practice, the command sentences sent to Coqtop are terminated at the "." and start with any previous whitespace. +Each sentence is assigned a unique stateId after being sent to Coq (via Add). +States: + * Processing: has been received by Coq and has no obvious syntax error (that would prevent future parsing) + * Processed: + * InProgress: + * Incomplete: the validity of the sentence cannot be checked due to a prior error + * Complete: + * Error: the sentence has an error + +State ID 0 is reserved as a 'dummy' state. + +-------------------------- + +## <a name="commands">Commands</a> + +### <a name="command-about">**About(unit)**</a> +Returns information about the protocol and build dates for Coqtop. +``` +<call val="About"> + <unit/> +</call> +``` +#### *Returns* +```html + <value val="good"> + <coq_info><string>8.6</string> + <string>20150913</string> + <string>December 2016</string> + <string>Dec 23 2016 16:16:30</string> + </coq_info> +</value> +``` +The string fields are the Coq version, the protocol version, the release date, and the compile time of Coqtop. +The protocol version is a date in YYYYMMDD format, where "20150913" corresponds to Coq 8.6. An IDE that wishes +to support multiple Coq versions can use the protocol version information to know how to handle output from Coqtop. + +### <a name="command-add">**Add(stateId: integer, command: string, verbose: boolean)**</a> +Adds a toplevel command (e.g. vernacular, definition, tactic) to the given state. +`verbose` controls whether out-of-band messages will be generated for the added command (e.g. "foo is assumed" in response to adding "Axiom foo: nat."). +```html +<call val="Add"> + <pair> + <pair> + <string>${command}</string> + <int>${editId}</int> + </pair> + <pair> + <state_id val="${stateId}"/> + <bool val="${verbose}"/> + </pair> + </pair> +</call> +``` + +#### *Returns* +* The added command is given a fresh `stateId` and becomes the next "tip". +```html +<value val="good"> + <pair> + <state_id val="${newStateId}"/> + <pair> + <union val="in_l"><unit/></union> + <string>${message}</string> + </pair> + </pair> +</value> +``` +* When closing a focused proof (in the middle of a bunch of interpreted commands), +the `Qed` will be assigned a prior `stateId` and `nextStateId` will be the id of an already-interpreted +state that should become the next tip. +```html +<value val="good"> + <pair> + <state_id val="${stateId}"/> + <pair> + <union val="in_r"><state_id val="${nextStateId}"/></union> + <string>${message}</string> + </pair> + </pair> +</value> +``` +* Failure: + - Syntax error. Error offsets are byte offsets (not character offsets) with respect to the start of the sentence, starting at 0. + ```html + <value val="fail" + loc_s="${startOffsetOfError}" + loc_e="${endOffsetOfError}"> + <state_id val="${stateId}"/> + <richpp>${errorMessage}</richpp> + </value> + ``` + - Another kind of error, for example, Qed with a pending goal. + ```html + <value val="fail"><state_id val="${stateId}"/><richpp>${errorMessage}</richpp></value> + ``` + +------------------------------- + +### <a name="command-editAt">**EditAt(stateId: integer)**</a> +Moves current tip to `${stateId}`, such that commands may be added to the new state ID. +```html +<call val="Edit_at"><state_id val="${stateId}"/></call> +``` +#### *Returns* +* Simple backtrack; focused stateId becomes the parent state +```html +<value val="good"> + <union val="in_l"><unit/></union> +</value> +``` + +* New focus; focusedQedStateId is the closing Qed of the new focus; senteneces between the two should be cleared +```html +<value val="good"> + <union val="in_r"> + <pair> + <state_id val="${focusedStateId}"/> + <pair> + <state_id val="${focusedQedStateId}"/> + <state_id val="${oldFocusedStateId}"/> + </pair> + </pair> + </union> +</value> +``` +* Failure: If `stateId` is in an error-state and cannot be jumped to, `errorFreeStateId` is the parent state of ``stateId` that shopuld be edited instead. +```html +<value val="fail" loc_s="${startOffsetOfError}" loc_e="${endOffsetOfError}"> + <state_id val="${errorFreeStateId}"/> + ${errorMessage} +</value> +``` + +------------------------------- + +### <a name="command-init">**Init()**</a> +* No options. +```html +<call val="Init"><option val="none"/></call> +``` +* With options. Looking at + [ide_slave.ml](https://github.com/coq/coq/blob/c5d0aa889fa80404f6c291000938e443d6200e5b/ide/ide_slave.ml#L355), + it seems that `options` is just the name of a script file, whose path + is added via `Add LoadPath` to the initial state. +```html +<call val="Init"> + <option val="some"> + <string>${options}</string> + </option> +</call> +``` +Providing the script file enables Coq to use .aux files created during +compilation. Those file contain timing information that allow Coq to +choose smartly between asynchronous and synchronous processing of +proofs. + +#### *Returns* +* The initial stateId (not associated with a sentence) +```html +<value val="good"> + <state_id val="${initialStateId}"/> +</value> +``` + +------------------------------- + + +### <a name="command-goal">**Goal()**</a> +```html +<call val="Goal"><unit/></call> +``` +#### *Returns* +* If there is a goal. `shelvedGoals` and `abandonedGoals` have the same structure as the first set of (current/foreground) goals. `backgroundGoals` contains a list of pairs of lists of goals (list ((list Goal)*(list Goal))); it represents a "focus stack" ([see code for reference](https://github.com/coq/coq/blob/trunk/engine/proofview.ml#L113)). Each time a proof is focused, it will add a new pair of lists-of-goals. The first pair is the most nested set of background goals, the last pair is the top level set of background goals. The first list in the pair is in reverse order. Each time you focus the goal (e.g. using `Focus` or a bullet), a new pair will be prefixed to the list. +```html +<value val="good"> + <option val="some"> + <goals> + <!-- current goals --> + <list> + <goal> + <string>3</string> + <list> + <richpp>${hyp1}</richpp> + ... + <richpp>${hypN}</richpp> + </list> + <richpp>${goal}</richpp> + </goal> + ... + ${goalN} + </list> + <!-- `backgroundGoals` --> + <list> + <pair> + <list><goal />...</list> + <list><goal />...</list> + </pair> + ... + </list> + ${shelvedGoals} + ${abandonedGoals} + </goals> + </option> +</value> +``` + +For example, this script: +```coq +Goal P -> (1=1/\2=2) /\ (3=3 /\ (4=4 /\ 5=5) /\ 6=6) /\ 7=7. +intros. +split; split. (* current visible goals are [1=1, 2=2, 3=3/\(4=4/\5=5)/\6=6, 7=7] *) +Focus 3. (* focus on 3=3/\(4=4/\5=5)/\6=6; bg-before: [1=1, 2=2], bg-after: [7=7] *) +split; [ | split ]. (* current visible goals are [3=3, 4=4/\5=5, 6=6] *) +Focus 2. (* focus on 4=4/\5=5; bg-before: [3=3], bg-after: [6=6] *) +* (* focus again on 4=4/\5=5; bg-before: [], bg-after: [] *) +split. (* current visible goals are [4=4,5=5] *) +``` +should generate the following goals structure: +``` +goals: [ P|-4=4, P|-5=5 ] +background: +[ + ( [], [] ), (* bullet with one goal has no before or after background goals *) + ( [ P|-3=3 ], [ P|-6=6 ] ), (* Focus 2 *) + ( [ P|-2=2, P|-1=1 ], [ P|-7=7 ] ) (* Focus 3; notice that 1=1 and 2=2 are reversed *) +] +``` +Pseudocode for listing all of the goals in order: `rev (flat_map fst background) ++ goals ++ flat_map snd background`. + +* No goal: +```html +<value val="good"><option val="none"/></value> +``` + +------------------------------- + + +### <a name="command-status">**Status(force: bool)**</a> +CoqIDE typically sets `force` to `false`. +```html +<call val="Status"><bool val="${force}"/></call> +``` +#### *Returns* +* +```html +<status> + <string>${path}</string> + <string>${proofName}</string> + <string>${allProofs}</string> + <string>${proofNumber}</string> +</status> +``` + +------------------------------- + + +### <a name="command-query">**Query(query: string, stateId: integer)**</a> +In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state. +```html +<call val="Query"> + <pair> + <string>${query}</string> + <state_id val="${stateId}"/> + </pair> +</call> +``` +#### *Returns* +* +```html +<value val="good"> + <string>${message}</string> +</value> +``` +------------------------------- + + + +### <a name="command-evars">**Evars()**</a> +```html +<call val="Evars"><unit/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <option val="some"> + <list> + <evar>${evar1}</evar> + ... + <evar>${evarN}</evar> + </list> + </option> +</value> +``` + +------------------------------- + + +### <a name="command-hints">**Hints()**</a> +```html +<call val="Hints"><unit/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <option val="some"> + <pair> + <list/> + <list> + <pair> + <string>${hint1}</string> + <string>${hint2}</string> + </pair> + ... + <pair> + <string>${hintN-1}</string> + <string>${hintN}</string> + </pair> + </list> + </pair> + </option> +</value> +``` + +------------------------------- + + +### <a name="command-search">**Search([(constraintTypeN: string, constraintValueN: string, positiveConstraintN: boolean)])**</a> +Searches for objects that satisfy a list of constraints. If `${positiveConstraint}` is `false`, then the constraint is inverted. +```html +<call val="Search"> + <list> + <pair> + <search_cst val="${constraintType1}"> + ${constraintValue1} + </search_cst> + <bool val="${positiveConstraint1}"/> + </pair> + ... + <!-- Example: --> + <pair> + <search_cst val="name_pattern"> + <string>bool_rect</string> + </search_cst> + <bool val="true"/> + </pair> + </list> +</call> +``` +#### *Returns* +* +```html +<value val="good"> + <list> + <coq_object> + <list> + <string>${metaInfo}</string> + ... + </list> + <list> + <string>${name}</string> + </list> + <string>${definition}</string> + </coq_object> + ... + </list> +</value> +``` +##### Types of constraints: +* Name pattern: `${constraintType} = "name_pattern"`; `${constraintValue}` is a regular expression string. +* Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. +* SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. +* In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure. +* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*. + +------------------------------- + + +### <a name="command-getoptions">**GetOptions()**</a> +```html +<call val="GetOptions"><unit/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <list> + <pair> + <list><string>${string1}</string>...</list> + <option_state> + <bool>${sync}</bool> + <bool>${deprecated}</bool> + <string>${name}</string> + ${option_value} + </option_state> + </pair> + ... + </list> +</value> +``` + +------------------------------- + + +### <a name="command-setoptions">**SetOptions(options)**</a> +Sends a list of option settings, where each setting roughly looks like: +`([optionNamePart1, ..., optionNamePartN], value)`. +```html +<call val="SetOptions"> + <list> + <pair> + <list> + <string>optionNamePart1</string> + ... + <string>optionNamePartN</string> + </list> + <option_value val="${typeOfOption}"> + <option val="some"> + ${value} + </option> + </option_value> + </pair> + ... + <!-- Example: --> + <pair> + <list> + <string>Printing</string> + <string>Width</string> + </list> + <option_value val="intvalue"> + <option val="some"><int>60</int></option> + </option_value> + </pair> + </list> +</call> +``` +CoqIDE sends the following settings (defaults in parentheses): +``` +Printing Width : (<option_value val="intvalue"><int>60</int></option_value>), +Printing Coercions : (<option_value val="boolvalue"><bool val="false"/></option_value>), +Printing Matching : (...true...) +Printing Notations : (...true...) +Printing Existential Instances : (...false...) +Printing Implicit : (...false...) +Printing All : (...false...) +Printing Universes : (...false...) +``` +#### *Returns* +* +```html +<value val="good"><unit/></value> +``` + +------------------------------- + + +### <a name="command-mkcases">**MkCases(...)**</a> +```html +<call val="MkCases"><string>...</string></call> +``` +#### *Returns* +* +```html +<value val="good"> + <list> + <list><string>${string1}</string>...</list> + ... + </list> +</value> +``` + +------------------------------- + + +### <a name="command-stopworker">**StopWorker(worker: string)**</a> +```html +<call val="StopWorker"><string>${worker}</string></call> +``` +#### *Returns* +* +```html +<value val="good"><unit/></value> +``` + +------------------------------- + + +### <a name="command-printast">**PrintAst(stateId: integer)**</a> +```html +<call val="PrintAst"><state_id val="${stateId}"/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <gallina begin="${gallina_begin}" end="${gallina_end}"> + <theorem begin="${theorem_begin}" end="${theorem_end}" type="Theorem" name="${theorem_name}"> + <apply begin="${apply_begin}" end="${apply_end}"> + <operator begin="${operator_begin}" end="${operator_end}" name="${operator_name}"/> + <typed begin="${typed_begin}" end="${typed_end}"> + <constant begin="${constant_begin}" end="${constant_end}" name="${constant_name}"/> + ... + <token begin="${token_begin}" end="token_end">${token}</token> + ... + </typed> + ... + </apply> + </theorem> + ... + </gallina> +</value> +``` + +------------------------------- + + + +### <a name="command-annotate">**Annotate(annotation: string)**</a> +```html +<call val="Annotate"><string>${annotation}</string></call> +``` +#### *Returns* +* + +take `<call val="Annotate"><string>Theorem plus_0_r : forall n : nat, n + 0 = n.</string></call>` as an example. + +```html +<value val="good"> + <pp startpos="0" endpos="45"> + <vernac_expr startpos="0" endpos="44"> + <keyword startpos="0" endpos="7">Theorem</keyword> + plus_0_r : + <constr_expr startpos="19" endpos="44"> + <keyword startpos="19" endpos="25">forall</keyword> + n : + <constr_expr startpos="30" endpos="33">nat</constr_expr> + , + <unparsing startpos="35" endpos="44"> + <unparsing startpos="35" endpos="40"> + <unparsing startpos="35" endpos="40"> + <unparsing startpos="35" endpos="36"> + <constr_expr startpos="35" endpos="36">n</constr_expr> + </unparsing> + <unparsing startpos="36" endpos="38"> +</unparsing> + <unparsing startpos="38" endpos="39"> </unparsing> + <unparsing startpos="39" endpos="40"> + <constr_expr startpos="39" endpos="40">0</constr_expr> + </unparsing> + </unparsing> + </unparsing> + <unparsing startpos="40" endpos="42"> =</unparsing> + <unparsing startpos="42" endpos="43"> </unparsing> + <unparsing startpos="43" endpos="44"> + <constr_expr startpos="43" endpos="44">n</constr_expr> + </unparsing> + </unparsing> + </constr_expr> + </vernac_expr> + . + </pp> +</value> +``` + +------------------------------- + +## <a name="feedback">Feedback messages</a> + +Feedback messages are issued out-of-band, + giving updates on the current state of sentences/stateIds, + worker-thread status, etc. + +In the descriptions of feedback syntax below, wherever a `state_id` +tag may occur, there may instead be an `edit_id` tag. + +* <a name="feedback-addedaxiom">Added Axiom</a>: in response to `Axiom`, `admit`, `Admitted`, etc. +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="addedaxiom" /> +</feedback> +``` +* <a name="feedback-processing">Processing</a> +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="processingin"> + <string>${workerName}</string> + </feedback_content> +</feedback> +``` +* <a name="feedback-processed">Processed</a> +```html +<feedback object="state" route="0"> + <feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="processed"/> +</feedback> +``` +* <a name="feedback-incomplete">Incomplete</a> +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="incomplete" /> +</feedback> +``` +* <a name="feedback-complete">Complete</a> +* <a name="feedback-globref">GlobRef</a> +* <a name="feedback-error">Error</a>. Issued, for example, when a processed tactic has failed or is unknown. +The error offsets may both be 0 if there is no particular syntax involved. +* <a name="feedback-inprogress">InProgress</a> +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="inprogress"> + <int>1</int> + </feedback_content> +</feedback> +``` +* <a name="feedback-workerstatus">WorkerStatus</a> +Ex: `workername = "proofworker:0"` +Ex: `status = "Idle"` or `status = "proof: myLemmaName"` or `status = "Dead"` +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="workerstatus"> + <pair> + <string>${workerName}</string> + <string>${status}</string> + </pair> + </feedback_content> +</feedback> +``` +* <a name="feedback-filedependencies">File Dependencies</a>. Typically in response to a `Require`. Dependencies are *.vo files. + - State `stateId` directly depends on `dependency`: + ```html + <feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="filedependency"> + <option val="none"/> + <string>${dependency}</string> + </feedback_content> + </feedback> + ``` + - State `stateId` depends on `dependency` via dependency `sourceDependency` + ```xml + <feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="filedependency"> + <option val="some"><string>${sourceDependency}</string></option> + <string>${dependency}</string> + </feedback_content> + </feedback> + ``` +* <a name="feedback-fileloaded">File Loaded</a>. For state `stateId`, module `module` is being loaded from `voFileName` +```xml +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="fileloaded"> + <string>${module}</string> + <string>${voFileName`}</string> + </feedback_content> +</feedback> +``` + +* <a name="feedback-message">Message</a>. `level` is one of `{info,warning,notice,error,debug}`. For example, in response to an <a href="#command-add">add</a> `"Axiom foo: nat."` with `verbose=true`, message `foo is assumed` will be emitted in response. +```xml +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="message"> + <message> + <message_level val="${level}"/> + <string>${message}</string> + </message> + </feedback_content> +</feedback> +``` + +* <a name="feedback-custom">Custom</a>. A feedback message that Coq plugins can use to return structured results, including results from Ltac profiling. Optionally, `startPos` and `stopPos` define a range of offsets in the document that the message refers to; otherwise, they will be 0. `customTag` is intended as a unique string that identifies what kind of payload is contained in `customXML`. +```xml +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="custom"> + <loc start="${startPos}" stop="${stopPos}"/> + <string>${customTag}</string> + ${customXML} + </feedback_content> +</feedback> +``` + diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd6..a25da7d926 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -697,8 +697,8 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivalent to the command line option {\tt -Q {\dirpath} - {\str}}. It adds the physical directory {\str} to the current {\Coq} +This command is equivalent to the command line option {\tt -Q {\str} + {\dirpath}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. \begin{Variants} @@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory \end{Variants} \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command is equivalent to the command line option {\tt -R {\dirpath} - {\str}}. It adds the physical directory {\str} and all its +This command is equivalent to the command line option {\tt -R {\str} + {\dirpath}}. It adds the physical directory {\str} and all its subdirectories to the current {\Coq} loadpath. \begin{Variants} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c37367de5b..4c333379bd 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom. \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof} \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt - exact {\term}; Save.} That is, you have to give the full proof in + exact {\term}. Qed.} That is, you have to give the full proof in one gulp, as a proof term (see Section~\ref{exact}). \variant {\tt Proof.} diff --git a/engine/proofview.ml b/engine/proofview.ml index c01879765b..2e6266cf15 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -828,14 +828,12 @@ let tclPROGRESS t = let quick_test = initial.solution == final.solution && initial.comb == final.comb in - let exhaustive_test = + let test = + quick_test || Util.List.for_all2eq begin fun i f -> Progress.goal_equal initial.solution i final.solution f end initial.comb final.comb in - let test = - quick_test || exhaustive_test - in if not test then tclUNIT res else diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dd8a48b85e..74504e36d4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -274,17 +274,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = - (* pboutill: There are letins in pat which is incompatible with notations and - not explicit application. *) - match pat with - | PatCstr(loc,cstrsp,args,na) - when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> - let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in - let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) - | _ -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in match availability_of_prim_token p sc scopes with | None -> raise No_match @@ -293,7 +284,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na with No_match -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> @@ -307,16 +298,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = if !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = - match projs with - | [] -> acc - | None :: q -> ip q args acc - | Some c :: q -> - match args with - | [] -> raise No_match - | CPatAtom(_, None) :: tail -> ip q tail acc - (* we don't want to have 'x = _' in our patterns *) - | head :: tail -> ip q tail - ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, CPatAtom(_, None) -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + ((extern_reference loc Id.Set.empty (ConstRef c), pat) :: acc) + | _ -> raise No_match in + ip q tail acc + | _ -> assert false in CPatRecord(loc, List.rev (ip projs args [])) with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c916fcd886..8400fdc967 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -432,31 +432,6 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let rec free_vars_of_pat il = - function - | CPatCstr (loc, c, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in - List.fold_left free_vars_of_pat il l2 - | CPatAtom (loc, ro) -> - begin match ro with - | Some (Ident (loc, i)) -> (loc, i) :: il - | Some _ | None -> il - end - | CPatNotation (loc, n, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (fst l1) in - List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) - | _ -> anomaly (str "free_vars_of_pat") - -let intern_local_pattern intern lvar env p = - List.fold_left - (fun env (loc, i) -> - let bk = Default Implicit in - let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in - let n = Name i in - let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in - env) - env (free_vars_of_pat [] p) - type binder_data = | BDRawDef of (Loc.t * glob_binder) | BDPattern of @@ -490,13 +465,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | Some ty -> ty | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) in - let env = intern_local_pattern intern lvar env p in - let cp = + let il,cp = match !intern_cases_pattern_fwd (None,env.scopes) p with - | (_, [(_, cp)]) -> cp + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err_loc (loc,"",str "Unsupported nested \"as\" clause."); + il,cp | _ -> assert false in - let il = List.map snd (free_vars_of_pat [] p) in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl) let intern_generalization intern env lvar loc bk ak c = @@ -947,17 +924,6 @@ let find_remaining_scopes pl1 pl2 ref = in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs), simple_adjust_scopes len_pl2 (aux (impl_list,scope_list))) -let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 - -let product_of_cases_patterns ids idspl = - List.fold_right (fun (ids,pl) (ids',ptaill) -> - (ids @ ids', - (* Cartesian prod of the or-pats for the nth arg and the tail args *) - List.flatten ( - List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) - idspl (ids,[Id.Map.empty,[]]) - (* @return the first variable that occurs twice in a pattern naive n^2 algo *) @@ -994,6 +960,45 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr))) +open Term +open Declarations + +(* Similar to Cases.adjust_local_defs but on RCPat *) +let insert_local_defs_in_pattern (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | Context.Rel.Declaration.LocalDef _ :: decls, args -> Constrexpr.RCPatAtom (Loc.ghost,None) :: aux decls args + | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) + | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) l + +let add_local_defs_and_check_length loc env g pl args = match g with + | ConstructRef cstr -> + (* We consider that no variables corresponding to local binders + have been given in the "explicit" arguments, which come from a + "@C args" notation or from a custom user notation *) + let pl' = insert_local_defs_in_pattern cstr pl in + let maxargs = Inductiveops.constructor_nalldecls cstr in + if List.length pl' + List.length args > maxargs then + error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr); + (* Two possibilities: either the args are given with explict + variables for local definitions, then we give the explicit args + extended with local defs, so that there is nothing more to be + added later on; or the args are not enough to have all arguments, + which a priori means local defs to add in the [args] part, so we + postpone the insertion of local defs in the explicit args *) + (* Note: further checks done later by check_constructor_length *) + if List.length pl' + List.length args = maxargs then pl' else pl + | _ -> pl + let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st @@ -1212,6 +1217,17 @@ let alias_of als = match als.alias_ids with *) +let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 + +let product_of_cases_patterns aliases idspl = + List.fold_right (fun (ids,pl) (ids',ptaill) -> + (ids @ ids', + (* Cartesian prod of the or-pats for the nth arg and the tail args *) + List.flatten ( + List.map (fun (subst,p) -> + List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) + idspl (aliases.alias_ids,[aliases.alias_map,[]]) + let rec subst_pat_iterator y t p = match p with | RCPatAtom (_,id) -> begin match id with Some x when Id.equal x y -> t | _ -> p end @@ -1221,7 +1237,7 @@ let rec subst_pat_iterator y t p = match p with | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a) | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl) -let drop_notations_pattern looked_for = +let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) let ensure_kind top loc g = @@ -1350,9 +1366,9 @@ let drop_notations_pattern looked_for = | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - RCPatCstr (loc, g, - List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ - List.map (in_pat false scopes) args, []) + let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in + let pl = add_local_defs_and_check_length loc genv g pl args in + RCPatCstr (loc, g, pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1376,7 +1392,7 @@ let drop_notations_pattern looked_for = let rec intern_pat genv aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in - let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in + let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in @@ -1445,7 +1461,7 @@ and check_no_patcast_subst (pl,pll) = let intern_cases_pattern genv scopes aliases pat = check_no_patcast pat; intern_pat genv aliases - (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) + (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := @@ -1455,7 +1471,7 @@ let intern_ind_pattern genv scopes pat = check_no_patcast pat; let no_not = try - drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat + drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc in match no_not with @@ -1466,7 +1482,7 @@ let intern_ind_pattern genv scopes pat = let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in (with_letin, - match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type loc) | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x) @@ -1796,7 +1812,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = and intern_multiple_pattern env n (loc,pl) = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in check_number_of_pattern loc n pl; - product_of_cases_patterns [] idsl_pll + product_of_cases_patterns empty_alias idsl_pll (* Expands a disjunction of multiple pattern *) and intern_disjunctive_multiple_pattern env loc n mpl = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0c5393cf41..5648821539 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1158,6 +1158,7 @@ let match_notation_constr u c (metas,pat) = metas ([],[],[]) (* Matching cases pattern *) + let add_patterns_for_params ind l = let mib,_ = Global.lookup_inductive ind in let nparams = mib.Declarations.mind_nparams in @@ -1190,10 +1191,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - sigma,(0,add_patterns_for_params (fst r1) largs) + let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + sigma,(0,l) | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = add_patterns_for_params (fst r1) args1 in + let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0bbe4bb4cb..a380443fe3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -291,7 +291,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) let sub = Int.Map.bindings sub in - List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) + List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type)) end_of_type_with_pop sub in @@ -1388,8 +1388,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly (Pp.str "No tcc proof !!") - | Some lemma -> + | Undefined -> anomaly (Pp.str "No tcc proof !!") + | Value lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) @@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls - + | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> @@ -1586,8 +1586,9 @@ let prove_principle_for_gen let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> error "No tcc proof !!" - | Some lemma -> lemma + | Undefined -> error "No tcc proof !!" + | Value lemma -> lemma + | Not_needed -> Coqlib.build_coq_I () in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 34ce669672..e11cd9eac6 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -9,7 +9,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) - constr option ref -> (* a pointer to the obligation proofs lemma *) + Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) types -> (* the type of the recursive argument *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f56e92414e..8419f1d8f2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -506,3 +506,9 @@ let list_rewrite (rev:bool) (eqs: (constr*bool) list) = (List.fold_right (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i) (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; + + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index e5c756f564..83cadf5f5a 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -114,3 +114,10 @@ val acc_rel : Term.constr Util.delayed val well_founded : Term.constr Util.delayed val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic + + + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fa84e4ddf3..7ff31f1127 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -41,7 +41,7 @@ open Eauto open Indfun_common open Sigma.Notations open Context.Rel.Declaration - + (* Ugly things which should not be here *) @@ -1296,7 +1296,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in - ref_ := Some lemma ; + ref_ := Value lemma ; let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in @@ -1412,6 +1412,7 @@ let com_terminate (new_goal_type); with Failure "empty list of subgoals!" -> (* a non recursive function declared with measure ! *) + tcc_lemma_ref := Not_needed; defined () @@ -1484,7 +1485,6 @@ let (com_eqn : int -> Id.t -> (* Pp.msgnl (str "eqn finished"); *) );; - let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let env = Global.env() in @@ -1524,7 +1524,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in - let tcc_lemma_constr = ref None in + let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index f60eedbe6e..c84c736b85 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -13,7 +13,7 @@ bool -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> int -> Constrexpr.constr_expr -> (Term.pconstant -> - Term.constr option ref -> + Indfun_common.tcc_lemma_value ref -> Term.pconstant -> Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e3076a..cefd48538a 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -666,6 +666,36 @@ let clever_rewrite p vpath t gl = let t' = applist(t, (vargs @ [abstracted])) in exact (applist(t',[mkNewMeta()])) gl +(** simpl_coeffs : + The subterm at location [path_init] in the current goal should + look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce + via "simpl" each [ci] and the final constant [k]. + The path [path_k] gives the location of constant [k]. + Earlier, the whole was a mere call to [focused_simpl], + leading to reduction inside the atoms [vi], which is bad, + for instance when the atom is an evaluable definition + (see #4132). *) + +let simpl_coeffs path_init path_k gl = + let rec loop n t = + if Int.equal n 0 then pf_nf gl t + else + (* t should be of the form ((v * c) + ...) *) + match kind_of_term t with + | App(f,[|t1;t2|]) -> + (match kind_of_term t1 with + | App (g,[|v;c|]) -> + let c' = pf_nf gl c in + let t2' = loop (pred n) t2 in + mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) + | _ -> assert false) + | _ -> assert false + in + let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let newc = context (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) + in + Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl + let rec shuffle p (t1,t2) = match t1,t2 with | Oplus(l1,r1), Oplus(l2,r2) -> @@ -728,7 +758,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -763,7 +793,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -786,7 +816,7 @@ let shuffle_mult_right p_init e1 k2 e2 = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -813,7 +843,7 @@ let shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -854,7 +884,7 @@ let rec scalar p n = function let scalar_norm p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | (_::l) -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; @@ -865,7 +895,7 @@ let scalar_norm p_init = let norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _:: l -> clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: @@ -875,7 +905,7 @@ let norm_add p_init = let scalar_norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _ :: l -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 886a982634..daac33f503 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -80,31 +80,70 @@ let add_binders na1 na2 binding_vars (names, terms as subst) = let rec build_lambda vars ctx m = match vars with | [] -> - let len = List.length ctx in - lift (-1 * len) m + if Vars.closed0 m then m else raise PatternMatchingFailure | n :: vars -> (* change [ x1 ... xn y z1 ... zm |- t ] into [ x1 ... xn z1 ... zm |- lam y. t ] *) - let len = List.length ctx in - let init i = - if i < pred n then mkRel (i + 2) - else if Int.equal i (pred n) then mkRel 1 - else mkRel (i + 1) - in - let m = substl (List.init len init) m in let pre, suf = List.chop (pred n) ctx in - match suf with + let (na, t, suf) = match suf with | [] -> assert false - | (_, na, t) :: suf -> - let map i = if i > n then pred i else i in - let vars = List.map map vars in - (** Check that the abstraction is legal *) - let frels = free_rels t in - let brels = List.fold_right Int.Set.add vars Int.Set.empty in - let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in - (** Create the abstraction *) - let m = mkLambda (na, t, m) in - build_lambda vars (pre @ suf) m + | (_, na, t) :: suf -> (na, t, suf) + in + (** Check that the abstraction is legal by generating a transitive closure of + its dependencies. *) + let is_nondep t clear = match clear with + | [] -> true + | _ -> + let rels = free_rels t in + let check i b = b || not (Int.Set.mem i rels) in + List.for_all_i check 1 clear + in + let fold (_, _, t) clear = is_nondep t clear :: clear in + (** Produce a list of booleans: true iff we keep the hypothesis *) + let clear = List.fold_right fold pre [false] in + let clear = List.drop_last clear in + (** If the conclusion depends on a variable we cleared, failure *) + let () = if not (is_nondep m clear) then raise PatternMatchingFailure in + (** Create the abstracted term *) + let fold (k, accu) keep = + if keep then + let k = succ k in + (k, Some k :: accu) + else (k, None :: accu) + in + let keep, shift = List.fold_left fold (0, []) clear in + let shift = List.rev shift in + let map = function + | None -> mkProp (** dummy term *) + | Some i -> mkRel (i + 1) + in + (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *) + let subst = + List.map map shift @ + mkRel 1 :: + List.mapi (fun i _ -> mkRel (i + keep + 2)) suf + in + let map i (id, na, c) = + let i = succ i in + let subst = List.skipn i subst in + let subst = List.map (fun c -> Vars.lift (- i) c) subst in + (id, na, substl subst c) + in + let pre = List.mapi map pre in + let pre = List.filter_with clear pre in + let m = substl subst m in + let map i = + if i > n then i - n + keep + else match List.nth shift (i - 1) with + | None -> + (** We cleared a variable that we wanted to abstract! *) + raise PatternMatchingFailure + | Some k -> k + in + let vars = List.map map vars in + (** Create the abstraction *) + let m = mkLambda (na, Vars.lift keep t, m) in + build_lambda vars (pre @ suf) m let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu @@ -307,6 +346,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when c1 = c2 -> + Array.fold_left2 (sorec ctx env) subst args1 args2 + | _ -> raise PatternMatchingFailure in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818f4..0eda776519 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -559,12 +559,45 @@ let rec cases_pattern_of_glob_constr na = function PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found +open Declarations +open Term +open Context + +(* Keep only patterns which are not bound to a local definitions *) +let drop_local_defs typi args = + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | [], [] -> [] + | Rel.Declaration.LocalDef _ :: decls, pat :: args -> + begin + match pat with + | PatVar (_,Anonymous) -> aux decls args + | _ -> raise Not_found (* The pattern is used, one cannot drop it *) + end + | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) args + +let add_patterns_for_params_remove_local_defs (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + let l = + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in + drop_local_defs typi l in + Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l + (* Turn a closed cases pattern into a glob_constr *) let rec glob_constr_of_closed_cases_pattern_aux = function | PatCstr (loc,cstr,[],Anonymous) -> GRef (loc,ConstructRef cstr,None) | PatCstr (loc,cstr,l,Anonymous) -> let ref = GRef (loc,ConstructRef cstr,None) in + let l = add_patterns_for_params_remove_local_defs cstr l in GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533f..6b8f131f41 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -76,3 +76,5 @@ val map_pattern : (glob_constr -> glob_constr) -> val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr + +val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 2090aad8a0..79e9c727d7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,7 +160,9 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in @@ -358,9 +360,9 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = + let mkGLambda na c = GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0a90e0dbd3..beed9e36b7 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -661,7 +661,8 @@ let evar_of_binder holes = function | NamedHyp s -> evar_with_name holes s | AnonHyp n -> try - let h = List.nth holes (pred n) in + let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in + let h = List.nth nondeps (pred n) in h.hole_evar with e when CErrors.noncritical e -> errorlabstrm "" (str "No such binder.") diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a37..58a86a4aa5 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -219,8 +219,8 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow - | VernacError _ -> assert false + | VernacWriteState _ + | VernacError _ -> VtUnknown, VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d1ae85e7be..2c911addf5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -593,6 +593,7 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = + not only_classes || let open Context.Named.Declaration in try let t = Global.lookup_named (get_id hyp) |> get_type in (* Section variable, reindex only if the type changed *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1a45217a4a..e39159fb82 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -89,6 +89,11 @@ let get_coq_eq ctx = with Not_found -> error "eq not found." +let univ_of_eq env eq = + match kind_of_term (Retyping.get_type_of env Evd.empty eq) with + | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false) + | _ -> assert false + (**********************************************************************) (* Check if an inductive type [ind] has the form *) (* *) @@ -744,7 +749,7 @@ let build_congr env (eq,refl,ctx) ind = let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -752,6 +757,7 @@ let build_congr env (eq,refl,ctx) ind = let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt (mkNamedLambda varB (mkSort (Type uni)) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 66da9ee182..b3655d3735 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -487,6 +487,7 @@ module New = struct let check_evars env sigma extsigma origsigma = let rec is_undefined_up_to_restriction sigma evk = + if Evd.mem origsigma evk then None else let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) @@ -500,7 +501,7 @@ module New = struct let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with - | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc + | Some (evk',evi) -> (evk',evi)::acc | _ -> acc) extsigma [] in diff --git a/test-suite/Makefile b/test-suite/Makefile index c10cd4ed44..e87e133768 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -44,7 +44,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1))))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v index 7d0dc090e1..36ab7ff599 100644 --- a/test-suite/bugs/closed/3080.v +++ b/test-suite/bugs/closed/3080.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) Delimit Scope type_scope with type. Delimit Scope function_scope with function. diff --git a/test-suite/bugs/closed/3323.v b/test-suite/bugs/closed/3323.v index 22b1603b60..4622634eaa 100644 --- a/test-suite/bugs/closed/3323.v +++ b/test-suite/bugs/closed/3323.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 297 lines to 117 lines, then from 95 lines to 79 lines, then from 82 lines to 68 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3332.v b/test-suite/bugs/closed/3332.v index d86470cdee..a3564bfcce 100644 --- a/test-suite/bugs/closed/3332.v +++ b/test-suite/bugs/closed/3332.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-time") -*- *) +(* -*- coq-prog-args: ("-time") -*- *) Definition foo : True. Proof. Abort. (* Toplevel input, characters 15-21: diff --git a/test-suite/bugs/closed/3346.v b/test-suite/bugs/closed/3346.v index 638404f2cb..09bd789345 100644 --- a/test-suite/bugs/closed/3346.v +++ b/test-suite/bugs/closed/3346.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Monomorphic Inductive paths (A : Type) (a : A) : A -> Type := idpath : paths A a a. (* This should fail with -indices-matter *) Fail Check paths nat O O : Prop. diff --git a/test-suite/bugs/closed/3348.v b/test-suite/bugs/closed/3348.v index d9ac09d8d3..904de68964 100644 --- a/test-suite/bugs/closed/3348.v +++ b/test-suite/bugs/closed/3348.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Set Printing Universes. Inductive Empty : Set := . diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index f8113e4c78..555accfd51 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -20,7 +20,7 @@ while it is expected to have type "IsHProp (* Top.17 *) Empty" Defined. Module B. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v index d7ce02ea87..1e0c8e61f4 100644 --- a/test-suite/bugs/closed/3375.v +++ b/test-suite/bugs/closed/3375.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *) +(* -*- mode: coq; coq-prog-args: ("-impredicative-set") -*- *) (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v index f7ab5f76a5..ae8e41e29e 100644 --- a/test-suite/bugs/closed/3393.v +++ b/test-suite/bugs/closed/3393.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *) Set Universe Polymorphism. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v index 374a53928d..9a57ca7703 100644 --- a/test-suite/bugs/closed/3427.v +++ b/test-suite/bugs/closed/3427.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *) Generalizable All Variables. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v index d258bb31f8..b0c4b23702 100644 --- a/test-suite/bugs/closed/3539.v +++ b/test-suite/bugs/closed/3539.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *) (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0 coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *) diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index a547685070..90182a4881 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *) (* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index fc4c171e2c..367d380ec3 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index a327bbf2a9..bb6af6a66c 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *) (* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v index c19a2d4a06..66dee702aa 100644 --- a/test-suite/bugs/closed/3956.v +++ b/test-suite/bugs/closed/3956.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter"); mode: visual-line -*- *) Set Universe Polymorphism. Set Primitive Projections. Close Scope nat_scope. diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index e4d76732a3..fc1c504f14 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index d34a2b8b1b..a8bf950ff2 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -1,5 +1,5 @@ Unset Strict Universe Declaration. -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *) (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v new file mode 100644 index 0000000000..806ffb771f --- /dev/null +++ b/test-suite/bugs/closed/4132.v @@ -0,0 +1,31 @@ + +Require Import ZArith Omega. +Open Scope Z_scope. + +(** bug 4132: omega was using "simpl" either on whole equations, or on + delimited but wrong spots. This was leading to unexpected reductions + when one atom (here [b]) is an evaluable reference instead of a variable. *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +Qed. + +Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "index out of bounds" in the past, + but I never managed to reproduce that in any version, + even before my fix. *) +Qed. + +Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "Failure(occurence 2)" in the past, + but I never managed to reproduce that. *) +Qed. diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v new file mode 100644 index 0000000000..4aef5bb95e --- /dev/null +++ b/test-suite/bugs/closed/4306.v @@ -0,0 +1,32 @@ +Require Import List. +Require Import Arith. +Require Import Recdef. +Require Import Omega. + +Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + match xys with + | (nil, _) => snd xys + | (_, nil) => fst xys + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', y :: ys') + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (x :: xs', ys') + end + end. +Proof. + intros; simpl; omega. + intros; simpl; omega. + intros; simpl; omega. +Qed. + +Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + let (xs, ys) := xys in + match (xs, ys) with + | (nil, _) => ys + | (_, nil) => xs + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', ys) + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (xs, ys') + end + end.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v index 60c9354597..1ad81345db 100644 --- a/test-suite/bugs/closed/4394.v +++ b/test-suite/bugs/closed/4394.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Require Import Equality List. Inductive Foo (I : Type -> Type) (A : Type) : Type := diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v index 5c23f8404b..a89cf0cbc3 100644 --- a/test-suite/bugs/closed/4400.v +++ b/test-suite/bugs/closed/4400.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. Set Printing Universes. Inductive Foo (I : Type -> Type) (A : Type) : Type := diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v index a32acf789c..56a7b4f6e9 100644 --- a/test-suite/bugs/closed/4456.v +++ b/test-suite/bugs/closed/4456.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) (* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) (* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 coqtop version 8.5beta3 (November 2015) *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 08628377f0..4fab9d44f3 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1199 lines to 430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, then from 269 lines to 255 lines *) diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index ae17fb145d..ccef1c3040 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) (* File reduced by coq-bug-finder from original input, then from 1125 lines to 346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, then from 285 lines to 271 lines *) diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index da140c9318..82f1e3fe73 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v index c89a86d634..a59eed2c86 100644 --- a/test-suite/bugs/closed/4656.v +++ b/test-suite/bugs/closed/4656.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal True. constructor 1. Qed. diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v index 1ae5081851..10e48db6dd 100644 --- a/test-suite/bugs/closed/4673.v +++ b/test-suite/bugs/closed/4673.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) (* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 coqtop version 8.5 (February 2016) *) Axiom proof_admitted : False. diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v index f047624c84..2d41828f19 100644 --- a/test-suite/bugs/closed/4722.v +++ b/test-suite/bugs/closed/4722.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *) +(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *) diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v index 3854bbffdd..cfb4548d2c 100644 --- a/test-suite/bugs/closed/4727.v +++ b/test-suite/bugs/closed/4727.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0), (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) -> o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v index a6ebda61cf..a90abd71cf 100644 --- a/test-suite/bugs/closed/4733.v +++ b/test-suite/bugs/closed/4733.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) Require Import Coq.Lists.List. Require Import Coq.Vectors.Vector. diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v index d87906f313..33a1d1a50b 100644 --- a/test-suite/bugs/closed/4769.v +++ b/test-suite/bugs/closed/4769.v @@ -1,5 +1,5 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) (* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3 coqtop version trunk (June 2016) *) diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v index 4cec43184c..71a51c6312 100644 --- a/test-suite/bugs/closed/4780.v +++ b/test-suite/bugs/closed/4780.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *) (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 coqtop version 8.5pl1 (April 2016) *) diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v index 9d65840acd..bbb34f465c 100644 --- a/test-suite/bugs/closed/4785_compat_85.v +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +(* -*- coq-prog-args: ("-compat" "8.5") -*- *) Require Coq.Lists.List Coq.Vectors.Vector. Require Coq.Compat.Coq85. diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v index a914962629..fe6e65a0f0 100644 --- a/test-suite/bugs/closed/4811.v +++ b/test-suite/bugs/closed/4811.v @@ -2,7 +2,7 @@ (* Submitted by Jason Gross *) -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) (* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 coqtop version 8.5pl1 (April 2016) *) diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v index 904abb2287..e411ce62f0 100644 --- a/test-suite/bugs/closed/4818.v +++ b/test-suite/bugs/closed/4818.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Prob" "-top" "Product") -*- *) (* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) (* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 coqtop version 8.5pl1 (June 2016) *) diff --git a/test-suite/bugs/closed/5193.v b/test-suite/bugs/closed/5193.v new file mode 100644 index 0000000000..cc8739afe6 --- /dev/null +++ b/test-suite/bugs/closed/5193.v @@ -0,0 +1,14 @@ +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Typeclasses eauto := debug. +Set Typeclasses Debug Verbosity 2. + +Inductive Finx(n : nat) : Set := +| Fx1(i : nat)(e : n = S i) +| FxS(i : nat)(f : Finx i)(e : n = S i). + +Context `{Finx_eqdec : forall n, Eqdec (Finx n)}. + +Goal {x : Type & Eqdec x}. + eexists. + try typeclasses eauto 1 with typeclass_instances. diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v index 7254afb429..72722f5f6d 100644 --- a/test-suite/bugs/closed/5198.v +++ b/test-suite/bugs/closed/5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from diff --git a/test-suite/bugs/closed/5300.v b/test-suite/bugs/closed/5300.v new file mode 100644 index 0000000000..18202df508 --- /dev/null +++ b/test-suite/bugs/closed/5300.v @@ -0,0 +1,39 @@ +Module Test1. + + Module Type Foo. + Parameter t : unit. + End Foo. + + Module Bar : Foo. + Module Type Rnd. Definition t' : unit := tt. End Rnd. + Module Rnd_inst : Rnd. Definition t' : unit := tt. End Rnd_inst. + Definition t : unit. + exact Rnd_inst.t'. + Qed. + End Bar. + + Print Assumptions Bar.t. +End Test1. + +Module Test2. + Module Type Foo. + Parameter t1 : unit. + Parameter t2 : unit. + End Foo. + + Module Bar : Foo. + Inductive ind := . + Definition t' : unit := tt. + Definition t1 : unit. + Proof. + exact ((fun (_ : ind -> False) => tt) (fun H => match H with end)). + Qed. + Definition t2 : unit. + Proof. + exact t'. + Qed. + End Bar. + + Print Assumptions Bar.t1. + Print Assumptions Bar.t1. +End Test2. diff --git a/test-suite/bugs/closed/5377.v b/test-suite/bugs/closed/5377.v new file mode 100644 index 0000000000..130d9f9abf --- /dev/null +++ b/test-suite/bugs/closed/5377.v @@ -0,0 +1,54 @@ +Goal ((forall (t : Type) (x y : t), + True -> + x = y)) -> False. +Proof. + intro HG. + let P := lazymatch goal with + | [ H : forall t x y, True -> @?P t x y + |- _ ] + => P + end in + pose (f := P). + unify f (fun (t : Type) (x y : t) => x = y). +Abort. + +Goal True. +Proof. +let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with + | fun _ y _ => @?C y => C + end in +pose (f := c). +unify f (fun n : nat => n). +Abort. + +Goal (forall x : nat, x = x -> x = x \/ x = x) -> True. +Proof. +intro. +let P := lazymatch goal with +| [ H : forall y, @?P y -> @?P y \/ _ |- _ ] + => P +end in +pose (f := P). +unify f (fun x : nat => x = x). +Abort. + +Goal (forall x : nat, x = x -> x = x \/ x = x) -> True. +Proof. +intro. +lazymatch goal with +| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ] + => idtac +end. +Abort. + +Axiom eq : forall {T} (_ : T), Prop. + +Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop. +Proof. +intro. +let P := lazymatch goal with +| [ H : forall t _ x, @?P t x |- _ ] + => P +end in +pose (f := P). +Abort. diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v new file mode 100644 index 0000000000..fce671c754 --- /dev/null +++ b/test-suite/bugs/closed/5469.v @@ -0,0 +1,3 @@ +(* Some problems with the special treatment of curly braces *) + +Reserved Notation "'a' { x }" (at level 0, format "'a' { x }"). diff --git a/test-suite/bugs/closed/5470.v b/test-suite/bugs/closed/5470.v new file mode 100644 index 0000000000..5b3984b6df --- /dev/null +++ b/test-suite/bugs/closed/5470.v @@ -0,0 +1,3 @@ +(* This used to raise an anomaly *) + +Fail Reserved Notation "x +++ y" (at level 70, x binder). diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v new file mode 100644 index 0000000000..390133162f --- /dev/null +++ b/test-suite/bugs/closed/5486.v @@ -0,0 +1,15 @@ +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k : + forall _ : T, Fm), + @eq Fm + (k + match p return T with + | pair p0 swap => fst p0 + end) f. + intros. + (* next statement failed in Bug 5486 *) + match goal with + | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ] + => pose (let (a, b) := d in e a b) as t0 + end. diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v new file mode 100644 index 0000000000..9b995f4503 --- /dev/null +++ b/test-suite/bugs/closed/5487.v @@ -0,0 +1,9 @@ +(* Was a collision between an ltac pattern variable and an evar *) + +Goal forall n, exists m, n = m :> nat. +Proof. + eexists. + Fail match goal with + | [ |- ?x = ?y ] + => match x with y => idtac end + end. diff --git a/test-suite/bugs/closed/5522.v b/test-suite/bugs/closed/5522.v new file mode 100644 index 0000000000..0fae9ede42 --- /dev/null +++ b/test-suite/bugs/closed/5522.v @@ -0,0 +1,7 @@ +(* Checking support for scope delimiters and as clauses in 'pat + applied to notations with binders *) + +Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. ) + (at level 200, x binder, y binder, f at level 200). + +Check multifun '((x, y)%core as z) in (x+y,0)=z. diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v new file mode 100644 index 0000000000..88f219be30 --- /dev/null +++ b/test-suite/bugs/closed/5526.v @@ -0,0 +1,3 @@ +Fail Notation "x === x" := (eq_refl x) (at level 10). +Reserved Notation "x === x" (only printing, at level 10). +Notation "x === x" := (eq_refl x) (only printing). diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v new file mode 100644 index 0000000000..bb1222489a --- /dev/null +++ b/test-suite/bugs/closed/5550.v @@ -0,0 +1,10 @@ +Section foo. + + Variable bar : Prop. + Variable H : bar. + + Goal bar. + typeclasses eauto with foobar. + Qed. + +End foo. diff --git a/test-suite/bugs/closed/HoTT_coq_012.v b/test-suite/bugs/closed/HoTT_coq_012.v index a3c697f8ca..420aaf9745 100644 --- a/test-suite/bugs/closed/HoTT_coq_012.v +++ b/test-suite/bugs/closed/HoTT_coq_012.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Definition UU := Type. Inductive toto (B : UU) : UU := c (x : B). diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 3f5d7b0215..39a7103d1b 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *) +(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v index e2bf1dbedb..263dec4857 100644 --- a/test-suite/bugs/closed/HoTT_coq_053.v +++ b/test-suite/bugs/closed/HoTT_coq_053.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Printing Universes. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v index c687965937..635024e983 100644 --- a/test-suite/bugs/closed/HoTT_coq_054.v +++ b/test-suite/bugs/closed/HoTT_coq_054.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) Inductive Empty : Prop := . Inductive paths {A : Type} (a : A) : A -> Type := diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v index a250987714..561b7e557d 100644 --- a/test-suite/bugs/closed/HoTT_coq_055.v +++ b/test-suite/bugs/closed/HoTT_coq_055.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Inductive Empty : Prop := . diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v index 9c7e394dc3..2e6c735cf5 100644 --- a/test-suite/bugs/closed/HoTT_coq_059.v +++ b/test-suite/bugs/closed/HoTT_coq_059.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x. diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index 90d1d18306..e01f73f1b3 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) Set Universe Polymorphism. Definition admit {T} : T. diff --git a/test-suite/bugs/closed/HoTT_coq_097.v b/test-suite/bugs/closed/HoTT_coq_097.v index 38e8007b6c..f2b2e57b9c 100644 --- a/test-suite/bugs/closed/HoTT_coq_097.v +++ b/test-suite/bugs/closed/HoTT_coq_097.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Set Printing Universes. Inductive Empty : Set := . diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index 7c1ab8dc2c..fa4072a8f6 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v index b6c0da76ba..ea4bcd8b45 100644 --- a/test-suite/bugs/closed/HoTT_coq_108.v +++ b/test-suite/bugs/closed/HoTT_coq_108.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *) (* File reduced by coq-bug-finder from 139 lines to 124 lines. *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index 6ee6e65323..cd9cad4064 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") *) (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *) Set Universe Polymorphism. Set Asymmetric Patterns. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v index 4530548b8f..4541f13d01 100644 --- a/test-suite/bugs/opened/4803.v +++ b/test-suite/bugs/opened/4803.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) Require Import Coq.Lists.List. Require Import Coq.Vectors.Vector. diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v index 6611db70e2..1e9e919797 100644 --- a/test-suite/output-modulo-time/ltacprof.v +++ b/test-suite/output-modulo-time/ltacprof.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *) +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) Ltac sleep' := do 100 (do 100 (do 100 idtac)). Ltac sleep := sleep'. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 50131470eb..3dad6271af 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 8ce6f9795c..f064dfe763 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -2,18 +2,18 @@ t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with - | @k _ x0 => f x0 (F x0) + | k _ x0 => f x0 (F x0) end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t Argument scopes are [function_scope function_scope _] = fun d : TT => match d with - | @CTT _ _ b => b + | {| f3 := b |} => b end : TT -> 0 = 0 = fun d : TT => match d with - | @CTT _ _ b => b + | {| f3 := b |} => b end : TT -> 0 = 0 proj = @@ -72,3 +72,11 @@ e1 : texp t1 e2 : texp t2 The term "0" has type "nat" while it is expected to have type "typeDenote t0". +fun '{{n, m, _}} => n + m + : J -> nat +fun '{{n, m, p}} => n + m + p + : J -> nat +fun '(D n m p q) => n + m + p + q + : J -> nat +The command has indeed failed with message: +The constructor D (in type J) expects 3 arguments. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4074896420..6a4fd007df 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:= | TBinop t1 t2 _ b e1 e2 => O end. +(* Test notations with local definitions in constructors *) + +Inductive J := D : forall n m, let p := n+m in nat -> J. +Notation "{{ n , m , q }}" := (D n m q). + +Check fun x : J => let '{{n, m, _}} := x in n + m. +Check fun x : J => let '{{n, m, p}} := x in n + m + p. + +(* Cannot use the notation because of the dependency in p *) + +Check fun x => let '(D n m p q) := x in n+m+p+q. + +(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *) + +Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index e69e23276b..b2e3c3e923 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Module M. Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 3036f8f05b..505c5ce378 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Section S. Definition foo := nonexistent. End S. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 360f379676..0cb870c577 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,3 +98,7 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +fun x : ?A => x === x + : forall x : ?A, x = x +where +?A : [x : ?A |- Type] (x cannot be used) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 4b8bfe3124..5676fe8c7c 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" := (at level 85, x binder, z binder). Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(**********************************************************************) +(* Test printing of #5526 *) + +Notation "x === x" := (eq_refl x) (only printing, at level 10). +Check (fun x => eq_refl x). diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index 36d643a447..d45343fe60 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -14,3 +14,19 @@ build 5 : test_r build_c 5 : test_c +fun '(C _ p) => p + : N -> True +fun '{| T := T |} => T + : N -> Type +fun '(C T p) => (T, p) + : N -> Type * True +fun '{| q := p |} => p + : M -> True +fun '{| U := T |} => T + : M -> Type +fun '{| U := T; q := p |} => (T, p) + : M -> Type * True +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 6aa3df9830..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -19,3 +19,15 @@ Check build 5. Check {| field := 5 |}. Check build_r 5. Check build_c 5. + +Record N := C { T : Type; _ : True }. +Check fun x:N => let 'C _ p := x in p. +Check fun x:N => let 'C T _ := x in T. +Check fun x:N => let 'C T p := x in (T,p). + +Record M := D { U : Type; a := 0; q : True }. +Check fun x:M => let 'D T _ p := x in p. +Check fun x:M => let 'D T _ p := x in T. +Check fun x:M => let 'D T p := x in (T,p). +Check fun x:M => let 'D T a p := x in (T,p,a). +Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out new file mode 100644 index 0000000000..d0c963be17 --- /dev/null +++ b/test-suite/output/Show.out @@ -0,0 +1,12 @@ +3 subgoals, subgoal 1 (ID 29) + + H : 0 = 0 + ============================ + 1 = 1 + +subgoal 2 (ID 33) is: + 1 = S (S m') +subgoal 3 (ID 20) is: + S (S n') = S m +(dependent evars: (printing disabled) ) + diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v new file mode 100644 index 0000000000..60faac8dd9 --- /dev/null +++ b/test-suite/output/Show.v @@ -0,0 +1,11 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) + +(* tests of Show output with -emacs flag to coqtop; see bug 5535 *) + +Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). +Proof. + intros. + induction n as [| n']. + induction m as [| m']. + Show. +Admitted. diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out new file mode 100644 index 0000000000..e5520b8dfa --- /dev/null +++ b/test-suite/output/ShowMatch.out @@ -0,0 +1,8 @@ +match # with + | f => + end + +match # with + | A.f => + end + diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v new file mode 100644 index 0000000000..02b7eada83 --- /dev/null +++ b/test-suite/output/ShowMatch.v @@ -0,0 +1,13 @@ +(* Bug 5546 complained about unqualified constructors in Show Match output, + when qualification is needed to disambiguate them +*) + +Module A. + Inductive foo := f. + Show Match foo. (* no need to disambiguate *) +End A. + +Module B. + Inductive foo := f. + (* local foo shadows A.foo, so constructor "f" needs disambiguation *) + Show Match A.foo. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 49c465b6c6..52fe98ac07 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end. Check match niln in listn O return O=O with niln => eq_refl end. + +(* A test about nested "as" clauses *) +(* (was failing up to May 2017) *) + +Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v index db6348fa17..732a024fc1 100644 --- a/test-suite/success/Compat84.v +++ b/test-suite/success/Compat84.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal True. solve [ constructor 1 ]. Undo. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index dd5aa81d1d..855f26698c 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -2,3 +2,26 @@ Scheme Induction for eq Sort Prop. Check eq_ind_dep. + +(* This was broken in v8.5 *) + +Set Rewriting Schemes. +Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a. +Unset Rewriting Schemes. + +Check myeq_rect. +Check myeq_ind. +Check myeq_rec. +Check myeq_congr. +Check myeq_sym_internal. +Check myeq_rew. +Check myeq_rew_dep. +Check myeq_rew_fwd_dep. +Check myeq_rew_r. +Check internal_myeq_sym_involutive. +Check myeq_rew_r_dep. +Check myeq_rew_fwd_r_dep. + +Set Rewriting Schemes. +Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. +Unset Rewriting Schemes. diff --git a/test-suite/success/all-check.v b/test-suite/success/all-check.v new file mode 100644 index 0000000000..391bc540e4 --- /dev/null +++ b/test-suite/success/all-check.v @@ -0,0 +1,3 @@ +Goal True. +Fail all:Check _. +Abort. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 4e2bf45118..4b2f7b53e1 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -414,4 +414,10 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2. Import EqNotations. Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a. +(* Check that pre-existing evars are not counted as newly undefined in "set" *) +(* Reported by Théo *) +Goal exists n : nat, n = n -> True. +eexists. +set (H := _ = _). +Abort. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index ce90990594..d7ec092d76 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,16 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* A variant of #2602 which was wrongly succeeding because "a", bound to + "?m", was then internally turned into a "_" in the second matching *) + +Goal exists m, S m > 0. +eexists. +Fail match goal with + | |- context [ S ?a ] => + match goal with + | |- S a > a => idtac + end +end. +Abort. diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 45c539e229..a865ee987f 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -42,6 +42,11 @@ let rec search_cst_label lab = function | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields +let rec search_mind_label lab = function + | [] -> raise Not_found + | (l, SFBmind mind) :: _ when Label.equal l lab -> mind + | _ :: fields -> search_mind_label lab fields + (* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: a) I don't see currently what should be used instead b) this shouldn't be critical for Print Assumption. At worse some @@ -133,6 +138,18 @@ let lookup_constant cst = else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None +let lookup_mind_in_impl mind = + try + let mp,dp,lab = repr_kn (canonical_mind mind) in + let fields = memoize_fields_of_mp mp in + search_mind_label lab fields + with Not_found -> + anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind) + +let lookup_mind mind = + try Global.lookup_mind mind + with Not_found -> lookup_mind_in_impl mind + (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) @@ -204,7 +221,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = where I_0, I_1, ... are in the same mutual definition and c_ij are all their constructors. *) if Refmap_env.mem firstind_ref data then data, ax2ty else - let mib = Global.lookup_mind mind in + let mib = lookup_mind mind in (* Collects references of parameters *) let param_ctx = mib.mind_params_ctxt in let nparam = List.length param_ctx in @@ -308,7 +325,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = else accu | IndRef (m,_) | ConstructRef ((m,_),_) -> - let mind = Global.lookup_mind m in + let mind = lookup_mind m in if mind.mind_typing_flags.check_guarded then accu else diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e90d638d03..9618cf1b2b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -294,22 +294,22 @@ let is_numeral symbs = | _ -> false -let rec get_notation_vars = function +let rec get_notation_vars onlyprint = function | [] -> [] | NonTerminal id :: sl -> - let vars = get_notation_vars sl in + let vars = get_notation_vars onlyprint sl in if Id.equal id ldots_var then vars else - if Id.List.mem id vars then + (* don't check for nonlinearity if printing only, see Bug 5526 *) + if not onlyprint && Id.List.mem id vars then errorlabstrm "Metasyntax.get_notation_vars" (str "Variable " ++ pr_id id ++ str " occurs more than once.") - else - id::vars - | (Terminal _ | Break _) :: sl -> get_notation_vars sl + else id::vars + | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl | SProdList _ :: _ -> assert false -let analyze_notation_tokens l = +let analyze_notation_tokens ~onlyprint l = let l = raw_analyze_notation_tokens l in - let vars = get_notation_vars l in + let vars = get_notation_vars onlyprint l in let recvars,l = interp_list_parser [] l in recvars, List.subtract Id.equal vars (List.map snd recvars), l @@ -515,11 +515,35 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) +let warn_skip_spaces_curly = + CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" + (fun () ->strbrk "Skipping spaces inside curly brackets") + +let rec drop_spacing = function + | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt + | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt + | fmt -> fmt + +let has_closing_curly_brace symbs fmt = + (* TODO: recognize and fail in case a box overlaps a pair of curly braces *) + let fmt = drop_spacing fmt in + match symbs, fmt with + | NonTerminal s :: symbs, (UnpTerminal s' as u) :: fmt when Id.equal s (Id.of_string s') -> + let fmt = drop_spacing fmt in + (match fmt with + | UnpTerminal "}" :: fmt -> Some (u :: fmt) + | _ -> None) + | _ -> None + let hunks_of_format (from,(vars,typs)) symfmt = + let a = ref None in let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when String.equal s' (String.make (String.length s') ' ') -> let symbs, l = aux (symbs,fmt) in symbs, u :: l + | symbs, (UnpTerminal "{") :: fmt when (a := has_closing_curly_brace symbs fmt; !a <> None) -> + let newfmt = Option.get !a in + aux (symbs,newfmt) | Terminal s :: symbs, (UnpTerminal s') :: fmt when String.equal s (String.drop_simple_quotes s') -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l @@ -785,6 +809,15 @@ let check_useless_entry_types recvars mainvars etyps = (pr_id x ++ str " is unbound in the notation.") | _ -> () +let check_binder_type recvars etyps = + let l1,l2 = List.split recvars in + let l = l1@l2 in + List.iter (function + | (x,ETBinder b) when not (List.mem x l) -> + errorlabstrm "" (str (if b then "binder" else "closed binder") ++ + strbrk " is only for use in recursive notations for binders.") + | _ -> ()) etyps + let not_a_syntax_modifier = function | SetOnlyParsing -> true | SetOnlyPrinting -> true @@ -952,10 +985,6 @@ let check_curly_brackets_notation_exists () = error "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved." -let warn_skip_spaces_curly = - CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" - (fun () ->strbrk "Skipping spaces inside curly brackets") - (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = let rec skip_break acc = function @@ -987,8 +1016,9 @@ let compute_syntax_data df modifiers = if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in - let (recvars,mainvars,symbols) = analyze_notation_tokens toks in + let (recvars,mainvars,symbols) = analyze_notation_tokens onlyprint toks in let _ = check_useless_entry_types recvars mainvars etyps in + let _ = check_binder_type recvars etyps in let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in @@ -1210,7 +1240,7 @@ let add_notation_in_scope local df c mods scope = let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in - let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in + let (recvars,mainvars,symbs) = analyze_notation_tokens onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let i_typs, onlyprint = if not (is_numeral symbs) then begin let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in @@ -1287,7 +1317,7 @@ let add_notation local c ((loc,df),modifiers) sc = let add_notation_extra_printing_rule df k v = let notk = let dfs = split_notation_string df in - let _,_, symbs = analyze_notation_tokens dfs in + let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in make_notation_key symbs in Notation.add_notation_extra_printing_rule notk k v diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bfdae85d50..2a599444c2 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -160,7 +160,9 @@ let pr_new_syntax po loc chan_beautify ocom = and a glimpse of the executed command *) let pp_cmd_header loc com = - let shorten s = try (String.sub s 0 30)^"..." with _ -> s in + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in let noblank s = for i = 0 to String.length s - 1 do match s.[i] with diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3df6d7a580..9beb3a6063 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -120,14 +120,29 @@ let show_intro all = [Not_found] is raised if the given string isn't the qualid of a known inductive type. *) +(* + + HH notes in PR #679: + + The Show Match could also be made more robust, for instance in the + presence of let in the branch of a constructor. A + decompose_prod_assum would probably suffice for that, but then, it + is a Context.Rel.Declaration.t which needs to be matched and not + just a pair (name,type). + + Otherwise, this is OK. After all, the API on inductive types is not + so canonical in general, and in this simple case, working at the + low-level of mind_nf_lc seems reasonable (compared to working at the + higher-level of Inductiveops). + +*) + let make_cases_aux glob_ref = match glob_ref with - | Globnames.IndRef i -> - let {Declarations.mind_nparams = np} - , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } - = Global.lookup_inductive i in - Util.Array.fold_right2 - (fun consname typ l -> + | Globnames.IndRef ind -> + let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in + Util.Array.fold_right_i + (fun i typ l -> let al = List.rev (fst (decompose_prod typ)) in let al = Util.List.skipn np al in let rec rename avoid = function @@ -136,8 +151,9 @@ let make_cases_aux glob_ref = let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in Id.to_string n' :: rename (n'::avoid) l in let al' = rename [] al in - (Id.to_string consname :: al') :: l) - carr tarr [] + let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in + (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) + tarr [] | _ -> raise Not_found let make_cases s = |