aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
| | | | | | | | components and resolving them separately, reporting more precise failures. Improve error messages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11105 85f007b7-540e-0410-9357-904b9bb8a0f7
* now Escape toggles query paneGravatar jnarboux2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11103 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ diversesGravatar herbelin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plutôt que de reposer sur le vernacexpr pour détecter les débuts deGravatar herbelin2008-06-11
| | | | | | | | | | buts, on se base sur les informations de Pfedit (comme le fait Pierre Courtieu). Permet d'être plus robuste sur les extensions de syntaxe ouvrant des buts, style Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11100 85f007b7-540e-0410-9357-904b9bb8a0f7
* escape key now hides paneGravatar jnarboux2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zpow_facts.Zmult_power: kills a useless hypothesisGravatar letouzey2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout query Locate dans coqide sur suggestion Arthur C.Gravatar herbelin2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11097 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.Gravatar herbelin2008-06-10
| | | | | | | - Test match dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
| | | | | | | | | | | | | | | - Changement au passage de la convention "at -n1 ... -n2" en "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut pas mélanger des positifs et des négatifs. - Au passage: - simplification de gclause avec fusion de onconcl et concl_occs, - généralisation de l'utilisation de la désignation des occurrences par la négative aux cas de setoid_rewrite, clrewrite et rewrite at, - correction d'un bug de "rewrite in at" qui utilisait le at de la conclusion dans les hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
* open and save buttons are the defaultGravatar barras2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11093 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-13 09:39:03 +0000