| Age | Commit message (Collapse) | Author |
|---|
|
Idea: make coqtop more independant of the standard library.
In the future, we can imagine loading the syntax for numerals right
after their definition. For the moment, it is easier to stay lazy
and load the syntax plugins slightly before the definitions.
After this commit, the main (sole ?) references to theories/
from the core ml files are in Coqlib (but many parts of coqlib
are only used by plugins), and it mainly concerns Init
(+ Logic/JMeq and maybe a few others).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient
pas evalues, laissant des variables libres (symptome: exc Not_found)
- reals: Open Local --> Local Open
- ListTactics: syntaxe des listes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
loadable plugins
- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
when launching coqtop (see Coqtop.load_initial_plugins):
extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
is explicitely given to configure, coqtop is statically linked with all of
the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
same location as the .v during the build, but can be moved later in any place of
the ml loadpath.
This is clearly an experimentation. Feedback most welcome...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10923 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- si on met Rle_ge et Rge_le tous les deux en Resolve (et de même
pour Rlt_gt et Rgt_lt) alors on introduit un cycle,
- si on en met un des deux en Immediate, alors on perd la symétrie car si
un développement n'a un lemme en hints que pour Rge (resp Rle),
alors il ne sera pas utilisable si on met Rge_le (resp Rle_ge) en Immediate
(et c'est ce qui arrive notamment dans HighSchoolGeometry).
L'idéal serait d'introduire une notion de raisonnement modulo équivalence
dans auto afin que chaque lemme sur Rle (resp Rge) soit systématiquement
applicable aussi face à Rge (resp Rle) sans redondances et sans
cycle. Ainsi Rle_ge and co n'auraient pas un statut de hints mais plutôt un
statut de conversions implicites entre notions synonymes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
lemmes se terminant par False ou not sur n'importe quelle formule
(cela crée trop d'incompatibilités dans les "try apply" etc.); de
toutes façons, "contradict" joue presque ce rôle (à ceci près qu'il
ne traverse pas les conjonctions) (tactics/tactics.ml).
- Quelques corrections sur RIneq.v
- le hint Rlt_not_eq avait été oublié dans la phase de restructuration,
- davantage de noms canoniques (O -> 0, etc.),
- nouvelle tentative de ramener "auto" vers Rle (avec Rle_ge) plutôt
que vers Rge qui est moins souvent associé à des hints.
- Utilisation du formateur deep_ft pour afficher les scripts de preuve afin
d'éviter le besoin d'un "Set Printing Depth" (vernacentries.ml).
- Suppression de certaines utilisations de l'Anomaly de meta_fvalue
qui ne correspondaient pas à des comportements anormaux (reductionops.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10760 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Hints reste à faire. (dommage que Rge et Rle ne soient pas
convertibles)
- Ajout de Nnat et Ndigits dans NArith.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10751 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour
éviter la confusion avec le Rlt_not_le de RIneq.
- Quelques variantes de lemmes en plus dans RIneq.
- Déplacement des énoncés de sigT dans sig (y compris la complétude)
et utilisation de la notation { l:R | }.
- Suppression hypothèse inutile de ln_exists1.
- Ajout notation ² pour Rsqr.
Au passage:
- Déplacement de dec_inh_nat_subset_has_unique_least_element
de ChoiceFacts vers Wf_nat.
- Correction de l'espace en trop dans les notations de Specif.v liées à "&".
- MAJ fichier CHANGES
Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne
sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1"
non prouvé).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(rapport de bug 1807). Cf explication dans le fichier et/ou dans le
bug-tracker.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10613 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Rpower_O alors qu'on la garde pour les autres propriétés de la puissance.
(résultat d'une discussion avec Assia et Jean-Marc)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10609 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10599 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place
d'une option "modulo_conv" pour contrôler l'usage de cette delta.
- Pour éviter que rewrite ne réussise trop souvent, la delta est
désactivée pour les tactiques d'élimination (une étude fine reste à faire).
- On n'utilise aussi delta que sur les sous-termes du problème
d'unification initial. C'est une heuristique qui est intuitive mais qui
reste à être évaluée.
- Au bilan, le surcoût en temps de compilation des theories est d'un
peu moins d'1%.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10473 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(crédits à Sylvie Boldo)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10146 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
maintenant les differentes tactics marchent mieux mais le code
est moche ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- essai de suppression des dependances debiles. (echec)
- Application des patch debian.
Pour ring et field :
- introduciton de la function de sign et de puissance.
- Correction de certains bug.
- supression de ring_replace ....
Pour exact_no_check :
- ajout de la tactic : vm_cast_no_check (t)
qui remplace "exact_no_check (t<: type of Goal)"
(cette version forcais l'evaluation du cast dans le
pretypage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9298 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Rfun_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %F)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
bas, i.e. Set; renommage canonique Rmax_comm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
bas, i.e. Set; renommage canonique Rmax_comm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
'properties' de Subversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
but is bugguy with it. Temporary fix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
en préparation du passage à des inductifs à polymorphisme de sorte
("sigT R" va devenir de type le type de R, càd Set)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7219 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6897 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5197 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
documentee).
Reste a retablir la semantique de pose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
