| Age | Commit message (Collapse) | Author |
|---|
|
Update Numbers that was implicitely using [simpl_relation] instead of
the default tactic [program_simpl].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
NB: the grammar entry is placed in vernac:command on purpose
even if it should have gone into vernac:gallina_ext. Camlp4
isn't factorising rules starting by "Declare" in a correct way
otherwise...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- to type patterns w/o losing the information of what subterm is a hole
would need to remember where holes were in "understand", but "understand"
needs sometimes to instantiate evars to ensure the type of an evar
is not its original type but the type of its instance (what can
e.g. lower a universe level); we would need here to update evars
type at the same time we define them but this would need in turn to
check the convertibility of the actual and expected type since otherwise
type-checking constraints may disappear;
- typing pattern is apparently expensive in time; is it worth to do it
for the benefit of pattern-matching compilation and coercion insertion?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
the general sigma of the goal so that tactics have no such low-level
tclEVARS, Evd.merge, or check_evars to do:
- what takes tclEVARS and check_evars in charge is now a new
tactical of name tclWITHHOLES (this tactical has a flag to support
tactics in either the "e"- mode and the non "e"- mode);
- the merge of goal evars and holes is now done generically at
interpretation time (in tacinterp) and as a side-effect it also
anticipates the possibility to refer to evars of the goal in the
arguments;
- with this approach, we don't need such constr/open_constr or
bindings/ebindings variants and we can get rid of all ugly
inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
this is the case e.g. of "rewrite !c" which morally reevaluates c at
each new rewriting step; this kind of tactics still receive a
specific sigma around their arguments and they have to merge evars
and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fixed some bugs in -beautify and robustness of {struct} clause.
Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1- Management of the name-space in a modular development / sharing of non-logical objects.
2- Performance of atomic module operations (adding a module to the environment, subtyping ...).
1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P
Module M := P.
Module M.
Include P.
...
End M.
Declare Module K : S with Module M := P.
In this 3 cases we don't want to be bothered by the duplication of names.
Of course, M.foo delta reduce to P.foo but many non-logical features of coq
do not work modulo conversion (they use eq_constr or constr_pat object).
To engender a transparent name-space (ie using P.foo or M.foo is the same thing)
we quotient the name-space by the equivalence relation on names induced by the
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo).
So:
*************************************************************************************
* Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values *
*************************************************************************************
Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free
(also for a posteriori declaration of them, ex: a notation on M.foo will be
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.
2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate
several functors then we have bigger vo.
Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12383 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12338 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
have no effect when the module is later imported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12332 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
obligation tactic so that [Program] can work without importing
anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12330 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by Context. Now Context has exactly the same semantics as Variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
obligations in [Program Fixpoint].
- Add maximal implicits for pairs in [Program.Syntax].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12319 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- better implicits for [antisymmetry]
- don't throw away implicit arguments info when doing [Program
Definition : type.]
- add standard debugging tactics to print goals/hyps in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12317 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
when the environment is reset. Bug is due to the use of
the imperative the_globrevtab when trying to pretty-print the terms
involved which may refer to the last defined obligation which is defined
in the exception's environment and not the global one anymore.
Bug reported by Francois Pottier.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12302 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
only used to allow a module to be ended before the summaries were
restored what can be solved by moving upwards the place where the
summaries are restored).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
wrong tycon.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12216 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in Program's pattern-matching compilation (fixes bug #2131).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
on a matched variable when it is of dependent type, when its type allows
it (no constructor in the real arguments).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12213 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
was true.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
and add an optional fail_evar flag to control resolution better in
interpretation functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12197 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactics that use it won't be in scope either.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12193 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unnecessarily computed when the user won't see it (avoids the costly
nf_evar_defs in typeclass errors).
Add hook support for mutual definitions in Program.
Try to solve only the argument typeclasses when calling [refine].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
definitions and variables (may increase the vo's size a bit), which in
turn fixes discharging with manual implicit args only.
Fix Context to correctly handle "kept" assumptions for typeclasses,
discharging a class variable when any variable bound in it is used.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12150 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de Bruijn-bound parameters (reported by W. Swierstra).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12142 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12126 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12116 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
clause resulting in stray notations for e.g. variable named "le")
and 12083 (fixing bug in as clause of apply in) from trunk.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12103 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml
so as to ease the comparison between these files. Application of a
change that cannot do harm: j_nf_evar now called after getting evd
from consider_remaining_unif_problems in
Subtac_pretyping_F.understand_judgment. Four differences remain
(is it the sign of a problem?):
1) understand_type fails in Pretyping if evars remain but does not fail in
Subtac_pretyping_F
2) resolve_typeclasses (when called) is called with ~onlyargs:false and
~fail:true in Pretyping.understand, Pretyping.understand_gen and
Pretyping.understand_type but with true and false in these same
functions in Subtac_pretyping_F
3) understand_ltac does not call typeclasses in Pretyping but it
does call it in Subtac_pretyping_F
4) understand_judgment does call typeclasses in Pretyping but not in
Subtac_pretyping_F
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Program.Tactics anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12089 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
clearing of recursive protototypes in Program obligations. Relies on
marking said prototypes with a particular constant and preprocessing
obligation goals with an appropriate tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
well-formed before doing anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12070 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This commit concerns about the first half of the useless code
mentionned by Oug for coqtop (without plugins). For the moment,
Oug is used in a mode where any elements mentionned in a .mli
is considered to be precious. This already allows to detect and
remove about 600 lines, and more is still to come.
Among the interesting points, the type Entries.specification_entry
and its constructors SPExxx were never used. Large parts of cases.ml
(and hence subtac_cases.ml) were also useless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- unnecessary and inefficient nf_evar_defs in coercion code
- use new way of inferring match return clauses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments.
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- de Bruijn bug #2083
- Avoid useless eta-expansion (bug #2060)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
