aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Remove some dead code in the vmGravatar letouzey2012-10-02
| | | | | | | | | | | | | 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
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Default hashconsing of identifiers.Gravatar ppedrot2012-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reusing the Hashset data structure in Hashcons. Hopefully, this shouldGravatar ppedrot2012-09-26
| | | | | | not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Incorrect commentGravatar msozeau2012-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing ocamldoc errorsGravatar ppedrot2012-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15833 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
| | | | | | Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | 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
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | 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
* kernel/Term:Gravatar regisgia2012-09-14
| | | | | | | 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
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
| | | | | | 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
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
| | | | | | | | | | | | | | 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
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | 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
* Adding newline after warning and restoring distinction betweenGravatar herbelin2012-04-15
| | | | | | 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
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
| | | | | | | | | | | | | | 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
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
| | | | | | 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
* Univ: switch the order of int and dir_path in UniverseLevel.LevelGravatar letouzey2012-03-22
| | | | | | | | 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
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
| | | | | | change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Final part of moving Program code inside the main code. Adapted ↵Gravatar msozeau2012-03-14
| | | | | | 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
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
| | | | | | | | 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
* Univ: avoid recording dummy universe constraints u<=u or u=uGravatar letouzey2012-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | 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
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
| | | | | | | | | | | 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
* Univ: a better Constraint.compareGravatar letouzey2012-03-01
| | | | | | | 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
* Univ: a faster is_leq test used when possibleGravatar letouzey2012-02-29
| | | | | | | | | | | | 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
* Univ: correct compare_neq (fix #2703)Gravatar letouzey2012-02-27
| | | | | | | | | | | | | | 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
* Proof using ...Gravatar gareuselesinge2011-12-12
| | | | | | | | | | | | | 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
* Term: properly ignore Casts between Apps in constr_ordGravatar puech2011-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: useless conversion to list in constr_ord deletedGravatar puech2011-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: Fix hash_constr behavior for Cast lnterleaved in application spines.Gravatar puech2011-11-28
| | | | | | | | 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
* TypoGravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14698 85f007b7-540e-0410-9357-904b9bb8a0f7
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
| | | | | | | | | | | | | 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
* Environ.set_universes is dead codeGravatar letouzey2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst: some simplifications, some more significant names to functions, etcGravatar letouzey2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14612 85f007b7-540e-0410-9357-904b9bb8a0f7
* First attempt at making Print Assumption compatible with opaque modules (fix ↵Gravatar letouzey2011-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | #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
* Mod_subst: Attempt to fix #2608Gravatar letouzey2011-10-24
| | | | | | | | | 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
* Safe_typing: adding a inductive block adds many labels (fix #2603)Gravatar letouzey2011-10-11
| | | | | | | | | | 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
* Names : check of labels, cleanup, nicer debug display of kn and constantGravatar letouzey2011-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst: an unused functionGravatar letouzey2011-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14551 85f007b7-540e-0410-9357-904b9bb8a0f7
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
| | | | 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.39.1) at 2024-06-23 19:23:25 +0000