aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-09-02added Makefile target: validate (to recheck all .vo in a row)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11347 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-02avoid small overflowsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11346 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-02[checker] basic conversion oracle: expand local vars firstbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11345 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
backtracking on coercion classes when a coercion path fails). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11344 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-27Fix implementation of "Global Instance" which redeclared the samemsozeau
instance multiple times at each section closing (still a hack). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11338 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-27Major speed and space improvements in setoid rewrite:msozeau
- Avoid using projections for singleton classes. Divides the size of proofs by 2 and simplifies the typechecking as well. - Switch to the new discrimination net implementation for classes, with the current convention that all constants are unfoldable. Users can add "Typeclasses Opaque" declarations make the dnet discriminate more, otherwise it should be entirely backward-compatible. - Fix bug introduced in r11333 in "transitivity" tactic in presence of coercions. Up to 15% gains on setoid-intensive files like Ring_polynom and Field_theory. More importantly, performance should not decrease significantly by adding new Morphism/Setoid declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-27Little cleanup in auto.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11336 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-26Give back progress information after feeding the Program Instance to themsozeau
obligation handler. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11335 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-23Fix dependency problem that makes compilation fail :)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11334 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
syntax yet. Doesn't change the auto/eauto behavior either. - Typeclass resolution now considers everything transparent by default and does it consistently for "open" and closed terms. - Correctly declare singleton classes definition as opaque for proof search. - Add a few initial declarations to make iff, id, compose... opaque - Add definition of dependent signatures for dependent function types and remove corresponding exception code in class_tactics. The instance requires higher-order unification and is not really usable yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11333 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-22Typo (corrige le bug #1928)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11332 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-21Fixes in dependent induction tactic to keep names, allow givingmsozeau
intro-patterns and avoid useless generalizations on inductive parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11331 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-21Various fixes w.r.t typeclasses and subtac: resolve tcs properly insidemsozeau
inductive and Program defs. Fix eterm bug when generating obligations and remove optimization of let-in removal which prevents factorization of proofs/"asserts" in Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11330 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-18Revert commit 11326, to see if it is what makes bench failglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11329 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-18Renaming parser -> coq-parserglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11328 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-16Install csdpcert with librariesglondu
csdpcert is not meant to be called directly by the user git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11327 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-16Mind environment variables in (generated) coq_config.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11326 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-16Fix build/install failures when ocamlopt is not availableglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11325 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-12Add coqide manpage (taken from Debian)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11324 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-08Various fixes in manpagesglondu
* hyphen meant as the ascii character should be escaped * lines starting with a dot have a special meaning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11322 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-07Suite commit #11311notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11321 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-07micromega : bug fixes and optimisationsfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11318 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-07eviter redondance du message d'erreur (Error while reading / File)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11316 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-07coqc: warning de l'option -dump-glob (unused case)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11315 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-06Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + ↵notin
suppression de la dépendance envers aeguill (bug #1922) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11311 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-06Add lemmas on lists: nth_default_eq, map_nth_errorglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11310 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-06correction : coqart is already publishedjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11307 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-05Correction de bugs:herbelin
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un terme applicatif au moment de tester f u1 .. un = g v1 .. vn au premier ordre : on revient sur l'algo tel qu'il était avant le commit 11187. - Bug #1887 (format récursif cassé à cause de la vérification des idents). - Nouveau choix de formattage du message "Tactic Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-05Correction bug de filtrage sous-terme #1920 introduit dans commitherbelin
11126 et qui faisait qu'on ne backtrackait en fait plus sur les sous-termes d'un terme qui lui filtrait. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11304 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-05Suite 11187 et 11298 : ne retarder le dépliage d'une projectionherbelin
canonique que si elle contribue vraiment à une équation canonique, c'est-à-dire si son argument principal est une evar; sinon on répercute le comportement historique qui est de préférer le dépliage du côté droit d'une équation constante/constante. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11303 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-04Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parherbelin
un nom importé) de la 8.2 vers le trunk. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M pretyping/termops.ml M toplevel/command.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11302 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-04Évolutions diverses et variées.herbelin
- Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-31Corrige un bug du commit 11187 (le comportement à respecter étaitherbelin
celui-là: si une structure canonique existe déjà avec une certaine projection canonique donnée, on garde l'ancienne structure si jamais une structure canonique plus récente arrive avec la même projection canonique). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11298 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-29Oops... the trunk behaviour is differentglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11296 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-29Update test-suite outputglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11294 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-29Typo in docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11292 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-29Backport r11289.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11291 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fix typoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11287 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Use COQINSTALLPREFIX for doc tooglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11286 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fix bashism in test-suite/checkglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11284 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Remove pcoq from check prerequisitesglondu
It is already built by world, and this way, "make -j3 check" from clean sources work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11283 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fixes in generalize_eqs/dependent induction to allow the user to specifymsozeau
generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fix wrong environment bug in test for setoid_rewrite or rewrite.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11279 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fix bug in term dnet preventing some unifications. Allow "higher-order"msozeau
class constraints of the form Π x1 ... xn, Class args. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11278 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Show configure choice for browser in CoqIDE preferencesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11275 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-27Now, -browser option is effective (and compiles)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11273 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-27(Partially) Revert previous commit because of FTBFSglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11272 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-27Add -browser option to configure scriptglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11271 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-27Oups (on refait le 11268 en mieux)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11270 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
Now there is a class "SetoidRelation" for registering relations that should always be considered as setoids and never unfolded. Every "Add Relation" command adds an instance and impl,iff are there by default. Now the test is: if there is a SetoidRelation instance, use it ; otherwise, allow unfolding to find an eq or fallback on setoid_rewrite. To avoid searching for SetoidRelation instances repeateadly we check that it is really needed first by unfolding the hyp. Only two scripts relied on the now-forbidden semantics of rewriting by an @eq inside a setoid relation, in Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 20:29:36 +0000