aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-10-18Fix bug #2227msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14572 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14571 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Revert "New evar_map printer ppevmfull which can typically be installed for"herbelin
This reverts commit 44a6b1a7dcc483a3ef762a83cae2f771cddb09b6. As kindly noticed to me by Arnaud, this function already existed. Sorry about the noise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14569 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Partly reverting r14539 about fully expanding "let-in"s and not justherbelin
expanding them up to the last Var/Rel they are aliased to. The analysis made in r14539 about ill-typed pattern-unification in bug however, when abstracting over a "let-in" (in solve_pattern_eqn), the alias must be preserved for ensuring the correctness of typing. In short, "let-in"s are back considered for pattern-unification as constants of which we don't want to know the content but solve_pattern_eqn now takes into account that they have a value. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14568 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17New evar_map printer ppevmfull which can typically be installed forherbelin
debugging with full sigma (typically for debugging type inference). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14567 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Patch by Dan Grayson to ensure that "Add LoadPath ... as ..." closesherbelin
the file descriptors on directories that it does not need to keep open (the maximum number of simultaneously opened file descriptors supported by the operating system is not so large in practice, e.g. 256 on MacOS X). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14565 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing ↵msozeau
zeta reductions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14564 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-15dev/base_include: display a nice message at the end of the loadletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14563 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-15debugging.txt: no more typing of #use "include" if using .ocamlinitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14562 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
In fact, this formula "fold ... = fold_right ... (rev (elements))" was already frequently used, but without ever stating it explicitely. Instead, we were always chaining two rewrites each time. Thanks to A. Appel for mentionning this question of fold_right vs. fold_left in the spec of fold. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14561 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-12Temporary revert commit 14550 since it breaks a few contribsletouzey
Interestingly, it appears that the Not_found in heads.ml is actually triggered in some contribs, but catched. Maybe a "try" tactical ? Are these Not_found another effects of bug #2608 or something similar ? Anyway, replacing Not_found by "assert false" currently breaks these contribs. So for the moment, we revert to the original code. When bug #2608 will have been solved, we'll try again enabling these "assert false". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14560 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-12Patch to support (a priori) all versions of make 3.xx >= 3.81herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14557 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-12test-suite: non-regression test for bug #2603letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14556 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Added test for bug #2615herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14555 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-11in heads.ml, at least turn the Not_found of #2608 into assert falseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14550 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
second-order matching) which was not working correctly in the general case. Also made that second-order matching for tactics (abstract_list_all) uses this algorithm, along the lines of a proposal first experimented by Dan Grayson (see unification.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Unification in the return clause of match was not supported in solve_evars.herbelin
This is now fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14548 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 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
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Hash-consing of mutual_inductive_body (and Univ.constraints)letouzey
Inductive definitions aren't that big, but they may contain some constr (in types, rel_context, etc), hence if we hash-cons the constr in Definition but not these ones, we may loose some sharing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14544 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Avoid some re-allocation during hash-cons of dir_pathletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14543 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Hash-cons the statically allocated Rels (1 to 16) to themselvesletouzey
This is just a minor detail, but if we take care to use in mkRel always the same physical Rels for n <= 16, then let's ensure that these Rels are preserved by hash-consing. This way, we avoid killing some sharing during hash-consing of most of constr but not all (for instance those in mind). In fact, this is probably superfluous since earlier commit about "| Rel n as t -> t", but let's be sure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14542 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Hashtbl_alt : typo in a commentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14541 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Hash-cons of constr : avoid some useless allocationsletouzey
Since we hash-cons arrays in place, no need to re-allocate a few structures around them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14540 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
- Compute chain of aliases once for all so as to simplify code. - In is_unification_pattern, expand all vars/rels of the unification problem until they are no longer vars/rels so that the list of vars/rels used in the rhs is correct, and, the list of arguments of the evars eventually become irreducible vars/rels (in particular, this solves bug #2615). - Some points remain unclear, e.g. whether solve_evar_evar should reason with all let-in expanded or with let-in expanded only up to the last expansion which is still a var or rel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14539 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
problems with dependencies. Generalized it to matching over dependent tuples as explored by Dan Grayson. Currently used only in Evarconv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Fixing buggy abberant code for Evarutil.expand_evarherbelin
by the way renamed into materialize_evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14537 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Little code simplification of instantiate_evar in evd.mlherbelin
(replace_vars was anyway optimized) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14536 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Added information about evar origin in pretty-printing evd for debugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14535 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
evar_define so that it can recursively deal with evar/evar problems. Also, check_evar_instance now called after each instantiation. Also did a bit of file reformatting. The commit apparently induces a loss of some 0,4% on the compilation of the standard library. Maybe, introducing a heuristic to decide when to call check_evar_instance (which I guess is responsible for the overhead) might be a good thing to look at? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Proper fix for complement/flip instances.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14533 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-09mainbiblio.bib : get rid of merge marker from failed mergeletouzey
Thanks to Tom Prince for spotting this git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14530 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
when schemes are generated for internal use of Coq. Ideally, I would like to add these names asynchronously in name spaces relevant for the corresponding inductive type, what modules do not support since modules cannot be reopened. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14529 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-08Rely on kernel to know if a name is already used so as to be consistent with it.herbelin
Maybe could we keep only the kernel check, but message would certainly need to be reformulated then. For instance, the message was previously different for an attempt to redefine a name whether this name was in the same section or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
Btw, we also get rid of equalities on something else than elements or sets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14524 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ↵msozeau
it properly in the syntax of terms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14522 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
- We now handle things like (H : E.eq x x -> ...) by rewriting E.eq x x into True. - There was also a confusion between E.t and its various equivalent (but syntactically different) forms. This should be solved by preventing inlining during an inner functor application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07ocamlbuild: remove -dllpath from coqrunbyteflagsglondu
See bug #2614. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14519 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.glondu
The changes to myocamlbuild.ml didn't compile. See bug #2614. Signed-off-by: Tom Prince <tom.prince@ualberta.net> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14518 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
There were some confusion on the role of clear_proofs which was applicable only to the global named_context. Hopefully made things clearer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14517 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05When a pattern match, don't use the first matching term but anherbelin
instance of the initial pattern (this fixes compilation of CoRN after r14499). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14516 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Removing vernacular code mistakenly committed.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14515 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
If two distinct parameters of the inductive type contributes to polymorphism, they must have distinct names, othewise an aliasing problem of the form "fun x x => max(x,x)" happens. Also insisted that a parameter contributes to universe polymorphism only if the corresponding occurrence of Type is not hidden behind a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-16 00:17:57 +0000