aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2012-10-02Remove some dead code in the vmletouzey
Apparently Cysmtable.set_global_boxed is unused, and removing it allows to get rid of a bunch of C code concerning "boxed" things (including ACCUMULATECOND instruction). Still TODO: Csymtable.set_transparent_const and Csymtable.set_opaque_const appear to be no-ops. Should we remove them ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15845 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-27Default hashconsing of identifiers.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15837 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26Incorrect commentmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15835 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-25Fixing ocamldoc errorsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15833 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14kernel/Term:regisgia
Backtrack on a type definition that was moved by error by the previous patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15798 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-18Proof using: nested sections bugfixgareuselesinge
It used to be the case that the list of declared section variables for a constant was taken into account only when discharging the first enclosing sections, but not any outer section. Example of the bug: Section A. Variable x : bool. Section B. Variable y : nat. Lemma foo : True. Proof using x y. Admitted. End B. End A. Check foo. (* nat -> True instead of bool -> nat -> True *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15445 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30More uniformisation in Pp.warn functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-15Adding newline after warning and restoring distinction betweenherbelin
fatal and non fatal identifier check errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15178 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-05Shortcuts and optimizations of comparisonsxclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15118 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
We now accept the following code: Definition E := 0. Module E. End E. Techically, we simply allow the same label to occur at most twice in a structure_body, which is a (label * structure_field_body) list). These two label occurences should not be at the same level of fields (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change. Drawback : no more simple List.assoc or equivalent should be performed on a structure_body ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22Univ: switch the order of int and dir_path in UniverseLevel.Levelletouzey
Our specialized comparison already handles the int and dir_path in this order. But there may remain some Pervasives.(=) elsewhere in the code, which should benefit from this reordering git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15080 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Final part of moving Program code inside the main code. Adapted ↵msozeau
add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
did not handle let-ins and was wrongly specified). Thanks to Pierre Boutillier and Pierre-Marie Pédrot for pointing out the source of the bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-12Univ: avoid recording dummy universe constraints u<=u or u=uletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15026 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
univ_depends checks whether a universe variable appears or is equal to a universe. In comparison with the previous hack in inductiveops based on try...catching UniverseInconsistency, this should be semantically equivalent, simplier, and more robust in case we allow someday an unsafe mode where merge_constraints would be a no-op. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-01Univ: a better Constraint.compareletouzey
Let's gain a few % by not using Pervasive.compare on a structure containing some universe_levels, but rather UniverseLevel.compare on them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15012 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29Univ: a faster is_leq test used when possibleletouzey
Let's reintroduce the idea of stopping the graph traversal as soon as a LE arc has been found, but this time we do so only when we're not interested by the LT/LE distinction. This way, we should remain correct but avoid largly the time penalty induced by the last fix on univ.ml: the +30% on contrib Container is almost gone, let's hope it'll be the same with Ssreflect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-27Univ: correct compare_neq (fix #2703)letouzey
The earlier version was a bit too quick to answer <= while strict constraints could still appear from remaining universes to explore. Typical situation: compare u v when u <= v and u <= w < v. Encountering u <= v isn't enough to conclude yet... This means that kernels from r13719 to now in trunk, and from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately detect universe inconsistencies, leading to potential proofs of False! Oups, sorry... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14993 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-12Proof using ...gareuselesinge
New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Term: properly ignore Casts between Apps in constr_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14739 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Term: useless conversion to list in constr_ord deletedpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14738 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28Term: Fix hash_constr behavior for Cast lnterleaved in application spines.puech
hash_constr should give the same hash to two terms differing only by the presence of Casts. It should now make the same quotients on terms than constr_ord or equals_constr. This handles the case of App(Cast(App(f, l1), _, a), l2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14735 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14698 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
Here Foo is Univ.constraints, Univ.universes, Evd.evar_map, Evd.Metamap Ok, all these structures are currently ocaml's maps or similar, with a unique empty value, and (=) can be used on them in this particular case. But using Foo.is_empty is safer : it will work even if the underlying representation changes. Example : for spotting non-legitimate use of (=) we might embed a type into a record with a functional field. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14614 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Environ.set_universes is dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14613 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Mod_subst: some simplifications, some more significant names to functions, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14612 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ↵letouzey
#2168) We replace Global.lookup_constant by our own code that looks for a module and enters its implementation. This is still preliminary work, I would prefer to understand more completely the part about module substitutions when entering an applied functor. But this code already appears to work quite well. Anyway, since we only search for constants, we don't need to reconstitute a 100% accurate environment, as long as the same objects are in it. Note: - Digging inside module structures is slower than just using Global.lookup_constant. Hence we try to avoid it as long as we could. Only in front of axioms (or in front of constant unknown to Global) do we check whether we have an inner-module implementation for this constant. There is some memoization of the search for internal structure_body out of a module_path. - In case of inner-module axioms, we might not be able to print its type, but only its long name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Mod_subst: Attempt to fix #2608letouzey
In presence of inlining, it seems that no alias is propagated on the canonical kernel_name. We modify [subst_con0] to enforce this semantics. It seems to work well, but my understanding of this code is still limited... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14587 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Safe_typing: adding a inductive block adds many labels (fix #2603)letouzey
When adding an inductive block in the environment, we now check that no types or constructors in this block correspond to a label already used in the current module. The earlier check was to try only the first inductive type (which serves as label in the structure_body), that was causing awkward situations, cf. for instance #2603. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14553 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Names : check of labels, cleanup, nicer debug display of kn and constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14552 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Mod_subst: an unused functionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14551 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14546 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:49:59 +0000