aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
| | | | | | | | 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
* Correction du bug #2118 (Coqdep does not escape #)Gravatar notin2009-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12536 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now "Include Self <expr>" handles partially applied functors, cf for example ↵Gravatar soubiran2009-11-18
| | | | | | | | | NZAddPropFunct in NZAdd.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12535 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diamond-shape instead of linear hiearchy in Numbers/NatIntGravatar letouzey2009-11-18
| | | | | | | | | | | | | | | | | | 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
* Allow interactive proofs in module typesGravatar letouzey2009-11-18
| | | | | | | | | | | | 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
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
| | | | | | | | | | 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
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
| | | | | | | | | | | | | | | | | | | | "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
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
| | | | | | | 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
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
| | | | | | 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
* Fix type class discharge again.Gravatar msozeau2009-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12526 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
| | | | | | | | | [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
* Fix [Instance: forall ..., C args := t] declarations to behave asGravatar msozeau2009-11-15
| | | | | | | | | 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
* Move Obj.magic call to the Vm moduleGravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dubious call to Obj.magic (and dead code, by the way)Gravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless call to Obj.magicGravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make usages of the Obj module explicitGravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless ppevd (which is identical to ppevm)Gravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12519 85f007b7-540e-0410-9357-904b9bb8a0f7
* scripting area now grabs focus at startup.Gravatar vgross2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12518 85f007b7-540e-0410-9357-904b9bb8a0f7
* new handling for lexical structures.Gravatar vgross2009-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* lexing refactoringGravatar vgross2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12516 85f007b7-540e-0410-9357-904b9bb8a0f7
* the inlining computation at functor application was raising not_found when ↵Gravatar soubiran2009-11-13
| | | | | | | | | 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
* Fix test-suite scripts: [Generalizable Variables] and small Gravatar msozeau2009-11-13
| | | | | | | changes in obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on fixing #2167Gravatar herbelin2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les ↵Gravatar notin2009-11-12
| | | | | | 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
* Oops, nf_evar_defs just changed to nf_evar_map.Gravatar msozeau2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12511 85f007b7-540e-0410-9357-904b9bb8a0f7
* Don't forget to normalize everything w.r.t. evars (fixes bug #2103).Gravatar msozeau2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore test-suite/csdp.cache erased from svn by mistakeGravatar letouzey2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12508 85f007b7-540e-0410-9357-904b9bb8a0f7
* BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)Gravatar letouzey2009-11-12
| | | | | | | | | | | | | | | | | | | | | | | - 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
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
| | | | | | abbreviations of applied references. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addendum to revision 12501.Gravatar herbelin2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
| | | | | | | | | | | | | | | 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
* Better compatibility for PeqbGravatar letouzey2009-11-11
| | | | | | | | | 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
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtracking on the use of automatically generated schemes forGravatar herbelin2009-11-11
| | | | | | | | | "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
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redoing broken commit r12498 (fixing bug #2167 + attempt to test theGravatar herbelin2009-11-11
| | | | | | | 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
* Fixing bug #2167 + attempt to test the compatibility of a more robustGravatar herbelin2009-11-11
| | | | | | 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
* Test for bug #2168, forgotten in r12496.Gravatar herbelin2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2168 (closing a section may have as side-effect the erasureGravatar herbelin2009-11-11
| | | | | | 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
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
| | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Compatibility ocaml <= 3.09Gravatar herbelin2009-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #2183Gravatar notin2009-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12492 85f007b7-540e-0410-9357-904b9bb8a0f7
* use only why-dp, support for z3Gravatar marche2009-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12491 85f007b7-540e-0410-9357-904b9bb8a0f7
* SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxGravatar letouzey2009-11-10
| | | | | | | | 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
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
| | | | | | | | | | | | | | | | | - 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
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
| | | | | | + 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
* Deactivation of (intrusive) printing of abbreviations from non-imported modules.Gravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit 12485 continued.Gravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12486 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-28 02:38:51 +0000