aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Collapse)Author
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Fixing camlp4 compilation w.r.t previous commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15481 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-02Flushing formatters before program exit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30Getting rid of Pp.msgppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30More uniformisation in Pp.warn functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12lib directory is cut in 2 cma.pboutill
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Adapt the checker after commit 15080letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15100 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
We now accept the following code: Definition E := 0. Module E. End E. Techically, we simply allow the same label to occur at most twice in a structure_body, which is a (label * structure_field_body) list). These two label occurences should not be at the same level of fields (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change. Drawback : no more simple List.assoc or equivalent should be performed on a structure_body ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 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-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-08-08Esubst: make types of substitutions & lifts privatepuech
Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07bug 2423: consider "" as the empty prefixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14265 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07fixed coqchk usage and man page + added option -coqlibbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-23ported r14149 from v8.3 branch: bug in checker (redefined global)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14150 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
The env was used for a particular case of Cbytegen.compile_constant_body, but we can actually guess that it will answer a particular BCallias con. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Add directories in COQPATH to search path.herbelin
This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Reorder search path order, so the standard library is search last.herbelin
This allows the construction of an extended library that shadows the standard library. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14000 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneletouzey
After discussion with Bruno and Hugo, coqtop now accepts that an opaque constant in a module type could be implemented by anything of the right type, even if bodies differ. Said otherwise, with respect to subtyping, an opaque constant behaves just as a parameter. This was already the case in coqchk, and a footnote in documentation is advertising for quite some time that: "Opaque definitions are processed as assumptions." Truly, it might seem awkward that "Definition x:=3" can implement "Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing can go wrong afterwards, since Coq is forced to ignore that the x in signature has body "2". Similarly, "T with Definition x := c" is now legal when T contains an opaque x, even when this x isn't convertible with c. By avoiding accesses to opaque bodies, we also achieve some speedup (less delayed load of .vo final sections containing opaque terms). Nota: the extraction will have to be adapted, since for the moment it might access the body of opaque constants: the warning emitted when doing that should become an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04checker: cleanupglondu
Backport of changes introduced in r13443. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13867 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04checker: add eta-expansionglondu
Backport of changes introduced in r13443 and r13494. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13866 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-03Propagate recent kernel changes to the checkerletouzey
Cf in particular commits 13807 (about inlining) and 13835-13836 (changing the internal structure of delta_resolver and substitution). A pity we should duplicate so much code in the Checker... I tried to fix the corresponding val_* functions that check the integrity of the .vo, it seems to work, but I'm not familiar with this code. After this commit, apparently "make validate" accepts all the stdlib again, apart the new file setoid_ring/Ring2.v recently added by Loic, where it says "type error" on ring_syntax1. To be investigated... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13865 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-17- Use transparency information all the way through unification andmsozeau
conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Checker: remove some dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 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-16Explicit Mod_checking signatureglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13422 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-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* checker/Safe_typing.LightenLibrary:regisgia
Remove the function "save" as the checker only needs to read vo files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13387 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* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
proofs is now the default behavior of coqtop. * lib/Coqtop: Update accordingly. * checker/Check library/Library: Pass the right "load_proofs" flag to LightenLibrary.load. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 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-30adpated the checker to handle coomutative cuts and lazynessbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 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-22ported bug fix r13290 to checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13304 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 01:42:31 +0000