| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
|
| | |
|
| |
|
|
|
| |
PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel
|
| |
|
|
|
|
|
|
|
|
|
|
| |
When Coq's Haskell extraction needs to use unsafeCoerce, it passes
the -fglasgow-exts option to GHC, but recent versions of GHC warn
against this:
xx.hs:1:16: Warning:
-fglasgow-exts is deprecated: Use individual extensions instead
This patch does as the warning suggests, replacing -fglasgow-exts
with the specific option that the extraction needs (-XMagicHash).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When Haskell extraction requires magic type coersion, Coq produces
the following code:
unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif
GHC version 7.6.3 does not allow imports after a type declaration,
and produces this error:
xx.hs:20:1: parse error on input `import'
(referring to the first import statement above). This patch moves
the unsafeCoerce type declaration to just after the import statement,
fixing this compile error.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
|
| |
|
|
|
|
| |
an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.
|
| | |
|
| |
|
|
| |
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
|
| |
|
|
|
|
|
|
| |
That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals.
There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs.
Factored code with Ltac's refine in Extratactics.
|
| |
|
| |
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
|
| |
|
|
|
|
|
| |
committed by mistake. The message pretended to have a fix which is only
superficially a fix. The problem is more complex.
This reverts commit 251218905daea0838a3738466afa1c278bb3e81b.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Proofs of C t1..tn+1 = C t1..tn+1, even when the terms were
syntactically the same, were built by composition of a proof of C
t1..tn = C t1..tn with a proof of reflexivity of tn+1. The latter was
reduced to showing C t1..tn = C u1..un for C u1..un the canonical
representant of C t1..tn in its congruence class. But if some pair
ti=ui was derivable by injectivity of the constructor C, it might go
back to find a proof of C t1..tn+1 = C t1..tn+1 again, while a simple
reflexivity proof was enough here.
Not sure that the fix prevents any further loop in this part of the
code though.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
| |
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
| | |
|
| |
|
|
|
| |
Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
|
| |
|
|
|
|
| |
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
|
| |
|
|
|
| |
This solution is a bit dumb, but I guess does what one expects.
Each decl mode proof commands stays in proof mode.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
| |
|
|
|
|
|
|
| |
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
| |
|
|
| |
as "||" is actually redefined in "plugins/micromega/sos_lib.ml".
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).
|
| | |
|
| |
|
|
|
| |
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
| |
|
| |
More information, less pmp.
|
| |
|
|
|
| |
Left a README, just in case someone will discover the remnants of it
decades from now.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
| |
Dead code formerly used by the now defunct [autoinstances].
|
| |
|
|
| |
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
| |
|
|
|
|
|
|
|
|
|
| |
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
| |
|
|
|
| |
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
|
| |
|
|
|
|
|
|
|
|
|
| |
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
| | |
|
| |
|
|
| |
Based on suggestion by @gasche.
|
| |
|
|
|
|
|
|
|
|
|
| |
I'm not quite sure why, but I'm pretty sure it's not. Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".
I haven't touched the older instances of it in the CHANGES file.
|
Pierre-Marie Pédrot
Arnaud Spiwack
Enrico Tassi
Nickolai Zeldovich
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Frédéric Besson
Pierre Boutillier
Xavier Clerc
Julien Forest
Matthieu Sozeau
Jason Gross