| Age | Commit message (Collapse) | Author |
|---|
|
Debug handling of identifiers in coqdoc (should work with modules and
sections) and add missing macros.
Move theories/Program to THEORIESVO to put the files in the standard
library documentation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 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
|
|
impossibles dans un filtrage dépendant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10981 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
applied to no parameters.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10922 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
noms illégaux si le type auquel elle s'appliquait n'était pas pur ascii).
[util.ml, termops.ml]
- Simplification de la procédure d'initialisation (apparemment des résidus
obsolètes de la V5.10) et messages d'erreurs [lib.ml, toplevel.ml, coqtop.ml]
- Quelques pattern-matching incomplets [topconstr.ml, detyping.ml]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10916 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ un error qui devrait être un anomaly
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
notations work and bug #1846 gets completely fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10890 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
|
|
rewrite interp_context to use this new code instead of doing
internalization by itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
quotations de tactiques pour simuler les métas des constr - quitte à devoir
utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
des Meta [pretyping]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10790 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10770 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- ajout de -> et <- pour substitution immédiate d'une égalité
(comportement à la subst si variable, à la rewrite in * sinon)
- ajout possibilité d'hypothèses avec paramètres
- correction d'un comportement bizarre de l'utilisation des noms dans
cas "[[|] H]" (cf CHANGES)
Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])"
pour décider de garder les noms, mais la syntaxe est assez
moche. Peut-être un "intros H: <- H': [ | ]" ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 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
|
|
any typeclass parameter by name anywhere in a
typeclass constraint. This allows to share implementations easily and to
give any subset of the parameters in any order in the constraints,
whereas we are still restricted to a prefix of the typeclass parameters
context when using "positional" specifications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10736 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Use support for abbreviations with params added by Hugo for inverse.
- Standard priorities for operators on relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10733 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Nouvel essai de prise en compte unfold dans apply (unification.ml)
- Correction bug commit précédent (constrintern.ml)
- Correction bug d'explication des evars non résolues (evarutil.ml)
- Fenêtre de query coqide plus large (command_windows.ml)
- Orthographe tauto (tauto.ml4)
- Crédits (ConstructiveEpsilon.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Example: "Notation reflexive R := (forall x, R x x)."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 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
|
|
and needed coercions. Change API of interp_constr_evars to get an
optional evar_defs ref argument. Makes Algebra compile again (at least).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10715 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
|
|
rewrite calls fail because an occurence is found under a lambda that
was not found before and there are no adequate morphism declarations to
make the rewrite succeed nor the possibility to give occurences to
rewrite (yet). Only setoid_rewrite will try rewriting under lambda's for
now. Example problem found in a port of the Random library.
Also improved the required_library error message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10704 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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10532 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
kernel:
-declaration.ml
unification des representations pour les modules et modules types.
(type struct_expr_body)
-mod_typing.ml
le typage des modules est separe de l'evaluation des modules
-modops.ml
nouvelle fonction qui pour toutes expressions de structure calcule
sa forme evaluee.(eval_struct)
-safe_typing.ml
ajout du support du nouvel operateur Include.(add_include).
library:
-declaremods.ml
nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
les alias via la nametab.
parsing:
-g_vernac.ml4:
nouvelles regles pour le support des Includes et pour l'application des signatures
fonctorielles.
extraction:
Adaptation a la nouvelle representation des modules et support de l'operateur with.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 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
|
|
implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evars and try to solve them too.
Finally, rework tactics on setoids and design a saturating tactic to help solve goals on any setoid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
amélioration message d'erreur si nombre de pattern incorrect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with a decidable equality. Fix name capture bug, again.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10419 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
extensionality tactic to apply the axiom properly and fix test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10414 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un
ordinateur où j'ai pas installé lablgtk2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Au passage, un peu plus de standardisation des noms de fonctions de
globalisation
Principe de base :
locate_foo : qualid -> foo (échoue avec Not_found)
global : reference -> global_reference (échoue avec UserError)
global_of_foo : foo -> global_reference (échoue avec UserError)
f_with_alias : se comporte comme f mais prenant aussi en compte les
notations de la forme "Notation id:=ref"
Principale exception :
locate, au lieu de locate_global
locate_global_with_alias, qui prend en entrée un "qualid located"
Restent beaucoup de fonctions qui pourraient utiliser
global_with_alias au lieu de global, notamment dans contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
decidability of the usual equality
Major changes:
* andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v
* added 2 files:
* toplevel/ind_tables.ml* : tables where the boolean eqs and the
decidability proofs are stored
* toplevel/auto_ind_decl.ml* : code of the schemes that are automatically
generated from inductives types (currently boolean eq & decidability )
* improvement of injection: if the decidability have been correctly computed,
injection can now break the equalities over dependant pair
How to use:
Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
Scheme Equality for I. tries to create the equality for the already declared
type I
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
filtrage; sauts de line intempestifs dans pretty.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the latter is bound to a var which is not a quantified one - this led
to remove a line marked "temporary compatibility" ... ; made a distinction
between quantified hypothesis as for "intros until" and binding names as
in "apply with"; in both cases, we now expect that a identifier not used
as a variable, as in "apply f_equal with f:=g" where "f" is a true binder
name in f_equal, must not be used as a variable elsewhere [see
corresponding change in Ints/Tactic.v])
- Fixing bug 1643 (bug in the algorithm used to possibly reuse a
global name in the recursive calls of a coinductive term)
- Fixing bug 1699 (bug in contracting nested patterns at printing time
when the return clause of the subpatterns is dependent)
- Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic)
- Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evdref si evar_defs ref)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
échouer sur les Rel liées a des Anonymous et export de l'instance
des evars vers le printeur du débogueur.
- Suppression d'un reste de code mort lié à la V7 dans pretyping.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9970 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
utilities from Util. Some additions in Util, and simplifications
in various files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
