aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-10-26 Coq_makefile: libraries in bytecode are now installed toopboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14608 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14607 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
tactic notations and ltac definitions (see bug report #2496). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14606 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14605 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Regression tests for bugs #2613 and #2616.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14604 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-25Coq_makefile: a more complete commentary about global variablespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14599 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Coq_makefile does not install/compile explicitely cmo and cmxs? that are in ↵pboutill
a cmx?a git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14598 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25coqdep defines a makefile variable name_MLLIB_DEPENDENCIES to store ↵pboutill
dependencies of name.mllib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14597 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Fixing use of type constraint for refining the "return" clause of "match".herbelin
Adams Chlipala's ltamer now compatible with forthcoming 8.4; thanks to Matthieu for how to reactivate inh_conv_coerces_to. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14596 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14595 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Fixing "destruct" test.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14594 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Continuing r1492 (useless changes were inadvertantly committed)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14593 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25New strategy to infer return predicate of match construct whenherbelin
external type has evars. We now create a new ad hoc evar instead of having evars as arguments of evars and use filters to resolved them as was done since about r10124. In particular, this completes the resolution of bug 2615. Evar filters for occurrences might be obsolete as a consequence of this commit. Also, abstract_tycon, evar_define, second_order_matching which all implement some form of second_order_matching should eventually be merged (abstract_tycon looks for subterms up to delta while second_order_matching currently looks for syntactic equal subterms, evar_define doesn't consider the possible dependencies in non-variables-nor-constructors subterms but has a better handling of aliases, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14592 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Still more unification in typing.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14591 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 12:29:08 +0000