| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
** Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.
|
|
* If this flag under=true: enable flag with_evars of refine_with
to create evar(s) if the "under lemma" has non-inferable args.
* Backward compatibility of ssr rewrite is kept.
* Fix test-suite/ssr/dependent_type_err.v
|
|
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
|
|
|
|
|
|
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaëtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
|
|
|
|
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
|
of objects having the same name as the section).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12496 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixing non-export of newly created Local Argument Scope.
- Fixing bad discharge of local variables in nested sections
(bug still exists in v8.2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).
Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Application to the test of notation import from within a section.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7
|
