aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-11-21Lazier behaviour of [auto] when introducing hypothesis: query the hint db's ↵puech
only when necessary. Hopefully should speed up [auto] a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12538 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-19Refactoring of coqide backtrack code, with the intent to put everythingvgross
into coqtop. Also, some cleaning in ide/gtk_parsing.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-19Correction du bug #2118 (Coqdep does not escape #)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12536 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Now "Include Self <expr>" handles partially applied functors, cf for example ↵soubiran
NZAddPropFunct in NZAdd.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12535 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Diamond-shape instead of linear hiearchy in Numbers/NatIntletouzey
NZBase -- NZAdd -- NZMul | | NZOrder ---------- NZAddOrder -- NZMulOrder -- NZProperties This is done by transforming NZBase into a functorial module type, and making NZAdd NZMul NZOrder accept an instance of NZBase as parameter. This is possible thanks to a combination of various new features of modules: - interactive proofs in module type (ie functors can be turned into type functors) - Include Type in Module (ie type functors can be turned into functors) - Include Self, <+ , etc, etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12534 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Allow interactive proofs in module typesletouzey
Elie suggested this change, it seems that there are no real reasons to forbid interactive proofs in module types. A functor can now be written with Module Type, and can hence be used later as parameter of other functors (while it can also be translated to regular functor by a Include Type in a Module). See next commit for a example of diamond-shape developpement that become possible with this feature. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12533 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
Any place where <: was legal can now contain many <: declarations. Moreover we can say that the module type we are declaring is a subtype of an earlier module type. See DecidableType2 for examples. Also try to handle correctly the freeze/unfreeze summaries when simulating start/include/end (syntax ... := ... <+ ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
"Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for "Module M (...). Include M1. Include M2. Include M3... End M." Moreover M2,M3,etc can be functors as long as they find what they need in what comes before them (see new command "Include Self"). The only real constraint is that M1,M2,M3,... should not have common elements (for the moment (?)). Same behavior for signature : Module Type M := M1 <+ M2 <+ M3. Note that this <+ is _not_ a primitive construct of the module language, for instance it cannot be used in signature (Module M <: M1 <+ M2 is illegal for the moment). Some example of use in Decidable2 and NZAxioms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
We can now have a diamond-like approch to extentions of signatures, instead of a linear-only chains as earlier... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12529 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
If you have some Module Type F (X:Sig), and you are in a Module Type containing everything required to satisfy Sig (typically thanks to some earlier Include), then you can say Include Self Type F, and voila, objects of F are now added in your context, instantiated by local objects. Same behavior (hopefully) for modules and functors when using Include Self F. This experimental new command allows to easily produce static signatures out of functorial ones: Module Type F_static. Include Sig. Include Self F. End F_static. ... is similar to ... Module Type F_static. Declare Module X:Sig. Include F X. End F_static. ... but without the pollution of this artificial inner module X. This allow to split things in many othogonal components, and then mix them. It is a lightweight way to tackle the "diamond problem" of modular developpements without things like "overlapping" Include's (planned, but not yet there). See next commit for an example of use. Thanks to Elie for the debugging of my first ugly prototype... NB: According to Yann R.G., this is related with Scala's Traits. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12528 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Some lemmas about dependent choice + extensions of Compare_dec +herbelin
synonyms in Le.v, Lt.v, Gt.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12527 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Fix type class discharge again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12526 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Document Generalizable Variables, and change syntax to msozeau
[Generalizable (All|No) Variables (ident+)?], also update type classes documentation to reflect the latest changes in instance decls. Fix a bug in [Util.list_split_when]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Fix [Instance: forall ..., C args := t] declarations to behave asmsozeau
expected, not introducing the [forall ...] variables to avoid unnecessary eta-expansions. Force to use { } in instance declarations when the class is a record even if it's a singleton. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12524 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Move Obj.magic call to the Vm moduleglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12523 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Remove dubious call to Obj.magic (and dead code, by the way)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12522 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Remove useless call to Obj.magicglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Make usages of the Obj module explicitglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12520 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Remove useless ppevd (which is identical to ppevm)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12519 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13scripting area now grabs focus at startup.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12518 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13new handling for lexical structures.vgross
Sentence extraction and proof folding is now done with tags. The lexer has been modified to use a callback to "stamp" the lexical constructs that must be distinguished. new funcs in ide/coqide.ml : apply_tag : GText.buffer -> GText.iter -> (int -> int) -> int -> int -> CoqLex.token -> unit remove_tags : GText.buffer -> GText.iter -> GText.iter -> unit tag_slice : GText.buffer -> GText.iter -> GText.iter -> (GText.buffer -> GText.iter -> GText.iter) -> unit get_sentence_bounds : GText.iter -> GText.iter * GText.iter end_tag_present : GText.iter -> bool tag_on_insert : GText.buffer -> unit force_retag : GText.buffer -> unit toggle_proof_visibility : GText.buffer -> GText.iter -> unit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12517 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13lexing refactoringvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12516 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13the inlining computation at functor application was raising not_found when ↵soubiran
the applied module did not fulfill the signature of the functor argument. Now Coq gives an understandable error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12515 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
changes in obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12514 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Backtrack on fixing #2167herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12513 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les ↵notin
versions de OCaml antérieures à 3.11.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12512 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Oops, nf_evar_defs just changed to nf_evar_map.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12511 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Don't forget to normalize everything w.r.t. evars (fixes bug #2103).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12510 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Restore test-suite/csdp.cache erased from svn by mistakeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12508 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)letouzey
- In fact, Bind Scope has no retrospective effect. Since we don't want it inside functor, we use it late, and hence we are forced to use manual "Arguments Scope" commands. - Added syntax for power in BigN / BigZ / BigQ. - Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq) as in QArith. Display of a rational numeral is hence either an integer (constructor BigQ.Qz) or something like 6756 # 8798. - Fix of function BigQ.Qred that was not simplifing (67#1) into 67. - More tests in test-suite/output/NumbersSyntax.v A nice one not in the test-suite: Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)). = 1 : bigQ Finished transaction in 3. secs (3.284206u,0.004s) :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12507 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Experiment propagation of implicit arguments and arguments scope forherbelin
abbreviations of applied references. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12506 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Addendum to revision 12501.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12505 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
on the way: - Added a testsuite output file - Try to avoid nasty unfolding (fix nfun ...) in type of I31. Idealy we would need a "Eval compute in" for the type of a inductive constructor - Stop opening Scopes for BigQ, BigN, BigZ by default The user should do some Open Scope. TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope (and so on for other operations), even with some Bind Scope around. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Better compatibility for Peqbletouzey
As show by contrib TreeAutomata, the Peqb now placed in BinPos was using 1st arg as "struct", instead of 2nd arg as earlier. Fix that, and remove the "Import BinPos BinNat" hack in Ndec (merci Hugo :-). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12503 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Backtracking on the use of automatically generated schemes forherbelin
"eq"-rewriting (a few contributions are still referring explicitly to eq_rect, eq_ind and co and the new mechanism, though working also for dependent rewriting, is not powerful enough in general wrt fixpoint guard to claim being uniformly better). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12501 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Redoing broken commit r12498 (fixing bug #2167 + attempt to test theherbelin
compatibility of a more robust check of unconvertibility when providing "with" arguments to "apply"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12499 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Fixing bug #2167 + attempt to test the compatibility of a more robustherbelin
check of unconvertibility when providing "with" arguments to "apply". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12498 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Test for bug #2168, forgotten in r12496.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12497 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Fixed bug #2168 (closing a section may have as side-effect the erasureherbelin
of objects having the same name as the section). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12496 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
- Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10Compatibility ocaml <= 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12493 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10Correction du bug #2183notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12492 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10use only why-dp, support for z3marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12491 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxletouzey
To retrieve the old behavior of spec_sub0 and spec_sub with precondition on order, just chain spec_sub with Zmax_r or Zmax_l. Idem with spec_pred0 and spec_pred. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
- No more nesting of Module and Module Type, we rather use Include. - Instead of in-name-qualification like NZeq, we use uniform short names + modular qualification like N.eq when necessary. - Many simplification of proofs, by some autorewrite for instance - In NZOrder, we instantiate an "order" tactic. - Some requirements in NZAxioms were superfluous: compatibility of le, min and max could be derived from the rest. - NMul removed, since it was containing only an ad-hoc result for ZNatPairs, that we've inlined in the proof of mul_wd there. - Zdomain removed (was already not compiled), idea of a module with eq and eqb reused in DecidableType.BooleanEqualityType. - ZBinDefs don't contain any definition now, migrate it to ZBinary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10DecidableType: A specification via boolean equality as an alternative to eq_decletouzey
+ adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12488 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-09Deactivation of (intrusive) printing of abbreviations from non-imported modules.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12487 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-09Commit 12485 continued.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12486 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 09:32:53 +0000