aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implement the substitution function for global options. Fixes anomaly in ↵Gravatar msozeau2012-02-23
| | | | | | ssreflect compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14991 85f007b7-540e-0410-9357-904b9bb8a0f7
* sequel of previous commitGravatar letouzey2011-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolate a few types of Goptions in a pure .mli, solving a dep issue with ↵Gravatar letouzey2011-12-21
| | | | | | | | | | | | | | ocamlbuild A few types of Goptions are mentioned in toplevel/interface.mli. Since the latter is a pure .mli, this shouldn't trigger a dependency with respect to goptions.ml, but apparently ocamlbuild isn't clever enough to notice this, and hence wants to link a pile of useless stuff with coqide. I'll discuss with Pierre-Marie about the best long-term way to avoid this mess, but in the meantime I split the concerned types of Goptions in a separate Goptionstyp.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
| | | | | | | | | arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
| | | | | | | | | | as to ensure the warning is flushed in real time. Made systematic the use of if_warn instead of if_verbose when the warning is intended to signal something anormal (if_warn is activated when compiling verbosely and when working interactively while if_verbose is activated only when working interactively and when loading verbosely). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof using ...Gravatar gareuselesinge2011-12-12
| | | | | | | | | | | | | New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
| | | | | | | | | | | | | | | | - Implicit arguments can be mentioned anonymously: Arguments map {_ _} f l. - To rename implicit arguments, the ": rename" flag must be used: Arguments map {T1 T2} f l : rename. Without the ": rename" flag arguments can be used to assert that a function has indeed the expected number of arguments and that the arguments are named as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a function to inspect current option state.Gravatar ppedrot2011-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
| | | | | | | | Example: Arguments eq_refl {B y}, [B] y. Check (eq_refl (B := nat)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
* New Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new vernacular "Arguments" attaches to constants the extra-logical piece of information regarding implicit arguments, notation scopes and the behaviour of the simpl tactic. The About vernacular is extended to print the new extra logical data for simpl. Examples: Arguments foo {A B}%type f [T] x. (* declares A B and T as implicit arguments, A B maximally inserted. declares type_scope on A and B *) Arguments foo {A%type b%nat} p%myscope q. (* declares A and b as maximally inserted implicit arguments. declares type_scope on A, nat_scope on b and the scope delimited by myscope on p *) Arguments foo (A B)%type c d. (* declares A and b in type_scope, but not as implicit arguments. *) Arguments foo A B c. (* leaves implicit arguments and scopes declared for foo untouched *) Arguments foo A B c : clear implicits (* equivalente too Implicit Arguments foo [] *) Arguments foo A B c : clear scopes (* equivalente too Arguments Scope foo [_ _ _] *) Arguments foo A B c : clear scopes, clear implicits Arguments foo A B c : clear implicits, clear scopes Arguments foo A B c : clear scopes and implicits Arguments foo A B c : clear implicits and scopes (* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *) Arguments foo A B c : default implicits. (* equivalent to Implicit Arguments foo. *) Arguments foo {A B} x , A [B] x. (* equivalent to Implicit Arguments foo [[A] [B]] [B]. *) Arguments foo a !b c !d. (* foo is unfolded by simpl if b and d evaluate to a constructor *) Arguments foo a b c / d. (* foo is unfolded by simpl if applied to 3 arguments *) Arguments foo a !b c / d. (* foo is unfolded by simpl if applied to 3 arguments and if b evaluates to a constructor *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the type infrastructure to handle properly API management of optionsGravatar ppedrot2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
| | | | | | | | | | | | | | | | | These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
* First attempt at making Print Assumption compatible with opaque modules (fix ↵Gravatar letouzey2011-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | #2168) We replace Global.lookup_constant by our own code that looks for a module and enters its implementation. This is still preliminary work, I would prefer to understand more completely the part about module substitutions when entering an applied functor. But this code already appears to work quite well. Anyway, since we only search for constants, we don't need to reconstitute a 100% accurate environment, as long as the same objects are in it. Note: - Digging inside module structures is slower than just using Global.lookup_constant. Hence we try to avoid it as long as we could. Only in front of axioms (or in front of constant unknown to Global) do we check whether we have an inner-module implementation for this constant. There is some memoization of the search for internal structure_body out of a module_path. - In case of inner-module axioms, we might not be able to print its type, but only its long name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heads: avoid potentially uncaught Not_found via an assert falseGravatar letouzey2011-10-24
| | | | | | | | | | The underlying issue (#2608) should be fixed now. In case something similar happens again, we won't be chasing again a Not_found here. Same idea as commit r14550, but this initial attempt was too zealous: we shouldn't also "protect" variable_head, since a Not_found in it is handled a few lines later. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary revert commit 14550 since it breaks a few contribsGravatar letouzey2011-10-12
| | | | | | | | | | | Interestingly, it appears that the Not_found in heads.ml is actually triggered in some contribs, but catched. Maybe a "try" tactical ? Are these Not_found another effects of bug #2608 or something similar ? Anyway, replacing Not_found by "assert false" currently breaks these contribs. So for the moment, we revert to the original code. When bug #2608 will have been solved, we'll try again enabling these "assert false". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14560 85f007b7-540e-0410-9357-904b9bb8a0f7
* in heads.ml, at least turn the Not_found of #2608 into assert falseGravatar letouzey2011-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
| | | | | | | | | | Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
| | | | | | | | | | Maybe could we keep only the kernel check, but message would certainly need to be reformulated then. For instance, the message was previously different for an attempt to redefine a name whether this name was in the same section or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
| | | | | | | | There were some confusion on the role of clear_proofs which was applicable only to the global named_context. Hopefully made things clearer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14517 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completing r14448 and thus continuing r14407 (using Cast to propagateGravatar herbelin2011-09-24
| | | | | | | | | | | | | | | | | | | | | information coming from tactics on how to solve cst/cst critical pairs in the kernel conversion machine). In r14448, extra Cast's were removed from kernel type-checker but (erroneously) not from the terms actually registered in the environment. The current commit completes the work by registering the term output by the type-checker and not the original term. Note that this needs to move hconsing from before to after typing. On the Coq library, propagating Cast (without keeping them on disk) induces a stable 1% speedup (Xeon w3540). Having hcons before or after type-checking makes no difference. It remains to test on user contribs whether the current commit compensates the slow down and vo size increasing coming with the improvement made to Qed in r14407. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
| | | | | | | | | | | | Now that Yann has provided a better hashing mechanism for constr, it might be interesting to (re-?)activate a global hash-consing of constr. Earlier, specific hash-cons tables were created at each call to hcons_constant_declaration. According to Hugo, this was meant to avoid blow-up in at least contrib Pocklington. This contrib seems to behave nicely now with global hashconsing (thanks Yann ;-). We'll see tomorrow what impact this has on other contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: new backtracking code, based on the Backtrack commandGravatar letouzey2011-09-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This approach, inspired by ProofGeneral, is *much* simplier than earlier, and should be more robust (I hope! feedback of testers is welcome). Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases. A stack on the coqtop side (in Ide_slave) convert this phrase count to labels in the sense of Backtrack, and to abort + depth informations concerning proofs. We avoid re-entering finished proofs during Rewind by some extra backtracking until before these proofs. The amount of extra backtracking is then answered by coqtop to coqide. Now: - for go_to_insert (the "goto" button), unlike PG, coqide replays the extra backtracked zone. - for undo_last_step (the "back" button), coqide now leaves the extra backtracked zone undone, just like PG. This happens typically when undoing a Qed, and this should be the only visible semantical change of this patch. Two points to check with Pierre C: - such a coqtop-side stack mapping labels to opened proofs might be interesting to PG, instead of passing lots of info via the prompt and computing stuff in emacs. - Unlike PG, we allow re-entering inside a module / section, while PG retracts to the start of it. Coqide seems to work fine this way, to check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lib: remove strange code about backtracking to the current stateGravatar letouzey2011-09-05
| | | | | | | We now forbid a "BackTo n" or "Backtrack n _ _" when n is the current label or a future one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14453 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lib.node: merge OpenedModtype and OpenedModule, same for Closed...Gravatar letouzey2011-09-05
| | | | | | This allows more sharing of code (cf. start_module / end_module) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heads: generic equality on constr replaced by destructorGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
| | | | | | | The env was used for a particular case of Cbytegen.compile_constant_body, but we can actually guess that it will answer a particular BCallias con. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "Print Module M" prints now by default both a signature (fields with their types) and a body (fields with their types and transparent bodies). "Print Module Type M" could be used both when M is a module or a module Type, it will only display th signature of M. The earlier minimalist behavior (printing only the field names) could be reactivated by option "Set Short Module Printing". For the moment, the content of internal sub-modules and sub-modtypes are not displayed. Note: this commit is an experiment, many sitations are still unsupported. When such situations are encountered, Print Module will fall back on the earlier minimalist behavior. This might occur in particular in presence of "with" annotations, or in the conjonction of a non-global module (i.e. functor or module type) and internal sub-modules. Side effects of this commit: - a better compare function for global_reference, with no allocations at each comparison - Nametab.the_globrevtab is now searched according to user part only of a kernel_name - The printing of an inductive block is now in Printer, and rely less on the Nametab. Instead, we use identifiers in mind_typename and mind_consnames. Note that Print M.indu will not display anymore the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
| | | | | | | | | | | This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goptions: repair Unset for int optionsGravatar letouzey2011-03-17
| | | | | | | | | Previous code was trying to do a bool write, and in case of error, a int write. But for compatibility reason, bool write error were turned into warnings, preventing Unset Foo Bar to work when Foo Bar is an int option. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
| | | | | | (in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Annotations at functor applications:Gravatar letouzey2011-02-11
| | | | | | | | | | | | | - The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]" - The earlier syntax !F X should now be written "F X [no inline]" (note that using ! is still possible for compatibility) - A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute foo_scope by bar_scope in all arguments scope of objects in F. BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier. Arguments scope for lemmas are fixed for instances of Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
* More comments and less doublons in some mliGravatar pboutill2011-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13820 85f007b7-540e-0410-9357-904b9bb8a0f7
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix some typosGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code improvements around libobjectGravatar herbelin2010-10-31
| | | | | | | | - renamed load_object in mltop into load_ml_object to avoid confusion with load_object in library - flushed the liboject warning in real time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
| | | | | | | discharge bug of implicit arguments related to commit 13484 (multiple implicit arguments sequences patch). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
| | | | | | | | | - fixing r13483 (supposed dead code in impargs was actually half-living: implicit arguments mode should merge with the {...} manually given implicit arguments but not with the "Implicit Arguments [...]" arguments), - fixing code of drop_first_implicits in r13484. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
| | | | | | | | | Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead code in impargs (afaics, no more need, since r11242, to mergeGravatar herbelin2010-10-03
| | | | | | automatic and manual implicit arguments twice). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13483 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
| | | | | | | | | | | | | | | | | too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
| | | | | | | | | | | | | | | (declare_constant_gen was not exported, leading to a lot of silly tests before calling those functions) and replaced them by declare_constant : ?internal:internal_flat -> ... declare_constant's default behaviour is the same as the old declare_constant. * fixed the default behaviour of inductive scheme failure during coq's compilation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
* * library/Library: Reformulate a comment.Gravatar regisgia2010-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13382 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:10:04 +0000