aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* MSetInterface: more modularityGravatar letouzey2010-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12637 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff ↵Gravatar letouzey2010-01-07
| | | | | | with Inline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
* DecidableType2+OrderedType2 : notations in specific Module Type, slicing of ↵Gravatar letouzey2010-01-07
| | | | | | | | | | | | | | | | OrderedType2 OrderedType2 is reorganized in atomic module type following the same approach used for DecidableType2. We use the following convention: module type Foo' is exactly module type Foo, except that some notations may have been added. In functor arg, we can use Foo or Foo' depending on whether we want nice notation or not. Note that any implementation of Foo is accepted as implementation of Foo' :-). For the moment, these notations are not placed in specific scopes, I think it isn't useful, but I may be wrong, we'll see later when using them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12635 85f007b7-540e-0410-9357-904b9bb8a0f7
* misc improvements in some Structures filesGravatar letouzey2010-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12634 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetAVL: hints made local since some of them are quite violent (transitivity)Gravatar letouzey2010-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12633 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowed handling of partly-applied record constructors. (Fix for bug #2196.)Gravatar gmelquio2010-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch on subtyping check of opaque constants.Gravatar soubiran2010-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12631 85f007b7-540e-0410-9357-904b9bb8a0f7
* "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ↵Gravatar letouzey2010-01-06
| | | | | | | | by ...") Application in some proofs of Numbers's abstract division git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers abstract layer: more Module Type, used especially for divisions.Gravatar letouzey2010-01-05
| | | | | | | Properties are now rather passed as functor arg instead of via Include or some inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
* use TIMECMD instead of TIME in makefile (unix cmd time reads its format in TIME)Gravatar letouzey2010-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/NumbersGravatar letouzey2010-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
| | | | | | | | This used to be convenient in FSets, but since we now try to integrate DecidableType and OrderedType as foundation for other part of the stdlib, this should be avoided, otherwise some eauto take a _long_ time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Division in Numbers: proofs with less auto (less sensitive to hints, in ↵Gravatar letouzey2010-01-05
| | | | | | particular about eq) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Division in Numbers: factorisation of signaturesGravatar letouzey2010-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
| | | | | | | | | NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Few misc. updates.Gravatar herbelin2010-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12621 85f007b7-540e-0410-9357-904b9bb8a0f7
* The following script was rasing an errorGravatar soubiran2010-01-04
| | | | | | | | | | | | | | | | | | | | | | | | Require Export FSets FMaps. Require FMapAVL. (* avl ou listes : aucun impact pour l'instant... *) Module FMap := FMapList. Module FMapHide (X : FMapInterface.S). Include X. End FMapHide. Module State := Nat_as_OT. Module StateMap' := FMap.Make(State). Module StateMap := FMapHide StateMap'. Module LabelMap := StateMap. About LabelMap.MapsTo. (*cannot print global_reference ....*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in last commit, missing a substitution call.Gravatar msozeau2010-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12619 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix handling of instance declarations in presence of let-ins (bugGravatar msozeau2010-01-01
| | | | | | | reported by Eelis van der Weegen). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).Gravatar herbelin2009-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2156 (non positive occurrence error message displayed "Rel"'s).Gravatar herbelin2009-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2193: computation of dependencies in the "match" returnGravatar herbelin2009-12-30
| | | | | | predicate was incomplete. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
| | | | | | | | | | In trunk the different possible combinations of "at" and "in" with occurrences are taken into account. In 8.2 branch, it remains fragile (syntaxes that were accepted remain accepted and a message warns if the occurrences coming after the "with" are not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renouncing to have the option "Automatic Introduction" on by default.Gravatar herbelin2009-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
| | | | | | | what allows to better control position of side-conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing precedence while printing patterns in Ltac (was modified in r12607)Gravatar herbelin2009-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
| | | | | | | | | | | | | | | | | | general_multi_multi_rewrite. Due to the option "!" of rewrite, a lemma may need to be interpreted several times with different instances of the implicit arguments. Interpreting the term as a constr in tacinterp.ml would need to either refresh the holes (i.e. the evars) or detype what has been typed and in both cases, complicated things can happen because the evars associated to these holes may have been used in instantiating former evars of the goal. Leaving the term as a rawconstr would need to export the interpretation functions from tacinterp which is technically complicated in the current situation because equality.ml is currently linked before tacinterp. The solution used is to delay the interpretation using an ML closure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
| | | | | | | | | Class" too to handle references instead of just idents. Minor fix in coqdoc. zeta-normalize setoid_rewrite proofs, removing useless let-bindings generated by the tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved a bit further the code for pattern interpretation in match goalGravatar herbelin2009-12-23
| | | | | | | | | to anticipate support of possibly-typed patterns; Also removed a useless nf_evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patches and instructions to enable Input Method support in CoqIDE.Gravatar vgross2009-12-21
| | | | | | | TODO: don't patch the ELatin IM, create a separate IM or push the patch upstream. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
| | | | | | | | | no longer considered a progress (this prepares generally having tactics with arguments that contains holes that are added to the goal sigma). Incidentally, made that "clear" now restricts evars only if the restriction is really needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12602 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Rewrite [classify_unicode] using standard unicode tables.Gravatar regisgia2009-12-20
| | | | | | | | (This should be a conservative extension of the old version.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
| | | | | | | | (e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of useless eta-redexes during type class instance resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
| | | | | | | types so that the type of terms in Genarg can be changed w/o in full independence of the level. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12599 85f007b7-540e-0410-9357-904b9bb8a0f7
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
| | | | | | | As a consequence, revert to some pedestrian proofs of Equivalence here and there, without the need for the Measure class. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Const_omega: look for S in Init only (avoid future clash with S of Numbers)Gravatar letouzey2009-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12597 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZOdiv: fully use generic properties from ZDivTrunc.vGravatar letouzey2009-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverse order of arguments in min_case_strong for better uniformity (and ↵Gravatar letouzey2009-12-17
| | | | | | compatibility...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Division in Numbers : more properties, new filenames based on a paper by R. ↵Gravatar letouzey2009-12-17
| | | | | | | | | | | | | | Boute Following R. Boute (paper "the Euclidean Definition of the Functions div and mod"): - ZDivFloor.v for Coq historical division (former ZDivCoq.v) - ZDivTrunc.v for Ocaml convention (former ZDivOcaml.v) - ZDivEucl.v for "Mathematical" convention 0<=r (former ZDivMath.v) These property functors are more or less finished (except that sign and abs stuff should be migrated to a separate file). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12594 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de la nouvelle option pour functional inductionGravatar jforest2009-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12593 85f007b7-540e-0410-9357-904b9bb8a0f7
* adding an option functional_induction_rewrite_dependent to make functional ↵Gravatar jforest2009-12-16
| | | | | | induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Division in Numbers: more properties proved (still W.I.P.)Gravatar letouzey2009-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12591 85f007b7-540e-0410-9357-904b9bb8a0f7
* A generic euclidean division in Numbers (Still Work-In-Progress)Gravatar letouzey2009-12-15
| | | | | | | | | | | - For Z, we propose 3 conventions for the sign of the remainder... - Instanciation for nat in NPeano. - Beginning of instanciation in ZOdiv. Still many proofs to finish, etc, etc, but soon we will have a decent properties database for all divisions of all instances of Numbers (e.g. BigZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
* file integrated into the archive by mistakeGravatar letouzey2009-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Description of the new features of the module system (part two).Gravatar soubiran2009-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12588 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 19:30:42 +0000