aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
* \ Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \
| | * Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |/ |/|
* | Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
| |
* | Make "intro"/"intros" progress on existential variables.Gravatar Hugo Herbelin2018-05-02
| |
* | Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
| | | | | | | | | | | | | | | | | | | | | | | | We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
* | Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Gravatar Hugo Herbelin2018-04-26
| |
* | Merge PR #7237: [ssr] fix delayed clears (fix #7045)Gravatar Maxime Dénès2018-04-16
|\ \
* | | [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
| * | [ssr] fix delayed clears (fix #7045)Gravatar Enrico Tassi2018-04-13
|/ / | | | | | | | | We take into account all future ipats, not just the ones in the current branch
* | Merge PR #7087: Congruence tactic engine updateGravatar Pierre-Marie Pédrot2018-04-12
|\ \
* | | Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
| | |
| | * Fix #6770: fixpoint loses locality info in proof mode.Gravatar Gaëtan Gilbert2018-03-29
| |/ |/|
| * Congruence: Fixing a bug with native projections.Gravatar Hugo Herbelin2018-03-27
|/ | | | | | | | | There is a code to turn constants denoting projections into proper primitive projections, but it did not drop parameters. The code seems anyway redundant with an "expand_projections" which is already present in Cctac.decompose_term. After removal of this code, the two calls to congruence added to cc.v work.
* Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works).
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
| * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
| * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* | added test for coercion from typeGravatar charguer2018-03-09
| |
* | allow Prop as source for coercionsGravatar charguer2018-03-09
|/
* Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Gravatar Maxime Dénès2018-03-08
|\ \ \ | | | | | | | | | | | | wish #4129)
| | | * Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
| |_|/ |/| |
* | | Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \
| | * | An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
* | | | [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
| | | | | | | | | | | | | | | | Following up on #6791, we the option "Shrink Abstract".
* | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Gravatar Maxime Dénès2018-03-06
|\ \ \ \ | | | | | | | | | | | | | | | a record.
* \ \ \ \ Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \
| | | * | | | | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
| | * | | | | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| | |/ / / / /
* | | | | | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | |
| * | | | | | Adding a test file for evar handling in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| | |_|_|/ / | |/| | | |
* / | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
|/ / / / / | | | | | | | | | | | | | | | Noticed by Sigurd Schneider.
| * / / / Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/ / / /
* | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
* | | | Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
| | | |
| | * | Implement name mangling optionGravatar Jasper Hugunin2018-02-17
| | | |
* | | | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| |/ / |/| | | | | | | | | | | No using a mutable counter to skip them, instead we keep them in the environment.
| * | Fixing an anomaly in the presence of "let-in" in the type of a record.Gravatar Hugo Herbelin2018-02-13
|/ / | | | | | | Was raised by Jason on Gitter.
* | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | This ensures by construction that we never infer constraints outside the variance model.
* | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
* | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \
| * | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
| | |
* | | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ \ | |/ / |/| |
| * | More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| | |
| * | Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
| | |
* | | Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
|/ / | | | | | | | | | | | | The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else.