aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Changement de catch_error pour qu'il rattrape les erreurs d'arguments Gravatar aspiwack2008-06-27
| | | | | | | | | | | | | | | | | | | | implicites. On peut désormais utiliser le fait que des arguments implicites ne sont pas inférés pour backtracker dans des preuves. C'est utile en particulier avec les typeclasses, mais peut servir dans d'autres cas. Le code suivant ne fait donc aucune erreur : Definition toto {x:True} := True. Goal True. try apply toto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Logo Coq dans coqideGravatar notin2008-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11182 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvaise dépendance dans Makefile.docGravatar notin2008-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli lors de la révision #11177Gravatar notin2008-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11179 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some work on BigQ :Gravatar letouzey2008-06-25
| | | | | | | | | | | * keep only one implementation of BigQ * QMake (ex-Q0Make) becomes functorial * proofs in it have been reworked, some new functions (e.g. red, power) * BigQ.t is declared to be a setoid and a field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #11175 de la branche v8.2 vers le trunkGravatar notin2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Installation de la documentationGravatar notin2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Micromega : bugs fixes - renaming of tactics - documentationGravatar fbesson2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in documentation (isn't it?)Gravatar glondu2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les contraintes d'univers sont maintenant collectées dans le champs ↵Gravatar soubiran2008-06-25
| | | | | | mod_constraints des modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Catch a Not_found exception in the Combined Scheme mechanism to hide an uglyGravatar vsiles2008-06-24
| | | | | | | | Anomaly with a better error message git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ fichiers spécifiques trunkGravatar herbelin2008-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
| | | | | | | Change from named_context to rel_context for class params and fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction petit bug sur révision 11159 (res_pf fait un effet de bordGravatar herbelin2008-06-21
| | | | | | | sur le sigma, utilisation de refine à la place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1889, correct globalization in class declarations.Gravatar msozeau2008-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11160 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)Gravatar herbelin2008-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various improvements in handling of evars in general and typingGravatar msozeau2008-06-21
| | | | | | | | | | | | | | | | | | | | | | | constraints in Program: - normalize types and defs of local fixpoints before checking the guardness condition to avoid having to give type annotations, e.g: << Definition fold (A B : Set) (f : B -> A -> B) : B -> tree A -> B := fix aux acc t := match t with | Leaf x => f acc x | Node l => fold_left aux l acc end. >> - add new inh_coerce_to_prod to allow coercion of the typing constraint to a product before trying to split it. It's a noop in standard mode, and forgets subsets in Program. Allows to typecheck: << (λ x, x) : { f : nat -> nat | ... } >>. - Better handling of the "abstract" typing constraints in Program. - Correctly normalize w.r.t. evars. the tycon given by users in Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11156 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo in a commentGravatar letouzey2008-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fixes: print unbound variable in error message (patch by SamuelGravatar msozeau2008-06-19
| | | | | | | | 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
* incomplete bugfix for infoGravatar corbinea2008-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11149 85f007b7-540e-0410-9357-904b9bb8a0f7
* removed unwanted linebreaks in pretty printingGravatar corbinea2008-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
| | | | | | | | (résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in subtac:Gravatar msozeau2008-06-18
| | | | | | | | | | | | - 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
* Compatibility fixes (Add Setoid bug and accidental introduction of aGravatar msozeau2008-06-18
| | | | | | | tactic named "app"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11139 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleur gestion de la fonction de "cache" des alias (declaremods), et ↵Gravatar soubiran2008-06-18
| | | | | | correction d'un bug sur Import/Export module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Detection de l'architecture sous Windows (et sans uname -o)Gravatar notin2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11137 85f007b7-540e-0410-9357-904b9bb8a0f7
* Où l'on se débarrasse de uname -oGravatar notin2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
| | | | | | | discharge time. Also fix bug when loading modules containing classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup in subtac_cases, preparing to use improvements on return predicateGravatar msozeau2008-06-17
| | | | | | | | | 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
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
| | | | | | | Morphism/Relation bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
| | | | | | | | unsatisfiable constraints. Add a resolution call in tacinterp before trying the default tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
| | | | | | | | | | | | | | disambiguate syntax: [ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x : nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will not parse. Add applicative contexts in tactics match, to be able to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
| | | | | | | | | | restriction du contexte était attendue) + suppression warning + amélioration affichage en cas de clause "at" incorrecte + report commit 11121 (correction bug 1367) de la 8.2 vers le trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11128 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: 2 problèmes de undo encore:Gravatar herbelin2008-06-13
| | | | | | | | | | | | - dans le "replay", l'état n'était pas correctement sauvegardé d'où une perte d'efficacité en cas de rejeux répétés, - bug de synchronisation dans le calcul de la pile des lemmes ouverts. + réajout de la variante standard de Set Printing All dans le menu display. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
| | | | | | | globals. Change program_simpl to use [auto] and not [auto with *]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numéros de version dans la docGravatar notin2008-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un problème lié à une interaction entre hyperref etGravatar notin2008-06-12
| | | | | | | | | | | | | latex, qui empechait de produire des fichiers .dvi à partir des .tex générés par coqdoc. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/tools/coqdoc/coqdoc.sty M branches/v8.2/tools/coqdoc/coqdoc.sty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing the definitions of pred and minus in the style of GGGravatar werner2008-06-12
| | | | | | | | in order for them to preserve the structural order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction parser révélé par test-suiteGravatar herbelin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation WindowsGravatar notin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des 'cp' et 'mkdir' par 'install'Gravatar notin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Confusion sur commit précédent de library. La capture du Not_foundGravatar herbelin2008-06-12
| | | | | | | | | | dans la recherche du nom long était bien utile (parce que la table des filename n'est plus synchronisée et plus dans le initial.coq) mais c'est ailleurs qu'on reposait à tort sur la bonne synchronisation de la table des noms longs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11111 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans l'adaptation de library_full_filename lors du débranchementGravatar herbelin2008-06-11
| | | | | | | | des filename hors reset (r11077). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug alias d'alias.Gravatar soubiran2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'export des .cmi dans coq_makefileGravatar notin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 04:43:32 +0000