aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Adding Acc_intro_generator in order to help computations of Function in ↵Gravatar forest2013-11-20
| | | | particular
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
| | | | | | When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore Zsqrt compat now that refine works fine with match.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17021 85f007b7-540e-0410-9357-904b9bb8a0f7
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
| | | | | | | | | | | It now uses the same algorithm as pretyping does. This produces pretty weird goal when refining pattern matching terms. Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now. The file Zsqrt_compat.v has two temporary [Admitted] related to this issue. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
| | | | | | | | | new Axiom in Logic.v, proof_admitted : False. admit now simply cases proof_admitted and does not create a new Axiom in the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in definition clos_reflGravatar ppedrot2013-07-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3089. This implied tweaking the definition of the lexicographicGravatar ppedrot2013-07-26
| | | | | | | | product of lists, hence possibly introducing incompatibilities. Parts of the patch by Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a concat function to List theory. Strangely, it was missing.Gravatar ppedrot2013-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16633 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
| | | | | | ... no need to Unset them manually git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 85f007b7-540e-0410-9357-904b9bb8a0f7
* More dynamic argument scopesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
| | | | | | | | | | | | | - hypotheses are introduced in the left-to-right order - intropatterns have to match the number of generated hypotheses, and, if less, new introduction names are automatically generated - clearing the hypothesis on which injection is applied, if any. However, this is a source of incompatibilities (for a variant of injection that is hopefully not used a lot). Compatibility can be restored by "Unset Injection L2R Pattern Order". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving printing of 'rew' notationGravatar herbelin2013-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxing the constraint on eta-expanding on the fly while looking forGravatar herbelin2013-05-05
| | | | | | | | | | | notation to use at printing time. We now allow to print "sigT P" as "{x:_ & P x}", generating a "_" for the missing type, when the notation is defined by 'Notation "{ x : A & P }" := (sigT (fun x:A => P))'. Do better, and change the notation to "(sigT (A:=A) (fun x => P))" so that the type is known even when eta-expansion is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added group properties of eq_refl, eq_sym, eq_transGravatar herbelin2013-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Normalized type for Vector.map2Gravatar pboutill2013-03-25
| | | | | | fix CoRN but there must be an underlying bug ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16355 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16350 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
| | | | | | | | Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
* cbn friendly VectorDefGravatar pboutill2013-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16245 85f007b7-540e-0410-9357-904b9bb8a0f7
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
| | | | | | | | | | The offending functor in NZOrder wasn't actually used, so I've commented it for now. Btw, the Not_found in coqchk is now turned into something slightly more informative git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
| | | | | | | | It is much beter for everything (includind guard condition and simpl refolding) excepts typeclasse inference because unification does not recognize (fun x => f x b) a when it sees f a b ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
| | | | | | | | | | | | | | | | | | | | | | | Inner sub-modules with "Definition t := t" is hard to handle by extraction: "type t = t" is recursive by default in OCaml, and the aliased t cannot easily be fully qualified if it comes from a higher unterminated module. There already exists some workarounds (generating Coq__XXX modules), but this isn't playing nicely with module types, where it's hard to insert code without breaking subtyping. To avoid falling too often in this situation, I've reorganized: - GenericMinMax : we do not try anymore to deduce facts about min by saying "min is a max on the reversed order". This hack was anyway not so nice, some code was duplicated nonetheless (at least statements), and the module structure was complex. - OrdersTac : by splitting the functor argument in two (EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid the need for aliasing the type t, cf NZOrder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16100 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
| | | | | | | hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making subset_eq_compat applying over more general domain "Type" (see #2938).Gravatar herbelin2012-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
| | | | | | | | | | themselves satisfied Uniqueness of Identity Proofs. Otherwise said uniqueness of equality proofs is enough to characterize types whose equality has a degenerated "homotopical" structure (this is a short proof of a result inspired by Voevodsky's proof of inclusion of h-level n into h-level n+1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolating the ingredients of the proof of Prop<>Type (r15973). SeeingGravatar herbelin2012-11-15
| | | | | | | it as a consequence of the derivability of Hurkens' paradox in the presence of a retract from Type to Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some lemmas on property of rewriting. It will probably be worth atGravatar herbelin2012-11-15
| | | | | | | some time to provide a library stating the groupoid structure of equality proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a proof that Prop<>Type, for arbitrary fixed Type.Gravatar herbelin2012-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15973 85f007b7-540e-0410-9357-904b9bb8a0f7
* A decidability property of functional relations over decidable codomains.Gravatar herbelin2012-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15972 85f007b7-540e-0410-9357-904b9bb8a0f7
* For the record, two examples of short proofs of uniqueness of identityGravatar herbelin2012-11-15
| | | | | | proofs, on bool and nat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
| | | | | | | | | | | | | instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed a few calls to "Opaque" in Logic.v ineffective since at leastGravatar herbelin2012-10-24
| | | | | | V7.1. Thanks to Assia for reporting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
| | | | | | Thanks to F. Blanqui for spotting it out. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "En cours pour 'generalize in clause' et 'induction in clause'"Gravatar herbelin2012-10-04
| | | | | | Sorry, was committed mistakenly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15856 85f007b7-540e-0410-9357-904b9bb8a0f7
* En cours pour 'generalize in clause' et 'induction in clause'Gravatar herbelin2012-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15838 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT: a tail-recursive plengthGravatar letouzey2012-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Same for FinGravatar pboutill2012-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector equalities first stuffGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
| | | | | | | | | | | | After discovering a rewrite in Ergo that takes a loooong time due to a bad interaction with the instances of Permutation and PermutationA : - PermutationA is now in a separate file SetoidPermutation - File Permutation.v isn't Require'd by SetoidList anymore nor MergeSort.v, just the definitions in Sorted.v - Attempt to put a priority on these instances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
| | | | | | | | | | | | | | | | | | The ugly syntax "destruct x as [ ]_eqn:H" is replaced by: destruct x eqn:H destruct x as [ ] eqn:H Some with induction. Of course, the pattern behind "as" is arbitrary. For an anonymous version, H could be replaced by ?. The old syntax with "_eqn" still works for the moment, by triggers a warning. For making this new syntax work, we had to change the seldom-used "induction x y z using foo" into "induction x, y, z using foo". Now, only one "using" can be used per command instead of one per comma-separated group earlier, but I doubt this will bother anyone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two adaptations after the changes of level of ->Gravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15541 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore the compatibility notation Compare.not_eq_symGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15539 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:44:21 +0000