| Age | Commit message (Collapse) | Author |
|---|
|
Bronson), some keywords in coqdoc, and test well-typedness of predicate
in subtac_cases after abstraction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Use return clause inference in addition to the
automatic generation of equalities for pattern-matching.
- Disallow generation of coercions between type constructors,
which are not provable anyway.
- Improve inference for local (co-)fixpoints using the typing
constraint.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11140 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactic named "app").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11139 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inference. Little improvement un subtac_obligations: do not retry to
solve all obligations when finishing to solve one obligation nobody
depends on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
typeclass code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
files, about definitions and type of references.
- Add missing location information on fixpoints/cofixpoint in topconstr and
syntactic definitions in vernacentries for correct dumping.
- Dump definition information in vernacentries: defs, constructors,
projections etc...
- Modify coqdoc/index.mll to use this information instead of trying to
scan the file.
- Use the type information in latex output, update coqdoc.sty accordingly.
- Use the hyperref package to do crossrefs between definition and
references to coq objects in latex.
Next step is to test and debug it on bigger developments.
On the side:
- Fix Program Let which was adding a Global definition.
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fix typeclass interface: instance_constructor now takes the instance
constrs as argument to build and return the corresponding term and
type.
- Better typeclass error reporting when defining fixpoints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10975 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fix a typo in lowercase_utf8
- Fix generation of signatures in subtac_cases not working for dependent
inductive types with dependent indices.
- Fix coercion of inductive types generating ill-typed terms.
- Fix test script using new syntax for Instances.
- Move simpl_existTs to Program.Equality and use it in simpl_depind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Add a typeclasses_eauto which uses only the typeclass_instances
database.
- Set obligations as transparent by default to avoid the
common problem with ill-formed recursive defs due to opaque
obligations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binders.
- Change syntax of type class instances to better match the usual syntax of
lemmas/definitions with name first, then arguments ":" instance.
Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
Program.Utils, and subset_scope as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
name after internalisation, to get the correct behavior with typeclass
binders. This simplifies the pretty printing and translation
of the recursive argument name in various places too. Use this
opportunity to factorize the different internalization and
interpretation functions of binders as well.
This definitely fixes part 2 of bug
#1846 and makes it possible to use fixpoint definitions with typeclass arguments in
program too, with an example given in EquivDec.
At the same time, one fix and one enhancement in Program:
- fix a de Bruijn bug in subtac_cases
- introduce locations of obligations and use them in case the obligation tactic
raises a failure when tried on a particular obligation, as suggested by
Sean Wilson.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
du filtrage. Cela permet de détecter les cas impossibles et de simuler
les contraintes d'inversion exprimables sous la forme d'un assignement
des arguments du constructeurs (cf le cas de Vtail dans Bvector.v).
Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi)
avec vi composé uniquement de constructeurs, et que le résultat final
est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on
construit le prédicat
Q:=fun x1 .. xn y =>
match x1 .. xn y with
| v1(z) .. vn(z) t => P(z)
| _ .. _ _ => ?evar-speciale-cas-impossible
end
qui vérifiera bien que Q u1 .. un = P(w1,..,wp).
En raison de limitations de l'unification (on aurait besoin d'eta
conversion pour résoudre des problèmes du genre
"terme rigide == match x with _ => ?evar end", et besoin d'instanciation par
constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"),
je n'ai pas réussi à traiter le cas général.
Aussi, on adopte une stratégie pragmatique consistant à tester
plusieurs prédicats possibles :
- si un type final est donné, on essaie d'abord l'algorithme de
Matthieu et sinon le nouvel algorithme (permet par exemple de traiter
certains cas d'élimination dépendante de Bvector.v),
- s'il n'y a pas de type final, on essaie d'abord le nouvel algo et
sinon, on essaie avec un prédicat sans dépendance (permet de traiter
des cas compliqués comme celui de par cas sur I' dans le fichier
Case13.v de la test-suite).
Dans la pratique, il y a beaucoup de changement dans le code de compile_case.
- Par exemple, la compilation est maintenant toujours appelé avec un
prédicat (là où l'on pouvait avoir None, on a maintenant toujours au
moins une evar).
- En revanche, le membre droit des clauses est maintenant
optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une
branche impossible au moment du calcul du prédicat de retour.
- Aussi, on renonce aux PrLetIn et PrProd dans l'expression du
predicat de retour mais il faut savoir que c'est maintenant la liste
des tomatchs qui spécifie le contexte exact dans lequel le prédicat
de retour est bien typé.
- Et d'autres...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"pose as" de Program.
- Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml.
- Comportement de "simple apply" rendu plus proche de celui du apply 8.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des théorèmes prouvés par récursion ou corécursion mutuelle.
Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
account.
- Add test case for bug #1844 on Combined Scheme.
- Change Reflexive_partial_app_morphism to require a Reflexive proof to
cut down search earlier, without losing anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10846 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de l'argument donné contient des métavariables (souhait
#1408). Beaucoup d'infrastructure autour des constantes pour cela mais
qu'on devrait pouvoir récupérer pour analyser plus finement le
comportement des constantes en général :
1- Pour insérer les coercions, on utilise une transformation
(expérimentale) de Metas vers Evars le temps d'appeler coercion.ml.
2- Pour la compatibilité, on s'interdit d'insérer une coercion entre
classes flexibles parce que sinon l'insertion de coercion peut prendre
précédence sur la résolution des evars ce qui peut changer les
comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN).
3- Pour se souvenir rapidement de la nature flexible ou rigide du
symbole de tête d'une constante vis à vis de l'évaluation, on met en
place une table associant à chaque constante sa constante de tête (heads.ml)
4- Comme la table des constantes de tête a besoin de connaître
l'opacité des variables de section, la partie tables de declare.ml va
dans un nouveau decls.ml.
Au passage, simplification de coercion.ml, correction de petits bugs
(l'interface de Gset.fold n'était pas assez générale; specialize
cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml];
whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml])
et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml,
classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- More meaningful argument name for resolve_typeclasses.
- Try to remove unneeded instance declarations in
Morphisms.
- Allow the proofs of reflexivity arising from unchanged
arguments in setoid_rewrite to be fullfiled by Morphism instances and
not necessariy because the relation is reflexive (needed by
higher-order morphisms). Use a new "MorphismProxy" class to implement
that efficiently.
- Fix a bug in abstract_generalize not delta-reducing a type where it should.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
semantics.
- Add an Equivalence instance for pointwise equality from an
Equivalence on the codomain of a function type, used by default when
comparing functions with the Setoid's ===/equiv.
- Partially fix the auto hint database "add" function where the exact
same lemma could be added twice (happens when doing load for example).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- vérification de la cohérence des ident pour éviter une option -R
avec des noms non parsables (la vérification est faite dans
id_of_string ce qui est très exigeant; faudrait-il une solution plus
souple ?)
- correction message d'erreur inapproprié dans le apply qui descend dans les
conjonctions
- nettoyage autour de l'échec en présence de métas dans le prim_refiner
- nouveau message d'erreur quand des variables ne peuvent être instanciées
- quelques simplifications et davantage de robustesse dans inversion
- factorisation du code de constructor and co avec celui de econstructor and co
Documentation des tactiques
- edestruct/einduction/ecase/eelim et nouveautés apply
- nouvelle sémantique des intropatterns disjonctifs et documentation des
pattern -> et <-
- relecture de certaines parties du chapitre tactique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
declarations. By default, print the list of implicitely generalized
variables. Implement new commands Add Parametric Relation/Morphism for...
parametric relations and morphisms. Now the Add * commands are strict
about free vars and will fail if there remain some. Parametric just allows to
give a variable context. Also, correct a bug in generalization of
implicits that ordered the variables in the wrong order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
declarations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
whether or not to keep them regardless of the actual dependencies (in
order to implement the proper discharge behavior for type classes).
This means adding an argument to rebuild_function in libobject, giving
this information on variables after a section's constants have been
discharged (discharge_function is too early). Surface syntax for
Variable not added yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pas correctes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to reduce proofs (requested by users).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10735 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[in I] := t [return pred] in b", just as SSReflect does with let:.
Change implementation: no longer a separate AST node, just add a case_style
annotation on Cases to indicate it (if ML was dependently typed we
could ensure that LetPatternStyle Cases have only one term to be
matched and one branch, alas...). This factors out most code and we lose
no functionality (win ! win !). Add LetPat.v test suite.
- Slight improvement of inference of return clauses for dependent
pattern matching. If matching a variable of non-dependent type
under a tycon that mentions it while giving no return clause, the
dependency will be automatically infered. Examples at the end of
DepPat. Should get rid of most explicit returns under tycons.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Better interface in constrintern w.r.t. evars used during typechecking
- Add "unsatisfiable_constraints" exception which gives back the raw
evar_map that was not satisfied during typeclass search (presentation
could be improved).
- Correctly infer the minimal sort for typeclasses declared as
definitions (everything was in type before).
- Really handle priorities in typeclass eauto: goals produced with higher
priority (lowest number) instances are tried before other of lower
priority goals, regardless of the number of subgoals.
- Change inverse to a notation for flip, now that universe polymorphic
definitions are handled correctly.
- Add EquivalenceDec class similar to SetoidDec, declaring decision
procedures for equivalences.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations), explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
names, gives the ability to specify qualified classes in instance
declarations. Use that in the class_tactics code.
Refine the implementation of classes. For singleton classes the
implementation of the class becomes a regular definition (into Type or
Prop). The single method becomes a 'trivial' projection that allows to
launch typeclass resolution. Each instance is just a definition as
usual. Examples in theories/Classes/RelationClasses. This permits to
define [Class reflexive A (R : relation A) := refl : forall x, R x
x.]. The definition of [reflexive] that is generated is the same as the
original one. We just need a way to declare arbitrary lemmas as
instances of a particular class to retrofit existing reflexivity lemmas
as typeclass instances of the [reflexive] class.
Also debug rewriting under binders in setoid_rewrite to allow rewriting
with lemmas which capture the bound variables when applied (works only
with setoid_rewrite, as rewrite first matches the lemma with the entire,
closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal
[exists x, P (f x)].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
check_required_library where needed (fixes bug #1797).
Remove spurious messages from ring when not in verbose mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[id] instead of their expansions. Seems to slow things down a bit
(1s. on Ring_polynom).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
works in inductive type definitions and fixpoints. The semantics of
an implicit inductive parameter is maybe a bit weird: it is implicit in the
inductive definition of constructors and the contructor types but not in
the inductive type itself (ie. to model the fact that one rarely wants A
in vector A n to be implicit but in vnil yes). Example in test-suite/
Also, correct the handling of the implicit arguments across sections.
Every definition which had no explicitely given implicit arguments was
treated as if we asked to do global automatic implicit arguments on
section closing. Hence some arguments were given implicit status for no
apparent reason.
Also correct and test the parsing rule which disambiguates between {wf
..} and {A ..}.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10677 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction bug des filtres dans define_evar_as_abstraction
- Nettoyage, documentation et réorganisations diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10650 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10649 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
constant declarations, correct coercion between dependent products.
Remove fragile inh_conv_coerces_to code, may break existing Programs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10647 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.
While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.
Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(Axiom/Variable...). New tactic clapply to apply unapplied class methods
in tactic mode, simple solution to the fact that apply does not work
up-to classes yet. Add Functions.v for class definitions related to
functional morphisms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
eauto instead of an arbitrary tactic. Export more from eauto to allow
easier debugging.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Coq (solves part 2 of bug #1784). Add corresponding documentation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10530 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
recursive definitions. Now program accepts cofixpoints and uses the new
way infer structurally decreasing arguments. Also, checks for correct
recursive calls before giving the definition to the obligations machine
(solves part 1 of bug #1784).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Tabareau:
- first pass: generation of the Morphism constraints with metavariables
for unspecified relations by one fold over the term.
This builds a "respect" proof term for the whole term with holes.
- second pass: constraint solving of the evars, taking care of finding a
solution for all the evars at once.
- third step: normalize proof term by found evars, apply it, done!
Works with any relation, currently not as efficient as it could be due
to bad handling of evars. Also needs some fine tuning of the instances
declared in Morphisms.v that are used during proof search, e.g. using
priorities.
Reorganize Classes.* accordingly, separating the setoids in
Classes.SetoidClass from the general morphisms in Classes.Morphisms
and the generally applicable relation theory in Classes.Relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10493 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
wrapper around Ltac program_simpl ::= .
!!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
backwards compatible. Update CHANGES with things i've done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
hole kind info for topconstrs.
Derive eta_expansion from functional extensionality axiom.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
