aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-07-10Bool: iff lemmas about or, a reflect inductive, an is_true functionletouzey
For the moment, almost no lemmas about (reflect P b), just the proofs that it is equivalent with an P<->b=true. is_true b is (b=true), and is meant to be added as a coercion if one wants it. In the StdLib, this coercion is not globally activated, but particular files are free to use Local Coercion... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-09Finish adding out-of-the-box support for camlp4letouzey
If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Extraction: restrict autoinling to csts whose body is globally visible (fix ↵letouzey
#2241) Here, the constants "without body" we don't want to autoinline are constants made opaque by the rigid signature of their module. As mentionned by X.L. inlining them might lead to untypable code. The current solution is safe, but not ideal: we could want to inline such constants at least inside their own module, and we could also want to inline constants that are not globally visible (functors...). NB: AutoInline is anyway not activated by default anymore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13273 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Updating reference manual credits: gb is now nsatz.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Extraction: more factorization of common match branchesletouzey
In addition to the "| _ -> cst" situation, now we can also reconstruct a "| e -> f e" final branch. For instance, this has a tremenduous effect on Compcert/backend/Selection.v. NB: The "fun" factorisation is almost more general than the "cst" situation, but not always. Think of A=>A|B=>A, 1st branch will be recognized as (fun x->x), not (fun x->A). We also add a fine detection of inductive types with phantom type variables, for which this optimisation is type-unsafe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13267 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Extraction: Unset Extraction AutoInline is now the defaultletouzey
The auto-inlining has always been cumbersome. We only keep the inlining of recursors (foo_rect for inductive foo), and a short list of specific constants declared in mlutil.ml. In particular we inline andb and orb to keep their lazy behavior. The previous behavior is available via Set Extraction AutoInline git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13266 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13265 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Fixed compilation with statically-linked plugins (the decl_modeherbelin
plugins has to be linked before the xml plugin). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13262 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction Library Foo creates Foo.ml, not foo.ml (correct version)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13261 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
And similarly for Haskell: we do not force capitalized/uncapitalized filenames anymore, but we rather follow the name of the .v file (with new extensions of course). Ok, this is an incompatible change, but it is really convenient, some people where actually already doing some hacks to have this behavior (cf. Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07CHANGES: mention last-minute improvements of extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13250 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction: get advantage of nicer, algebraic, module typesletouzey
We use the mod_type_alg and typ_expr_alg field when they aren't empty. As a consequences, many signatures are now simple abbreviations, or "with" constructions, leading to .mli that are _way_ shorter this way. Various fixups concerning the "with Definition" syntax. In extract_seb_spec, we propagate both the alg and non-alg versions of the structure, for handlying nicely the "with" situation, and expanding situations not possible in ocaml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13249 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
- MPbound can be part of visible_mps (when printing the type of a module parameter, or when printing body of a With), hence the locality test base_mp mp = base_mp (top_visible_mp ()) isn't accurate. - new organisation, pp_ocaml_gen is splitted in many sub-functions, attempt to be clearer - the shortcut (if List.length ls = 1 then ...) isn't safe, we might detect name conflict even in this case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13248 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Mod_typing: fix the content of the typ_expr_alg fieldletouzey
Fix suggested by Elie. Without that, typ_expr_alg may contain Foo instead of Bar when Foo is a module of type Bar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13247 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Fix goal display when backtrackingvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13246 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Robustness fix : clean restart of coqtop on pipe error + force matchingvgross
of coqtop return codes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Turned off Mac dynlink hack for 10.6.3+ on x86_64thutchin
I don't have access to an x86_64 computer with 10.6 Maybe for 10.6.0/1/2 special cases aren't required Reverted commit r13083 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13243 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Stronger checks on coqtop termination, warning when zombies.vgross
Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
- Add module parameters in the structure of visible_layer, in order for module params to be part of name clash detection, avoiding this way a source of potentially wrong code. - In case of clash, module params are alpha-renamed to something unique (Foo__XXX where XXX is the number contained in the mbid). This solves some situations that were unsupported by extraction. for instance the "Module F (X:T). Module X:=X. ... End F." - We now check in Coq identifiers the presence of the extraction-reserved string __. If it is found, we issue a warning (which might become an error someday). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05FSets/Msets: some renaming of module params to simplify the task of the ↵letouzey
extraction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Fixing tabs closing problems by removing activation infrastructure.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13238 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Extraction: better support of modulesletouzey
- For Haskell, modules abbreviations and applied functors are expanded. The only remaining sitation that isn't supported is extracting functors and applying them after extraction. - Add a module extraction for Scheme with the same capabilities as for Haskell (with no Extraction Library, though). - Nicer extracted module types (use of the mb.mod_type_alg if present) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13236 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Remove dependency to Unix from module Profileglondu
Looking at the source code of Sys.time reveals that it is exactly what is computed by Profile.get_time. This can also be tested by evaluating: Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);; in an OCaml toplevel with Unix. This allows to put Profile in grammar.cma without the dependency to unix.cma while preprocessing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Sorting library: export as hints only lemmas that obviously simplifyherbelin
the size of the problem to solve. This is still more powerful than what 8.2 provided since no hints were exported yet when Permutation was in List.v in 8.2. Whether no hints should be exported at all, and whether hints should be exported in a specific database or not is unclear. At least, the contribs apparently supported the extra added power of auto introduced in r12585 (date of the revision of the Sorting library), so let's continue with it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13231 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-01Miscellaneous small updates:herbelin
- removed call to obsolete ppmsid printer in 8.3 - updated COMPATIBILITY file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13229 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
thunks. Move from [lazy] to [delayed] in subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Fix generalize_eqs tactic to not consider defined variables as being ↵msozeau
generalizable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13226 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-29Correct wrong handling of evars in instance definitions that preventedmsozeau
information going from the body to the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13224 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-29QArith: typo in name of hint db (fix #2346)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13220 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
a 3 state type to allow: * KernelVerbose / KernelSilent : handle the display of messages launch by Coq * UserVerbose : handle the display of messages launch by user actions Coq will still behaves the same way (TODOs in the code mark the places where we can now change the behaviour). I'll remove them in a few days when we'll have agreed on the correct behaviour. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Fix compilation by replacing some "auto with zarith" with "ring"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13212 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Extraction: handling modules (not functors) in Haskell by name manglingletouzey
Module types are ignored, functors and module ident raise an error When dealing with simple modules, even nested, the structure hierarchy is removed, and names are arranged in the following way: - For the monolithic extraction, we simply use next_ident_away on short names, as we do when the same name appears in two .v. - For modular extraction, A.B.t become A__B__t or _A__B__t depending whether t is a type, a constructor or a constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13210 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Update of documentation for the standard library (cf. #2332)letouzey
This is a slightly modified version of the patch proposed in #2332 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13209 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Extraction: remove a useless matchletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13208 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Made "replace" accepts open terms on its left-hand-side.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13206 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Fixed a bug introduced in a combination in r12807 and revealed inherbelin
r13080 via a failure in CoRN (pattern_of_constr needs correct sigma). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13205 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES. Fixed spelling of "uniform inheritance condition" in doc too (see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-26Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.herbelin
Fixing tests 2145.v about Nsatz. Adding nsatz target in Makefile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13203 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25Moved error when option does not exist into a warning (this allows toherbelin
improve compatibility between Coq versions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13196 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25bug 2328 fixed: failure when polynomial not i idealpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13195 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25modifs de nsatz suggerees par Hugopottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13194 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify" accepted evars as ordinary variables. I hope I did not invalidate some features that would have needed restricting conversion on evar-free terms, but since failure of conversion in presence of evars is redirected to the main unification algorithm, I guess it is OK. For better readibility, I also inlined and cleaned a bit trivial_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13192 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Names: remove obsolete mod_self_idletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13190 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Ajout d'une feuille de style pour les définitions spécifiques à Hevea + ↵notin
divers corrections sur la génération du manuel de référence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ↵notin
coq.inria.fr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13185 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Commit 13179 continued (updated CHANGES about support for Heq's library).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13181 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:41:57 +0000