aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2010-06-22Backport from trunk to 8.3 of modifications on groebner/nsatzherbelin
(13056-13058, 13062, 13069, 13073). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13180 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Fixing dependencies for coqidevgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13178 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22fix bug #2318, parsing error on dos line endingsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13177 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix ↵letouzey
#2158,#2179) Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is the hexa code for the unicode index of this character. For instance <alpha> is turned into __U03b1_. I know, this is ugly. Better solutions are welcome, but I'm afraid we can't do much better as long as ocaml and haskell don't accept unicode letters in idents. At least, this way we're pretty sure this translating won't create name conflit, as long as extraction users avoid __ in their names, something that they should already do btw (see for instance extraction of coinductive types in ocaml). Yes, I should add a test and a warning/error in case of use of __ someday. NB: this commit belongs proudly to the quick'n'dirty category git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13172 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18clear/revert dependent: restrict to hyp(h) instead of ident(h)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13169 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13168 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:18:32 +0000