| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
not let-ins in the binding list.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13335 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to their signature of implicit positions and scopes) is computed.
A bit of documentation in constrintern.mli.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
location dumping for binders uniformly treated in constrintern.ml (and
renamed the optional arg of interp_context from fail_anonymous to
global_level since the flag now also decides whether to dump binders as
global or local ones); added locations for the variables occurring in
the "as in" clauses;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
a 3 state type to allow:
* KernelVerbose / KernelSilent : handle the display of messages launch by Coq
* UserVerbose : handle the display of messages launch by user actions
Coq will still behaves the same way (TODOs in the code mark the places
where we can now change the behaviour). I'll remove them in a few days
when we'll have agreed on the correct behaviour.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).
Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.
Removed obsolete printer mod_self_id from dev/db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- #2095 (not fixed in v8.2 but fixed in v8.3 and trunk)
- #2108 (fixed in v8.2, v8.3, trunk)
- #2102 (moved warning to msg_warning to ensure flushing, but still
open enhancement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13121 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Definition's is not so painless. It seems to however generally provide
"nicer" scripts so let us keep it and update the contribs and
test-suite accordingly.
Also enforced that the actual introduced names to be exactly as given
in the statements.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixing a wierd behaviour of the goal window (scroll_at_iter doesn't work)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12991 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
informative exception if some constraints do not unify.
All calls except one used to raise a less informative exception when the
constraints weren't solved.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Also removed used of local_binders_length and local_assums_length
which are now incorrect due to the possible presence of `{ ... } contexts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12579 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@12500 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
|
|
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@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
colon in (mutual) proofs with [Set Automatic Introduction].
Fix a minor test-suite issue in ProgramWf due to new handling of the
default obligation tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12351 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
|
|
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
|
|
string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.
Added a file smartlocate.ml for high-level globalization functions.
Mini-nettoyage metasyntax.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 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
|
|
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
|
|
when it comes to notation declared in scope
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When defining an inductive type with a reserved notation in a
particuliar scope, the scope was not opened during the interpretation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12117 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
reorganization of code) and documentation (in pcoq.mli) of the code
for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
Notation, Notation); merged the two copies of interp_entry_name to
avoid they diverge.
- Added support in Tactic Notation for ne_..._list_sep in general and
for (ne_)ident_list(_sep) in particular.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 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
|
|
Combined Scheme.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12090 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
|
|
it does not cause a time penalty.
- Removing of get_type_of_with_meta made possible by the
evar_defs/evar_map merge.
- Adding unfolding of Meta in reductionops (this assumes that reduction does
not move Metas across binders...)
- Renaming newly created fold_map_rel_context into map_rel_context_in_env.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12061 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Not_found bug in Theorem with) from V8.2 to trunk.
- Improving indentation in presence of tabulation and utf-8 when
reporting error messages with "^^^^^^".
- Updating a few svn:ignore properties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par Evd). Ça s'accompagne de quelques autres modifications de
l'interface (certaines fonctions étaient des doublons, ou des
conversions entre evar_map et evar_defs).
J'ai modifié un peu la structure de evd.ml aussi, pour éviter des
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai
introduit des sous-modules pour les différentes couches.
Il y a à l'heure actuelle une pénalité en performance assez sévère (due
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique
est correct). Mais fera l'objet de plusieurs optimisations dans les
commits à venir.
Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour
l'instant incapable de comprendre ce qui cause cette erreur. J'espère
qu'on pourra le déterminer rapidement.
Ce commit est le tout premier commit dans le trunk en rapport avec les
évolution futures de la machine de preuve, en vue en particulier
d'obtenir un "vrai refine".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Quelques modifications autour (géographiquement) de Util.list_split_at
Util.list_split_at devient Util.list_split_when (dénomination inventée
arbitrairement par moi-même, mais qui ne devrait pas déranger grand
monde vu qu'il semble n'y avoir que deux occurences de cette fonction).
Pour laisser la place à la fonction suivante :
Introduction de Util.list_split_at: qui sépare la liste à une position
donnée (alors que la nouvellement nommé list_split_when sépare à la
première occurence "vrai" d'un prédicat).
Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux
fonctions.
Suppression de Impargs.list_split_at (appel à Util).
Suppression de Subtac_pretyping.list_split_at (qui était du code mort de
toute façon).
Suppression Util.list_split_by qui n'est utilisé nulle part et est une
réimplémentation de List.partition (qui est probablement meilleure, en
particulier tail-recursive)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
==========
This big patch is commited here with a HUGE experimental tag on it. It
is probably not a finished job. The aim of committing it now, as
agreed with Hugo, is to get some feedback from potential users to
identify more clearly the directions the implementation could take. So
please feel free to mail me any remarks, bug reports or advices at
<puech@cs.unibo.it>.
Here are the changes induced by it :
For the user
============
* Search tools have been reimplemented to be faster and more
general. Affected are [SearchPattern], [SearchRewrite] and [Search]
(not [SearchAbout] yet). Changes are:
- All of them accept general constructions, and previous syntactical
limitations are abolished. In particular, one can for example
[SearchPattern (nat -> Prop)], which will find [isSucc], but also
[le], [gt] etc.
- Patterns are typed. This means that you cannot search mistyped
expressions anymore. I'm not sure if it's a good or a bad thing
though (especially regarding coercions)...
* New tool to automatically infer (some) Record/Typeclasses instances.
Usage : [Record/Class *Infer* X := ...] flags a record/class as
subject to instance search. There is also an option to
activate/deactivate the search [Set/Unset Autoinstance]. It works
by finding combinations of definitions (actually all kinds of
objects) which forms a record instance, possibly parameterized. It
is activated at two moments:
- A complete search is done when defining a new record, to find all
possible instances that could have been formed with past
definitions. Example:
Require Import List.
Record Infer Monoid A (op:A->A->A) e :=
{ assoc : forall x y z, op x (op y z) = op (op x y) z;
idl : forall x, x = op x e ;
idr : forall x, x = op e x }.
new instance Monoid_autoinstance_1 : (Monoid nat plus 0)
[...]
- At each new declaration (Definition, Axiom, Inductive), a search
is made to find instances involving the new object. Example:
Parameter app_nil_beg : forall A (l:list A), l = nil ++ l.
new instance Build_Monoid_autoinstance_12 :
(forall H : Type, Monoid (list H) app nil) :=
(fun H : Type =>
Build_Monoid (list H) app nil ass_app (app_nil_beg H)
(app_nil_end H))
For the developper
==================
* New yet-to-be-named datastructure in [lib/dnet.ml]. Should do
efficient one-to-many or many-to-one non-linear first-order
filtering, faster than traditional methods like discrimination nets
(so yes, the name of the file should probably be changed).
* Comes with its application to Coq's terms
[pretyping/term_dnet.ml]. Terms are represented so that you can
search for patterns under products as fast as you would do not under
products, and facilities are provided to express other kind of
searches (head of application, under equality, whatever you need
that can be expressed as a pattern)
* A global repository of all objects defined and imported is
maintained [toplevel/libtypes.ml], with all search facilities
described before.
* A certain kind of proof search in [toplevel/autoinstance.ml]. For
the moment it is specialized on finding instances, but it should be
generalizable and reusable (more on this in a few months :-).
The bad news
============
* Compile time should increase by 0 to 15% (depending on the size of
the Requires done). This could be optimized greatly by not
performing substitutions on modules which are not functors I
think. There may also be some inefficiency sources left in my code
though...
* Vo's also gain a little bit of weight (20%). That's inevitable if I
wanted to store the big datastructure of objects, but could also be
optimized some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by user) and #2017 (unification pattern test too crude leading to
regression wrt to 8.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
declaration code to toplevel/record, including support for singleton
classes as definitions. Parsing code also factorized. Arnaud: one more
thing to think about when refactoring the definitions in vernacentries.
Add support for specifying what to do with anonymous variables in
contexts during internalisation (fixes bug #1982), current choice is to
generate a name for typeclass bindings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
help the type _checking_ anymore (they don't become typing constraints)
but they permit to coerce a subterm in a type. In particular, when
using a VM cast we avoid unneeded, unexpected conversions using the
default machine (oops!). Also remove the corresponding comment in
pretyping and fix the wrong use of casts in toplevel/command: accept
the trouble of using evars. This has the somewhat adverse effect that
when typing casted object we now have no typing constraints (see
e.g. examples in Cases.v)!
Probably, this will be backtracked partially tomorrow as many contribs
can rely on it and the change could make some unifications fail (in
particular with deep coercions). Let's try anyway!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
entre le calcul des arguments récursifs possibles -- bien que bidon en
attendant mieux -- et ce la tactique fix attend -- le premier expanse
les produits au maximum le second non)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
