aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use dashed lines for equivalence edges in dot output of universesGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13785 85f007b7-540e-0410-9357-904b9bb8a0f7
* More coherent comment orderingGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix some typosGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13783 85f007b7-540e-0410-9357-904b9bb8a0f7
* ratrapage exception, deja fait ...Gravatar bgregoir2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing an uncaught exception bug with use of vmcastGravatar herbelin2011-01-07
| | | | | | (backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13781 85f007b7-540e-0410-9357-904b9bb8a0f7
* MacOS integrationGravatar pboutill2011-01-07
| | | | | | | if `pkg-config --exists ige-mac-integration`, coqide.opt will be able to open files by double-clik in finder on Darwin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Separate load_file handler in coqideGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide is not built with coqmktop any moreGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Don't install both coqide.byte and coqide.optGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13776 85f007b7-540e-0410-9357-904b9bb8a0f7
* Call coqtop with -nois when probing for filesGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix print in coqideGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13774 85f007b7-540e-0410-9357-904b9bb8a0f7
* mli comments for docGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13773 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGESGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)Gravatar letouzey2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove fake alpha-specific case in configureGravatar glondu2011-01-06
| | | | | | Its effect is the same as in the default case... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13769 85f007b7-540e-0410-9357-904b9bb8a0f7
* s/appartness/membership/g (Closes: #2470)Gravatar glondu2011-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted r13715 "Add improved indenters that rely on the current proof state ↵Gravatar gmelquio2011-01-06
| | | | | | | | to choose the indentation depth." It seems to be the cause for bug #2472. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove Safe_marshalGravatar glondu2011-01-06
| | | | | | | | | | | | Safe_marshal was using intermediate strings that are subject to Sys.max_string_length limitation. Use directly binary channel-oriented functions instead. This is a fix for bug #2471. Remark: this might reduce robustness w.r.t. noise in the communication channel. AFAIK, the original purpose of Safe_marshal was to work around a bug on Windows... this should be investigated further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
* f_equiv : a clone of f_equal that handles setoid equivalencesGravatar letouzey2011-01-04
| | | | | | | | | | | For example, if we know that [f] is a morphism for [E1==>E2==>E], then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv] into the subgoals [E1 x x'] and [E2 y y']. This way, we can remove most of the explicit use of the morphism instances in Numbers (lemmas foo_wd for each operator foo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
| | | | | | | | | | - a ltac solve_proper which generalizes solve_predicate_wd and co - using le_elim is nicer that (apply le_lteq; destruct ...) - "apply ->" can now be "apply" most of the time. Benefit: NumPrelude is now almost empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename the "raw" argument extension into "glob"Gravatar glondu2010-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13761 85f007b7-540e-0410-9357-904b9bb8a0f7
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
| | | | | | | | | | | | Rationale: the expansion ignores the TYPED clause when {RAW,GLOB}_TYPED are given. Indeed, in this case, the final type is a consequence of either "INTERPRETED BY" (if given), or the default one based on GLOB_TYPED. This avoids the pitfall of the "raw" argument extension, where the TYPED clause was unused and totally misleading. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsGravatar glondu2010-12-25
| | | | | | | | | | It is quite nasty to insert those open in places where they can change the semantics of surrounding code... instead, prefer using fully-qualified names in generated code when possible. For ExtraArgType, simulate a "open Extrawit in ..." (which does exist primitively in OCaml >= 3.12) with the usual encoding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
| | | | | | | | perl -pi -e 's/(mk)R(Ref|Var|Evar|PatVar|App|Lambda|Prod|LetIn|Case s|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic|Prop|Type|Fix|CoFix|Struct Rec|WfRec|MeasureRec)/\1G\2/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13758 85f007b7-540e-0410-9357-904b9bb8a0f7
* s/raw/glob/g in decl_interp.ml for more consistencyGravatar glondu2010-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13757 85f007b7-540e-0410-9357-904b9bb8a0f7
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
| | | | | | | | | perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename files in funind to respect new conventionsGravatar glondu2010-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
| | | | | | | By the way, definitely remove "Dump Universes", which has been deprecated since 2006 (r9306). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13754 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactics/eqdecide.ml4: avoid a useless argument in decideEqualityGravatar glondu2010-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Precision in documentation of "decide equality"Gravatar glondu2010-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
| | | | | | | | This variant was ignoring its second argument, and didn't exactly respect its documented specification. This is fixed by removing the variant altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13746 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix diagram in genarg.mliGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prepare change of nomenclature rawconstr -> glob_constrGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13742 85f007b7-540e-0410-9357-904b9bb8a0f7
* More precise documentation for instantiateGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
| | | | | | | | We now keep some type information in the "info" field of constructors and cases, and compact a match with some default branches (or remove this match completely) only if this transformation is type-preserving. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
| | | | | | | of "match" is not general enough; if there is a non dependent type constraint, we also try w/o inversion predicate in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: try to avoid a few lookup in the universe graphGravatar letouzey2010-12-18
| | | | | | | | | | | | | | | | | | | | Sometimes the same (repr g u) was done in different functions after being passed u as argument. We rather try to compute (repr g u) as soon as possible, and then pass it instead of u. Beware of sync issues : if g changes, arcu might become obsolete (cf. setlt, setleq, merge ...) Typical code around occurences of declare_univ was doing up to 3 lookups: - is u in g ? - if not we descend again in g to add it - and then later repr is called on the same u. With my safe_repr, we do one lookup if u is in g, and a lookup and an addition otherwise. Ok, declare_univ was rarely used, but it seems nicer this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
| | | | | | | | | No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert last commit 13723 on Univ : minor gains and more complex codeGravatar letouzey2010-12-18
| | | | | | | | | | | | | | | | The gains on contribs are quite small, around 3% max, apart from 3 small contribs where it's about 10% (corresponding to 10s each). With last patch, we add quicker lookup for universes in the graph (up to 5 times less calls to cmp_univ_level on an example), but probably more "administrative" work (i.e. addition of updated paths in the graphs, handling pairs of updated graphs and results in functions, etc), and some sharing might also have been lost since graphs changed more. Anyway, little gain and more complex code, let's remove this patch for now ... until the next attempt to speed-up the universe layer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: an attempt to lazily compact chains of Equiv in a functionnal wayGravatar letouzey2010-12-17
| | | | | | | | We'll see experimentally if this helps... A few more functions could be adapted (e.g. between), and an occurence of compare just discard the compacted graph (in compare_greater) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13723 85f007b7-540e-0410-9357-904b9bb8a0f7
* NPeano.modulo : another trick a la "minus" for having a decreasing argGravatar letouzey2010-12-17
| | | | | | | | | | By writing y instead of 0 in the branch where y is 0, Coq can see that (modulo x y) is a structural subterm of y (but not necessarily a strict one). Same trick for div, but here it doesn't help. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13722 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer log2 function for nat (suggested by Hugo)Gravatar letouzey2010-12-17
| | | | | | | | | | | | | | The auxiliary variable q is now increased continuously instead of being doubled from time to time. Interest: this version is obviously linear, and specification proofs are slightly simplier. NB: the previous version was in fact also linear I think, but proving this requires a proper complexity analysis. I'm sure this algorithm is related with some cellular automata stuff in the spirit of the firing squad :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: two improvements (speed + space)Gravatar letouzey2010-12-16
| | | | | | | | | | | | | - The "compare" function on universes (the one answering EQ|LT|LE|NLE) was launching "collect" for creating the transitive upward closure of u, and then checking if v is in it. We now proceed more lazily, by stopping creating the transitive closure as soon as v is found. - In univ_entry, the first arg u of Equiv(u,v) is removed. It can indeed be retrieved from the key of the universe graph leading to this Equiv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clenv.connect_clenv without its Evd.foldGravatar letouzey2010-12-15
| | | | | | | | | | | Apparently, it seems that clenv.evd is either created from dummy_goal (in (e)auto) or from a copy of gls (in class_tactics). I've checked experimentally by some assert that on the stdlib the defined part of clenv.evd is always included in gls. I hence propose to simplify this function connect_clenv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar-related speed-up and clarifications in Class_tactics and RewriteGravatar letouzey2010-12-15
| | | | | | | | | | | Some functions are restricted to consider only undefined evars, and some Evd.fold are replaced by Evd.fold_undefined. I'm less sure about the modifications in rewrite.ml4, but in pratice they seem to work well on the stdlib. I was planning to say assert false for Not_found in Rewrite.evd_of_existentials but some file of the stdlib doesn't like that (to be checked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13717 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-14 21:18:02 +0000