aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2010-12-16Univ: two improvements (speed + space)letouzey
- 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
2010-12-01* Kernel/Term:regisgia
- Fix a bug in [comp_term] (casts were ignored). - Improve the efficiency of hash table lookup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13662 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-01* Kernel/Termregisgia
Remove an unsound optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-01* Kernel/Termregisgia
Fix an efficiency bug when hash-consing deep [constr]s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13660 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-15Minor fixes from Gregory Malecha. A typo fixed and a better (located) msozeau
error message in case of unnammed record parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13635 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03Correction bug 2427soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13617 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03Remove suspiciously named "implicit" stuff from Termglondu
The lambda_implicit series of functions are used only in Indtypes, so we move them there. In the checker, they are already there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13615 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03In Univ, unify order_request and constraint_typeglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13614 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02More generic Univ.dump_universesglondu
Instead of formatting directly to an output channel, provide an output function that handles formatting and I/O. This allows changing the output format. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13610 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-05Reintroduce kind_of_type (used by Presburger contrib)glondu
This partially reverts commit r13467. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13497 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-04Forgotten lifts in eta-expansionglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13494 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Fixing printing of module_path names (was using a debuggingherbelin
message since r11177). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13486 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Remove kind_of_type, kind_of_term2 (dead code)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13467 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Partial review of removed dead code (r13460)herbelin
- The code detected unused in notation.ml revealed a bug. - In term.ml, restored a (short) useless function for consistency/symmetry of the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13463 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
This commit fixes a bug that made the system inconsistent with proof irrelevance (the main idea being that Set = Prop by reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-15Sharing is not anymore broken by traverse_module.soubiran
+commit r13412 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13418 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-15Fix likely semantic typosglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13417 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* kernel/Safe_typing.LightenLibrary:regisgia
Fix an incorrect initialization of the index counter. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13386 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* (checker|kernel)/Safe_typing:regisgia
Rename "lighten_*" into "traverse_*" inside the [traverse_library] function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13385 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* (checker|kernel)/Safe_typing:regisgia
Fix a bug in traverse_library. The extraction was not satisfied with [mod_expr] set to [None]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13384 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* checker/SafeTyping kernel/SafeTyping:regisgia
Fix typos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13380 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* Improve documentation of LightenLibrary.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13378 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
This module introduces an indirection behind opaque const_body to enable the optional demarshalling of them. * library/Library checker/Check: Use LightenLibrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13377 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30better fix to bug #2319: types are compiled in the env of the bodiesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13362 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29kernel conversion and reduction do not raise assert failure on ill-typed ↵barras
terms, but an anomaly instead. It is caught in pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13353 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵barras
predicate in branch read-back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13349 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28ported r13340 to trunkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13341 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16fixed (serious) bug #2353: non-recursive parameters of nested inductive ↵barras
types were seen as real constructor arguments... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13290 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16removed a potentially dangerous try ... with _ -> ...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13289 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Mod_typing: fix the content of the typ_expr_alg fieldletouzey
Fix suggested by Elie. Without that, typ_expr_alg may contain Foo instead of Bar when Foo is a module of type Bar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13247 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Names: remove obsolete mod_self_idletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13190 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
Note that the code is no longer in constrextern.ml but in topconstr.ml where the code for reversing notations of term already was. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03"Improved" the form of the inferred type of "match" byherbelin
betaiota-reducing it automatically (this allows for instance to directly obtain the expected type for "match" expressions that have a "in I x return match x with ... end" automatically inferred return predicate feature (see e.g. Vhead and Vtail in Bvector.v). The need for this "optimization" was not noticed in V8.2 because in Bvector.v, betaiota was applied peremptorily at the end of sections. The need for it has been revealed by the removal of reduction at section closing when Arnaud introduced the new proof engine (should in particular make CoLoR compile). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13068 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20fixed guard check with commutative cutsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20Mrec was not substituted correctlybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13021 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Discontinue support for ocaml 3.09.*letouzey
Ocaml 3.10.0 is already three year old... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-18Some ocamldoc comments + Fixing name of .coqrc.version file in refmanpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm property of "u" in the analysis of "t". Commutative cuts aren't compatible with typing so we need to ensure that term of "x"'s type and term of "u"'s have the same subterm_spec. Consequently,declaration.MRec argument has changed to the inductive name instead of only the number of the inductive in the mutual_inductive family. In subterm_specif and check_rec_call, arguments are stored in a stack. At each lambda, one element is popped to add in renv a smarter subterm_spec for the variable. subterm_spec of constructor's argument was added this way, the job is now done more often. Some eta contracted match branches are now accepted but enforcing eta-expansion of branches might be anyway a recommended invariant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-09Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13006 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
dev/ocamldoc/ old "make source-doc" that documents ml files and didn't work is now "make ml-doc" but still don't work :-) "make clean" cleans dev/ocamldoc/ properly wierd? calls of dependency graph generation leave unchanged git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
In checker: - delta_resolver inferred by the module system is checked through regular delta reduction steps - the old mind_equiv field of mutual_inductive is simulated through a special table in environ - small optimization, if the signature and the implementation of a module are physically equal (always happen for the toplevel module of a vo) then the checker checks only the signature. In kernel - in names i have added two special equality functions over constant and inductive names for the checker, so that the checker does not take in account the cannonical name inferred by the module system. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12977 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29fixed bug #2224 (Error message in positivity check fixed)vsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12974 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 20:15:25 +0000