| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
The removed code isn't used locally and isn't exported in the signature
|
| |
|
|
|
|
|
|
| |
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
There are currently two other clashs : Lexer and Errors, but for
the moment these ones haven't impacted my experiments with extraction
and compiler-libs, while this Matching issue had. And anyway the new
name is more descriptive, in the spirit of the recent TacticMatching.
|
| |
|
|
|
| |
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
|
| | |
|
| | |
|
| |
|
|
| |
Impacts MapleMode.
|
| |
|
|
|
| |
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
To obtain a.vo one can now:
1) coqtop -quick -compile a
2) coqtop -vi2vo a.vi
To make that possible the .vo structure has been complicated. It is now
made of 5 segments.
| vo | vi | vi2vo | contents
--------------+------+-----+-------+------------------------------------
lib | Yes | Yes | Yes | libstack (modules, notations,...)
opauqe_univs | No | Yes | Yes | constraints coming from opaque proofs
discharge | No | Yes | No | data needed to close sections
tasks | No | Yes | No | STM tasks to produce proof terms
opaque_proofs | Yes | Yes | Yes | proof terms
--------------+------+-----+-------+------------------------------------
This means one can load only the strictly necessay parts. Usually one
does not load the tasks segment of a .vi nor the opaque_proof segment of
a .vo, unless one is turning a .vi into a .vo, in which case he load
all the segments.
Optional segments are marshalled as None. But for lib, all segments
are Array.t of:
| type
--------------+---------------------------------------------------------
lib | a list of Libobject.obj (n'importe quoi)
opauqe_univs | Univ.consraints Future.computation
discharge | what Cooking.cook_constr needs
tasks | Stm.tasks (a task is system_state * vernacexpr list)
opaque_proofs | Term.constr Future.computation
--------------+------+-----+-------+------------------------------------
Invariant: all Future.computation in a vo file (obtained by a vi2vo
compilation or not) have been terminated with Future.join (or
Future.sink). This means they are values (inside a box).
This invariant does not hold for vi files. E.g. opauqe_proofs can be
dangling Future.computation (i.e. NotHere exception). The vi2vo
compilation step will replace them by true values.
Rationale for opaque_univs: in the vi2vo transformation we want to reuse
the lib segment. Hence the missing pieces have to be put on the side,
not inside. Opaque proof terms are already in a separte segment.
Universe constraints are not, hence the new opauqe_univs segment. Such
segment, if present in a .vo file, is always loaded, and
Declare.open_constant will add to the environment the constraints stored
there. For regular constants this is not necessay since the constraints
are already in their enclosing module (and also in the constant_body).
With vi2vo the constraints coming from the proof are not in the
constant_body (hence not in the enclosing module) but there and are
added to the environment explicitly by Declare.open_constant.
Rationale for discharge: vi2vo produces a proof term in its original
context (in the middle of a section). Then it has to discharge the
object. This segment contains the data that is needed in order to do
so. It is morally the input that Lib.close_section passes to Cooking
(via the insane rewinding of libstack, GlobalRecipe, etc chain).
Checksums: the checksum of .vi and a .vo obtain from it is the same.
This means that if if b.vo has been compiled using a.vi, and then
a.vi is compiled into a.vo, Require Import b works (and recursively
loads a.vo).
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
containing opaque grammar objects, it now contains a string representing
the entry. In order to recover the entry from the string, the former must
have been created with [Pcoq.create_generic_entry] or similar. This is
guaranteed for entries generated by ARGUMENT EXTEND, and must be done by
hand otherwise.
Some plugins were fixed accordingly.
|
| | |
|
| | |
|
| |
|
|
| |
Moreover, cleanup of System.connect (used by the "external" tactic).
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Omega now reuse the same inner variable names (Zvar0, Zvar1, ...)
at each run. This way, the obtained proof-terms on
two identical omega runs should be the same.
This wasn't always the case earlier:
- the two proofs were almost always convertible, but with distinct
variable names.
- in very rare situations, the two proofs could even be non-convertible.
Indeed, the omega engine use hash-tables which may be sensible to
the names in the (in)equality system and hence lead to different
solutions. Example of this behavior (with ocaml 4, whose default hash
function is different from ocaml 3.12, leading to a different behavior
here !) :
--------------------------------------------------------------------
Require Import Omega.
Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Check (eq_refl : test1 = test2). (* OK *)
Check (eq_refl : test1 = test3). (* OK *)
Check (eq_refl : test1 = test4). (* KO, test4 is different !! *)
--------------------------------------------------------------------
The old behavior could be restored with "Unset Stable Omega".
Thanks to Frédéric Loulergue for spotting this sensibility to
the underlying ocaml versions...
|
| |
|
|
|
|
| |
To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
|
| |
|
|
| |
and nia.
|
| |
|
|
|
|
| |
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
|
| |
|
| |
My bad, I forgot to fix the classification before comitting.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A small plugin to support program deriving (à la Richard Bird) in Coq.
It's fairly simple:
Require Coq.Derive.Derive.
Derive f From g Upto eq As h.
Produces a goal (actually two, but the first one is automatically shelved):
|- eq g ?42
And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).
|
| |
|
|
| |
This commit removes the hook.
|
| |
|
|
|
|
| |
We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command.
In this commit, we remove the compute_guard parameter.
|
| |
|
|
|
|
|
|
|
|
| |
proofs end.
The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it.
In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands.
In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
|
| |
|
|
|
|
| |
synchrone.
The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
parsing is plugged.
|
| |
|
|
| |
provided tactic environment to handle open terms.
|
| |
|
|
|
|
|
|
| |
Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.
|
| | |
|
| |
|
|
| |
execution)
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Detected in CompCert.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17026 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
As a result the use of the glist-style interface for manipulating goals has almost been removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.
This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.
This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16986 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
all:tac applies tac to all the focused subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
They were a hack to avoid looking where exceptions were raised and not
caught. Hopefully I produce a cleaner stack now, catching errors when
it is needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
It is highlighted in yellow in Coqide.
The unsafe status is tracked throughout the execution of tactics such that
nested calls to admit are caught.
Many function (mainly those building constr with tactics such as typeclass
related stuff, and Function, and a few other like eauto's use of Hint Extern)
drop the unsafe status. This is unfortunate, but a lot of refactoring would
be in order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
It seems to work ok, but I'm not too confident in the long run.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16975 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Pierre Letouzey
Pierre-Marie Pédrot
Arnaud Spiwack
Enrico Tassi
Pierre Boutillier
Julien Forest
jforest
Frédéric Besson
Guillaume Melquiond
fbesson
ppedrot
aspiwack