aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
to their signature of implicit positions and scopes) is computed. A bit of documentation in constrintern.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16Amelioration dans Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16fixed bug #2316 (ring_simplify)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13284 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
Extraction under modules is highly experimental, and just work a bit. Don't expect too much of it. With this commit, I simply avoid a few "assert false" to occur when we are under modules. But things are still quite wrong, for instance with: Definition foo. Module M. Definition bar := foo. Recursive Extraction bar. Extraction of bar is ok, but foo isn't displayed, since extraction can't get it: Lib.contents_after doesn't mention it, it is probably in some frozen summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13281 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-12Fix compilation and test-suite of nsatzglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13279 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-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-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-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-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-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-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 (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-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-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-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-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-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-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-16Extraction: fix the eta reduction function used in code optimisationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13158 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-15Extraction: in support library, more and nicer big_intletouzey
- we use a wrapper file big.ml to have short names about big_int and specialized functions for extraction - new files : ExtrOcamlZInt for Z==>int and N==>int, ExtrOcamlZBigInt for Z==>big_int and N==>big_int git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
checking function was used instead of a test of existence in the context. Also restricted constr_of_id which had no reason to interpret a posteriori an already interpreted identifier as a global reference. Consequently adapted funind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13135 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-10Extraction Implicits: can accept argument names instead of just positionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
products as implicit if they're part of a term and not a type (issue a warning instead). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Allowing to use an ordering different than Lt with measurejforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13098 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Using vernac parsing for Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13094 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Extraction with implicits: perform the occur-check after optimisationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13093 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
people use the undocumented "Lemma foo x : t" feature in a way incompatible with this activation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Typo in ExtrOcamlString: list char instead of char listletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13089 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
- Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-04Extraction: attempt to provide nice extraction of chars and strings for Ocamlletouzey
When Requiring ExtrOcamlString : * ascii is mapped to Ocaml's char, the ugly translation of constructor and pattern-match should hopefully be seen very rarely (never ?). We add a hack in ocaml.ml for recognizing constant chars. * string is mapped to (list char). Extracting to Ocaml's string could be done, but would be really nasty (lots of non-trivial Extract Constant to add). For now, (list char) seems a good compromise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13078 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-04Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03plugins/xml: kill two warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13065 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03Misc fixes related to new nsatz (and ocamlbuild)letouzey
- Kill a warning in ideal.ml corresponding to really brain-dead code. - Restore extraction/vo.otarget in pluginsvo.itarget - In fact, plugins/_tags can be merged into _tags with nice ** patterns - Update .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03nsatz ajoutepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13058 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of ↵pottier
nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix typosglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 08:15:49 +0000