aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-27test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13805 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-27Make simpl use the proper constant when folding (mutual) fixpointsletouzey
Before this commit, when simpl was finding the constant name for folding some (mutual) fixpoint, this was done via some repr_con followed by make_con. Problem: this doesn't preserve the canonical part of a Names.constant. For instance the following script was buggish: Module M. Fixpoint foo n := match n with O => O | S n => bar n end with bar n := match n with O => O | S n => foo n end. End M. Module N. Include M. (* foo, bar have here "user name" N but "canonical name" M *) Eval simpl in (fun x => bar (S x)). (* Anomaly: uncaught exception Failure "Cannot print a global reference". *) (* since simpl has produce a different bar with both user and canonical N *) TODO : check all other uses of make_con in the rest of the sources... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13803 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-25Fix compilation with camlp5 (Closes: #2487)glondu
With hints from Daniel de Rauglaudre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13802 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-25Update .gitignoreglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13798 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-25Add a test for sorting all universes of stdlibglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-25Rewrite sort_universes to minimize the number of universesglondu
The whole standard library fits in 3 universes (instead of 22 with the previous algorithm). Very costy, time complexity: O(n^4) (if we assume map operations are done in constant time), with n being the number of universe variables. It takes ~35s for the whole stdlib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13796 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-20Numbers: simplier spec for testbitletouzey
We now specify testbit by some initial and recursive equations. The previous spec (via a complex split of the number in low and high parts) is now a derived property in {N,Z}Bits.v This way, proofs of implementations are quite simplier. Note that these new specs doesn't imply anymore that testbit is a morphism, we have to add this as a extra spec (but this lead to trivial proofs when implementing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13792 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-12Fix formatting issue in refmanglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13791 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Fix ocamlbuild-based build systemglondu
Caveat: in native code, if the executable is a symlink, Sys.executable_name points to the target of the symlink... this breaks coqide's way of locating coqtop. Workaround: make bin/coqide.opt a hardlink (or a copy) instead of a symlink. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13790 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Remove references to -ide option of coqmktopglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11In univ.ml, put universe_level primitives in its their own sub-moduleglondu
This is merely refactoring so that UniverseL{Map,Set} constructions appear nicely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13788 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Add [Typeclasses Debug] option that respects backtracking, solvemsozeau
regression in typeclass resolution not generating the proper subgoals (may break some contribs). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13787 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Add "Print Sorted Universes"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Use dashed lines for equivalence edges in dot output of universesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13785 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11More coherent comment orderingglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13784 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Fix some typosglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13783 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11ratrapage exception, deja fait ...bgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13782 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13781 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07MacOS integrationpboutill
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
2011-01-07Separate load_file handler in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13778 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Coqide is not built with coqmktop any morepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13777 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Don't install both coqide.byte and coqide.optpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13776 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Call coqtop with -nois when probing for filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13775 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Fix print in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13774 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07mli comments for docpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13773 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Update CHANGESpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13772 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-06Remove fake alpha-specific case in configureglondu
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
2011-01-06s/appartness/membership/g (Closes: #2470)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13767 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-06Reverted r13715 "Add improved indenters that rely on the current proof state ↵gmelquio
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
2011-01-06Remove Safe_marshalglondu
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
2011-01-04Ndigits: a Pshiftl_nat used in BigN (was double_digits there)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-04f_equiv : a clone of f_equal that handles setoid equivalencesletouzey
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
2011-01-03Numbers: some improvements in proofsletouzey
- 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
2010-12-27Rename the "raw" argument extension into "glob"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13761 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
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
2010-12-25Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsglondu
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
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
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
2010-12-24s/raw/glob/g in decl_interp.ml for more consistencyglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13757 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24More {raw => glob} changes for consistencyglondu
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
2010-12-24Rename files in funind to respect new conventionsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
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
2010-12-24tactics/eqdecide.ml4: avoid a useless argument in decideEqualityglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13753 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24Precision in documentation of "decide equality"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13752 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Remove the two-argument variant of "decide equality"glondu
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
2010-12-23Fix diagram in genarg.mliglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13745 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Rename rawterm.ml into glob_term.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
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
2010-12-23Prepare change of nomenclature rawconstr -> glob_constrglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13742 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:44:20 +0000