aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Correction de bugs:Gravatar herbelin2008-08-05
| | | | | | | | | | | | | - 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
* Correction bug de filtrage sous-terme #1920 introduit dans commitGravatar herbelin2008-08-05
| | | | | | | | | 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
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
| | | | | | | | | | | 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
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
| | | | | | | | | | | | 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
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Corrige un bug du commit 11187 (le comportement à respecter étaitGravatar herbelin2008-07-31
| | | | | | | | | | | 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
* Oops... the trunk behaviour is differentGravatar glondu2008-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update test-suite outputGravatar glondu2008-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in docGravatar glondu2008-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport r11289.Gravatar msozeau2008-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typoGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use COQINSTALLPREFIX for doc tooGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bashism in test-suite/checkGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove pcoq from check prerequisitesGravatar glondu2008-07-28
| | | | | | | | 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
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
| | | | | | | generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix wrong environment bug in test for setoid_rewrite or rewrite.Gravatar msozeau2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11279 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
| | | | | | | 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
* Show configure choice for browser in CoqIDE preferencesGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11275 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now, -browser option is effective (and compiles)Gravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11273 85f007b7-540e-0410-9357-904b9bb8a0f7
* (Partially) Revert previous commit because of FTBFSGravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11272 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add -browser option to configure scriptGravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups (on refait le 11268 en mieux)Gravatar herbelin2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11270 85f007b7-540e-0410-9357-904b9bb8a0f7
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
| | | | | | | | | | | | | | | 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
* - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecGravatar herbelin2008-07-26
| | | | | | | | | paramètres - ce qui satisfait la requête #1899 - et only parsing), en attendant l'avis de Pierre. - Des "points finals" manquants dans himsg.ml (cf 11230). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite 11266 (warning tools/gallina.ml)Gravatar herbelin2008-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11267 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
| | | | | | | | | | | | | | | | | contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #1904 (instances of evars were no longer substituted sinceGravatar herbelin2008-07-25
| | | | | | | | the context of fixpoint was typechecked binder per binder and not as whole) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11265 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better test for relations being setoids or not: do leibniz rewrite iffGravatar msozeau2008-07-25
| | | | | | | the applied relation is an abbreviation for @eq. Fixes bug #1915. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11264 85f007b7-540e-0410-9357-904b9bb8a0f7
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
| | | | | | | destruction of records as a lot of scripts currently rely on it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11263 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
| | | | | | | after all... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11259 85f007b7-540e-0410-9357-904b9bb8a0f7
* A (safe) implementation of prolog's cut in the typeclasses eauto to avoidGravatar msozeau2008-07-24
| | | | | | | | | redoing proofs for nothing, i.e, do not backtrack on proofs whose evars are disjoint from the evars of the rest of the goals. Fixes the example in bug #1911, needs some more testing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1913, checking for unresolved evars which aren't obligations.Gravatar msozeau2008-07-24
| | | | | | | Also check mutuality of fixpoints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11257 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed loop in dependency fold of the checkerGravatar barras2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11256 85f007b7-540e-0410-9357-904b9bb8a0f7
* moved magic numbers to configure (share coq/coqchk)Gravatar barras2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11254 85f007b7-540e-0410-9357-904b9bb8a0f7
* broke cyclic dependenciesGravatar barras2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 11236Gravatar notin2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation de l'information "strict" (càd à toplevel ou en train deGravatar herbelin2008-07-24
| | | | | | | | | | définir une ltac) dans l'interprétation des identificateurs isolés en position de tactiques, comme dans "let x:=y in t" (résoud l'incompatibilité #1906). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
| | | | | | | | | | | opportunity to extend the class of singleton types to (possibly mutual) recursive types with single constructors of which all arguments are in Prop. This covers Acc. Acc_rect can consequently be defined in the direct way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
| | | | | | | | Jean-Marc, feel free to check I've not broken anything concerning coqdoc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oops... forgot some debug code.Gravatar msozeau2008-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11245 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
| | | | | | | | | | terms and [head_of_constr id] to put the head of a constr in some new hypothesis. Both are used in a new tactic to deal with partial applications in setoid_rewrite. Also fix bug #1905 by using [subrelation] to take care of [Morphism (R ==> R') id] constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11244 85f007b7-540e-0410-9357-904b9bb8a0f7
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
| | | | | | | | | | | It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed by not destructing objects of record types. The new [intuition] was also pulling an unneeded dependency in Field_theory which can be cleared easily. Zis_gcd_bezout is also considered a conjunction now, which seems correct(?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
| | | | | | | | | setting "Set Manual Implicit Arguments" for manual-only implicits. Fix test-suite script. This removes the discharge_info argument of "dynamic" object's rebuild function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli lors du commit #11236Gravatar notin2008-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 11236Gravatar notin2008-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: better dependency computation (after optimisations)Gravatar letouzey2008-07-20
| | | | | | | | | | | | | | | | | | When doing monolithic extraction, the initial dependency graph may turn to be too broad thanks to later optimisations. We now do an extra dependency pass at the end, killing more useless code. In addition, when doing an "Extract Constant t => ...", if t isn't an axiom, we don't include the dependencies of the body of t. This may break earlier extraction setups (with or without Extract Constant), since they may take advantage of objects that were earlier "wrongly" included in the extracted code. The fix is simple : just add these missing objects to the extraction command-line. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11239 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
| | | | | | | - Divers: message d'erreur et typo relatifs au langage déclaratif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
| | | | | | | | effacé dans un intro-pattern (suggéré par ssreflect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 18:50:45 +0000