aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - Amélioration de la présentation de RIneq, même si un nettoyage desGravatar herbelin2008-04-04
| | | | | | | | | | 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
* Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiGravatar herbelin2008-04-04
| | | | | | | n'était pas encore fait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai d'un peu plus de conversion dans apply : suppression de laGravatar herbelin2008-04-03
| | | | | | | restriction de conversion sur les sous-termes seulement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10749 85f007b7-540e-0410-9357-904b9bb8a0f7
* New file FMapFullAVL containing the balancing proofs about FMapAVL:Gravatar letouzey2008-04-03
| | | | | | | | | | | | | | As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees is not necessary anymore for just fulfilling the Map interface. But we still want theses proofs to exists somewhere, since they ensure the correct efficiency of the FMapAVL operations. In addition, FSetFullAVL also contains the non-structural, ocaml-faithful version of compare. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ↵Gravatar soubiran2008-04-03
| | | | | | l'application du foncteur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10747 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un bug de coq_makefile sur les variables CAMLLIBS etGravatar notin2008-04-03
| | | | | | | | | | COQLIBS. - Ajout d'un message d'erreur si Camlp5 est compilé en mode strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework of FMapAVL inspired by recent changes of FSetAVL: Gravatar letouzey2008-04-03
| | | | | | | | | | | | | | | | | | * pure functions comes first, proofs are isolated in a sub-module * lazy (&&&) = if ... then ... else true instead of strict (&&) = andb * equal and compare done via continuations * a more clever map2_opt suggested by B. Gregoire: no more intermediate conversion to lists, some sub-functions can handle trivial situations, etc. * map2 is now done via map2_opt and another new iterator: map_option. By the way, this map_option allows to define easily an efficient filter function. Both map2_opt and map_option are currently not available through FMapInterface.S, but they can be used by direct reference to the underlying Raw module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgts mineurs:Gravatar herbelin2008-04-03
| | | | | | | | | | - correction commit incorrect d'une modif de test-suite/success/apply.v - réorganisation dev/ - renommage Print Modules en Print Libraries - $Id:$ dans g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch sur le typage d'un foncteur applique a un alias.Gravatar soubiran2008-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
| | | | | | | | | | | alleviate some problems with delta. Better precedence in lambda notation. Temporarily deactivate notations for relation conjunction, equivalence and so on, while we search for a better syntax and maybe a generalization (fixes bug #1820). Better destruct_call in Program.Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
| | | | | | | | | | | | whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo affichage "simple apply"Gravatar herbelin2008-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
| | | | | | | | pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish enhancemenent of return clause inference from tycons, integratingGravatar msozeau2008-04-01
| | | | | | | | | | the previous trick of prepare_predicate_from_tycon: if a matched term is dependent, does not appear in the tycon but one of its real arguments is a variable which appears in the tycon, we can transport this dependency in the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10737 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enhance handling of parameters in typeclass constraints: permit to specify ↵Gravatar msozeau2008-04-01
| | | | | | | | | | | | any typeclass parameter by name anywhere in a typeclass constraint. This allows to share implementations easily and to give any subset of the parameters in any order in the constraints, whereas we are still restricted to a prefix of the typeclass parameters context when using "positional" specifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add option to set the opacity of obligations to transparent, to be ableGravatar msozeau2008-04-01
| | | | | | | to reduce proofs (requested by users). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1819Gravatar notin2008-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10734 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix for rewriting under dependent products.Gravatar msozeau2008-03-31
| | | | | | | | - Use support for abbreviations with params added by Hugo for inverse. - Standard priorities for operators on relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 10730: MAJ xlate.mlGravatar herbelin2008-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications diverses et variées :Gravatar herbelin2008-03-30
| | | | | | | | | | | | | - Nouvel essai de prise en compte unfold dans apply (unification.ml) - Correction bug commit précédent (constrintern.ml) - Correction bug d'explication des evars non résolues (evarutil.ml) - Fenêtre de query coqide plus large (command_windows.ml) - Orthographe tauto (tauto.ml4) - Crédits (ConstructiveEpsilon.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
| | | | | | | | Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite files, change conflicting notation "->rel" and the othersGravatar msozeau2008-03-29
| | | | | | | | | | to "-R>" and the like. Split more precisely in inference of case predicate between the new code which currently works only for matched variables and the old one which works better on variables appearing in matched terms types (the two could also be merged). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | Add definitions of relational algebra in Classes/RelationClasses including equivalence, inclusion, conjunction and disjunction. Add PartialOrder class and show that we have a partial order on relations. Change SubRelation to subrelation for consistency with the standard library. The caracterization of PartialOrder is a bit original: we require an equivalence and a preorder so that the equivalence relation is equivalent to the conjunction of the order relation and its inverse. We can derive antisymmetry and appropriate morphism instances from this. Also add a fully general heterogeneous definition of respectful from which we can build the non-dependent respectful combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | | [in I] := t [return pred] in b", just as SSReflect does with let:. Change implementation: no longer a separate AST node, just add a case_style annotation on Cases to indicate it (if ML was dependently typed we could ensure that LetPatternStyle Cases have only one term to be matched and one branch, alas...). This factors out most code and we lose no functionality (win ! win !). Add LetPat.v test suite. - Slight improvement of inference of return clauses for dependent pattern matching. If matching a variable of non-dependent type under a tycon that mentions it while giving no return clause, the dependency will be automatically infered. Examples at the end of DepPat. Should get rid of most explicit returns under tycons. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionGravatar notin2008-03-28
| | | | | | | | d'un test non significatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10726 85f007b7-540e-0410-9357-904b9bb8a0f7
* - notations &&& and ||| equivalent to andb and orb, Gravatar letouzey2008-03-27
| | | | | | | | | | but with lazy behavior while (vm_)computing - FSetAVL.split has now a dedicated output type instead of ( ,( , )) - Some proof adaptations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
| | | | | | | | | | | | | | | | | | | - Better interface in constrintern w.r.t. evars used during typechecking - Add "unsatisfiable_constraints" exception which gives back the raw evar_map that was not satisfied during typeclass search (presentation could be improved). - Correctly infer the minimal sort for typeclasses declared as definitions (everything was in type before). - Really handle priorities in typeclass eauto: goals produced with higher priority (lowest number) instances are tried before other of lower priority goals, regardless of the number of subgoals. - Change inverse to a notation for flip, now that universe polymorphic definitions are handled correctly. - Add EquivalenceDec class similar to SetoidDec, declaring decision procedures for equivalences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites modifs dans la test-suite:Gravatar notin2008-03-26
| | | | | | | | | | | | | | | | | | | | | | | | test-suite/output/ZSyntax.out typo test-suite/bugs/closed/shouldsucceed/1776.v bug closed test-suite/success/extraction.v test-suite/success/extraction.v test-suite/bugs/closed/shouldsucceed/846.v backtrack sur le commit 10639 test-suite/bugs/closed/shouldsucceed/1322.v: petites modifications suite aux changement de setoid_replace test-suite/bugs/closed/shouldsucceed/1414.v: petites modifications suite aux changement dans Program git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans la gestion des dépendances vers les .mlGravatar notin2008-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10722 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et ↵Gravatar notin2008-03-26
| | | | | | coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees ↵Gravatar soubiran2008-03-26
| | | | | | | | | en-dehors du noyau et sont donc independantes des substitutions engendrees par les alias de module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des dépendances des .mlGravatar notin2008-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
| | | | | | | | engendrees par les alias de module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans la gestion des 'Declare ML Module'Gravatar notin2008-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
| | | | | | | | context [] pattern). May break some user contribs... Rename clsubstitute to substitute. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish fix in command where we still lost information on what was a typeGravatar msozeau2008-03-24
| | | | | | | | and needed coercions. Change API of interp_constr_evars to get an optional evar_defs ref argument. Makes Algebra compile again (at least). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix examples in Program documentation and add comindexes for the variousGravatar msozeau2008-03-23
| | | | | | | | commands. Update documentation of implicit arguments with the new syntax and an explanation for the way it works in inductive type definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
| | | | | | | | | | | | | | types. Change (again) the semantics of bindings and the binding modifier ! in typeclasses. Inside [ ], implicit binding where only parameters need to be given is the default, use ! to use explicit binding, which is equivalent to regular bindings except for generalization of free variables. Outside brackets (e.g. on the right of instance declarations), explicit binding is the default, and implicit binding can be used by adding ! in front. This avoids almost every use of ! in the standard library and in other examples I have. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Wf.v et unification (suite remarques faites sur cocorico)Gravatar herbelin2008-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.Gravatar herbelin2008-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les réels:Gravatar herbelin2008-03-23
| | | | | | | | | | | | | | | | | | | | | | | | - 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
* CoqIDE default font set to monospace so as indentation to be meaningfulGravatar herbelin2008-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility fixes, backtrack on definitions of reflexive,Gravatar msozeau2008-03-22
| | | | | | | | | | | | | symmetric... classes for now, merging Relations with RelationClasses requires some non-trivial changes on implicits but also some definitions are different (e.g. antisymmetric in Classes is defined w.r.t an equivalence relation and not eq). Move back to Reflexive and so on. reflexivity-like tactics fail in the same way as before if Setoid was not imported. There is now a scope for morphism signatures, hence "==>", "++>" and "-->" can be given different interpretations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10708 85f007b7-540e-0410-9357-904b9bb8a0f7
* One more AVL reorganisation: separate pure functions from proofs + ↵Gravatar letouzey2008-03-21
| | | | | | | | | | | | | functional scheme. - Proofs are placed in Raw.Proofs, that may someday become an opaque module. - use Functional Scheme in this module Raw.proofs, instead of Function: less derived objects. - more cleanup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct bug introduced in r10589, where we lost information thatGravatar msozeau2008-03-21
| | | | | | | | | | assumption types are types when type-checking them and necessary coercions were not inserted. Add empty_evar_defs definition in Evd and call the new helper function in constrintern that performs interpretation and gives back implicit argument information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some "if then else" instead of orb and andb, in order to vm_compute lazilyGravatar letouzey2008-03-21
| | | | | | | | | | | Extraction is unchanged, since orb/andb are detected as un-strict functions and inlined. This only prevents the use of some potential clever Extract Inlined Constant andb => "(&&)" and idem for orb, but this isn't a big deal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control rewriting under lambdas. Otherwise makes someGravatar msozeau2008-03-20
| | | | | | | | | | | | rewrite calls fail because an occurence is found under a lambda that was not found before and there are no adequate morphism declarations to make the rewrite succeed nor the possibility to give occurences to rewrite (yet). Only setoid_rewrite will try rewriting under lambda's for now. Example problem found in a port of the Random library. Also improved the required_library error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Installation des .vo nécessaire à BigQGravatar notin2008-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug sur les modules de la forme:Gravatar soubiran2008-03-20
| | | | | | | | | | Module F (X : S) : F_sig X. ... End F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10702 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-17 21:47:46 +0000