aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - 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
* still some useless invariants in FSetAVLGravatar letouzey2008-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10701 85f007b7-540e-0410-9357-904b9bb8a0f7
* some references to IntMap forgotten in last commitGravatar letouzey2008-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10700 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of the old IntMap library from StdLib to a user contrib ↵Gravatar letouzey2008-03-19
| | | | | | (Cachan/IntMap) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq.Relations.Relations can move back to its short nameGravatar letouzey2008-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10698 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
| | | | | | | | | | | | | | | | | | | | | | | names, gives the ability to specify qualified classes in instance declarations. Use that in the class_tactics code. Refine the implementation of classes. For singleton classes the implementation of the class becomes a regular definition (into Type or Prop). The single method becomes a 'trivial' projection that allows to launch typeclass resolution. Each instance is just a definition as usual. Examples in theories/Classes/RelationClasses. This permits to define [Class reflexive A (R : relation A) := refl : forall x, R x x.]. The definition of [reflexive] that is generated is the same as the original one. We just need a way to declare arbitrary lemmas as instances of a particular class to retrofit existing reflexivity lemmas as typeclass instances of the [reflexive] class. Also debug rewriting under binders in setoid_rewrite to allow rewriting with lemmas which capture the bound variables when applied (works only with setoid_rewrite, as rewrite first matches the lemma with the entire, closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal [exists x, P (f x)]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique gappaGravatar filliatr2008-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various improvements of coqdep, resulting in a big speedupGravatar letouzey2008-03-19
| | | | | | | | | | | | | | | | | | | | * use of Hashtbl for large sets/maps * reorganisation of directory-traversal functions, in order to avoid redundant stat / open * all files and directory whose names start by . are skipped while tranversing directories: no more visits of .svn ! * new option -boot to be used when computing dependencies of the stdlib: - no need in this case to records the system .vo in coqlibKnown - add directly inside coqdep the equivalent of -R theories Coq and -R contrib Coq As a result, coqdep'ing all the .vo of the stdlib now takes 25s on my machine instead of 2min30 earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implementation of rewriting under lambdas. Tested on exists only.Gravatar msozeau2008-03-18
| | | | | | | | | Adds some instances that incur again a small performance penalty because they cannot be discriminated against for now (the discrimination net is considering the head constructor to be Morphism). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a function to rebuild an elim scheme from elim_scheme_info. WillGravatar courtieu2008-03-18
| | | | | | | use it for elim principle type generation from merged graphs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hint for Debian users.Gravatar glondu2008-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10692 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved the implementation of rtreeGravatar barras2008-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10691 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 ↵Gravatar barras2008-03-18
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct implementation of normalization of signatures using setoidGravatar msozeau2008-03-18
| | | | | | | | rewriting, in some sense bootstrapping the system. Remove redundant morphisms for now to test for completeness (small performance penalty). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10689 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Small change in the make_eq_decidability call : the functions does not (yet)Gravatar vsiles2008-03-18
| | | | | | | | | work on mutual inductive types so if we can't compute it, we discard it but keep the boolean equality declaration which is ok even on mutuals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the possibility of specifying constants to unfold for typeclassGravatar msozeau2008-03-17
| | | | | | | | | | | | | | | | | | | | | resolution. Add [relation] and Setoid's [equiv] as such objects. Considerably simplify resolve_all_evars for typeclass resolution, adding a further refinement (and hack): evars get classified as non-resolvable (using the evar_extra dynamic field) if they are turned into a goal. This makes it possible to perform nested typeclass resolution without looping. We take advantage of that in Classes/Morphisms where [subrelation_tac] is added to the [Morphism] search procedure and calls the apply tactic which itself triggers typeclass resolution. Having [subrelation_tac] as a tactic instead of an instance, we can actually force that it is applied only once in each search branch and avoid looping. We could get rid of the hack when we have real goals-as-evars functionality (hint hint). Also fix some test-suite scripts which were still calling [refl] instead of [reflexivity]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10687 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Factorizing code : context_chop was used in several files (even as ↵Gravatar vsiles2008-03-17
| | | | | | | | | | | chop_context) so I moved it to termops.ml * Fixing a little bug in the Boolean to Leibniz transition in automatic boolean declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed unneeded tactics from RelationClasses. UseGravatar msozeau2008-03-16
| | | | | | | | check_required_library where needed (fixes bug #1797). Remove spurious messages from ring when not in verbose mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
| | | | | | | | | | | setoid rewrite. Refine and use the new unification flags setup by Hugo to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean indicating conversion is wanted to a Cpred representing the constants one wants to get unfolded to have more precise control. Add corresponding test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10684 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 04:44:44 +0000