aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Numbers: BigN and BigZ get instantiations of all properties about div and modGravatar letouzey2010-01-08
* * Segmenttree: New. A very simple implementation of segment trees.Gravatar regisgia2010-01-08
* Numbers: axiomatization + generic properties of abs and sgn.Gravatar letouzey2010-01-08
* Init/Logic: commutativity and associativity of /\ and \/Gravatar letouzey2010-01-08
* NZAxioms plus a compare allows to build an OrderedTypeGravatar letouzey2010-01-08
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Numbers: separation of funs, notations, axioms. Notations via module, without...Gravatar letouzey2010-01-07
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...Gravatar letouzey2010-01-07
* MSetInterface: more modularityGravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O...Gravatar letouzey2010-01-07
* misc improvements in some Structures filesGravatar letouzey2010-01-07
* MSetAVL: hints made local since some of them are quite violent (transitivity)Gravatar letouzey2010-01-07
* Allowed handling of partly-applied record constructors. (Fix for bug #2196.)Gravatar gmelquio2010-01-06
* Patch on subtyping check of opaque constants.Gravatar soubiran2010-01-06
* "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...Gravatar letouzey2010-01-06
* Numbers abstract layer: more Module Type, used especially for divisions.Gravatar letouzey2010-01-05
* use TIMECMD instead of TIME in makefile (unix cmd time reads its format in TIME)Gravatar letouzey2010-01-05
* Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/NumbersGravatar letouzey2010-01-05
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
* Division in Numbers: proofs with less auto (less sensitive to hints, in parti...Gravatar letouzey2010-01-05
* Division in Numbers: factorisation of signaturesGravatar letouzey2010-01-05
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Few misc. updates.Gravatar herbelin2010-01-04
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
* The following script was rasing an errorGravatar soubiran2010-01-04
* Fix bug in last commit, missing a substitution call.Gravatar msozeau2010-01-02
* Fix handling of instance declarations in presence of let-ins (bugGravatar msozeau2010-01-01
* Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).Gravatar herbelin2009-12-30
* Fixing bug #2156 (non positive occurrence error message displayed "Rel"'s).Gravatar herbelin2009-12-30
* Fixing bug #2193: computation of dependencies in the "match" returnGravatar herbelin2009-12-30
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* Renouncing to have the option "Automatic Introduction" on by default.Gravatar herbelin2009-12-29
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
* Fixing precedence while printing patterns in Ltac (was modified in r12607)Gravatar herbelin2009-12-29
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Moved a bit further the code for pattern interpretation in match goalGravatar herbelin2009-12-23
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
* Patches and instructions to enable Input Method support in CoqIDE.Gravatar vgross2009-12-21
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
* * Rewrite [classify_unicode] using standard unicode tables.Gravatar regisgia2009-12-20
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 11:43:05 +0000