aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-11-03Cleaning a little bit the files talking about descriptions: avoidingherbelin
same name for different statements as noticed by Adam Chlipala on coq-club, avoiding stating the same axiom twice in distinct files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14628 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-29Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).herbelin
There are preliminary problems to solve in the semantics of -I/-R which differs from the one of coqtop: - in case of ambiguity, internally to -R option, or between two -R/-I options, it is not clear at all that the semantics is as in coqtop (which by the way is not canonical either since it seems to depend on the underlying order of dirs in the file system), - in the presence of -I dir, Require A.b does not look if dir.A.b exists; similarly for Declare ML Module "f", Require "f" and Load "f" when f has a dirname part. I suggest to have a common library for coqdep, coqdoc and coqtop that ensures that -I/-R behave consistently for all tools. Incidentally made coqdep lexer a bit more strict about syntax errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14626 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-29Fixed broken globalization of identifiers containing utf8 lettersherbelin
without knowing it. Note: location tables have grown a lot, a better representation of the contents of the glob files in coqdoc might improve efficiency. Also added keywords. Information is now obtained from the glob file to know the exact span of identifiers. Kept a class of identifiers (and enriched them) for the main purpose of distinguishing between idents and symbols in the absence of a glob file. Still a lot of work to do in coqdoc to make it more robust... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14624 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-29Added checksums to glob files and warned about possibly missingherbelin
packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-27Remove avoidable use of GDynamicglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14620 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Deactivating second-order pattern-matching in evarconv for 8.4.herbelin
Kept in "destruct" though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14619 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Fix configuration box bug in recursive callpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14618 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Coq_makefile handles .mlpack filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14617 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Coqdep handles .mlpackpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14616 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)letouzey
When doing a [check_subtypes env mtb1 mtb2], we used to always add [mtb1] in the environment. But since the stricter checks of commit r14150, this is an error if the environment already knows [mtb1] (for instance when doing (F M) and checking that M is compatible with the type of the arg of F. [check_subtypes] now expect [mtb1] to be already in env, and we move the add_module to the unique call site of this function that requires it. Moreover, we solve a second issue : when subtyping a functor, we update the environment once inside the functor, and this is also refused by the checks of commits r14150. So we first remove the module name from the env before doing the update. Since the module added earlier was a functor, there is no inner defs to chase in env. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14615 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
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
2011-10-26Environ.set_universes is dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14613 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Mod_subst: some simplifications, some more significant names to functions, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14612 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Auto: avoid storing clausenv (and hence env, evar_map, universes) in voletouzey
It appears that registration of hints is the only place (at least when compiling stdlib) where Univ.universes (the graph of universes) is stored in vo. More precisely, a Hint Resolve will place in vo a pri_auto_tactic, which may contain some clausenv, which contain both a env and a evar_map, each of them containing a Univ.universes In fact, even env and evar_map are also never stored in vo apart from hints registration. Currently, there's nothing wrong in this storing of env / evar_map / universes. In fact, it seems that every stored universes are actually empty. Same for env, thanks to awkward lines { cl with env=empty_env }. But this may hinder potential evolutions of Univ.universes toward a private per-session representation. Conclusion: it is cleaner (and not that hard) to store a Term.types instead of the clausenv in vo, and reconstitute the clausenv at Require-time. On a compilation of the stdlib, the time effect is hardly noticable (<1%). NB: a Univ.universes is also stored in initial.coq, but this is a different story (Write State ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14611 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Makefile install rule fixpboutill
Consequence of r14597 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14610 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Coq_makefile includes coqtop -config without file generationpboutill
Make the compilation log cleaner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14609 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-16 10:32:07 +0000