aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-10-25Icons in CoqIdE preference panelpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14590 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Configuration window of CoqIdE looks more like other Gtk one.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14589 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Heads: avoid potentially uncaught Not_found via an assert falseletouzey
The underlying issue (#2608) should be fixed now. In case something similar happens again, we won't be chasing again a Not_found here. Same idea as commit r14550, but this initial attempt was too zealous: we shouldn't also "protect" variable_head, since a Not_found in it is handled a few lines later. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14588 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-24More unification in type_of and addition of e_type_of to get the newherbelin
evar_map after instantiations possibly happened. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14586 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14585 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
Also fixing use of filter in second_order_matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14584 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Fixing failing printer when the type of a binder name with implicitherbelin
associated type contain evars (call to aconstr_of_glob_constr was not protected against failure in the presence of evars). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14583 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Fail if some conv pbs remain after consider_remaining_unif_problems.herbelin
This complies with consider_remaining_unif_problems being the last chance to solve constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14582 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Now consider remaining conversion problems in solve_remaining_evars.herbelin
A step going towards a more uniform evar resolution protocol, currently: - solve simple constraints (+ actually some heuristics: f.o. unif and evar_define's heuristics) but postpone some of the remaining ones [evar_conv] - try type-classes resolution [resolve_typeclasses] - apply heuristics on remaining constraints and expect these constraints to be resolved [consider_remaining_unif_problems] - use the implicit tactic for yet open (unconstrained) evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14581 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Use also second-order unification if first-order fails at the time of ↵herbelin
considering open problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14580 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
pattern; this fixes stupid causes of failure of destruct shown by compiling contrib Containers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14579 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Fixing uncaught exception in pr_evar_map (pr_global failed for unknown ↵herbelin
global ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14578 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
constructors as non relevant for injection. Also made injection failing in such situation. Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases (observed in the compilation of CoinductiveReals.LNP_Digit). The most probable explanation is that this loop was formerly protected by a failing rewrite which stopped failing after revision 14549 made second-order pattern-matching more powerful. Also suppressed dead code in Invfun.intros_with_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-20More descriptive error messages in checkerglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14576 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14574 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14573 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-01 01:54:31 +0000