aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
| | | | | | | | | | | | | | | | | | | | | | | | | | Why? : avoid catching (and probably ignoring) exceptions such as Sys.Break, anomalies, assertions, leading to undetected bugs and ignored Ctrl-C. How? : when the precise exception(s) concerned by the try is known, use them explicitely in the "with". Otherwise, let's use the pattern "with e when Errors.noncritical e -> " Particular case : when an exception is catched and reraised immediately after some adjustments, we leave it untouched. Simply, for easily identifying these situations later, the name of the exception variable is changed to "reraise". Please also adopt this coding style. Automatic checks based on the "mascot" tool of X. Clerc will be runned regularly. If you want to avoid to check a particular try...with, use the variable name "any" after the "with". All these changes have been tested using the standard library and the test-suite, but unfortunately this is far from ensuring that coqtop behaves as before. We'll see after the nightly bench... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
| | | | | | | has to be refered through its qualified name even when the module containing it is imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
| | | | | | | | - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
| | | | | | | | | * Remove the mind_of_delta and constant_of_delta functions, prefer instead the {mind,constant}_of_delta_kn functions. * Attempt to make subst_ind and subst_con0 more self-contained git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reduced the noise level when dynlinking in bytecode mode or whenGravatar mdenes2013-02-24
| | | | | | | | -no-native-compiler flag is on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16239 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dir_path --> DirPathGravatar letouzey2013-02-19
| | | | | | | | Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
* module_path --> ModPath.t, kernel_name --> KerName.tGravatar letouzey2013-02-19
| | | | | | | For the moment, the compatibility names about these new modules are still used in the rest of Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16220 85f007b7-540e-0410-9357-904b9bb8a0f7
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
| | | | | | | | | | | | Gmap uses Pervasives.compare which may interact badly with structures like pairs of kernel names For the moment, we consider elements in classes and coercions only according to their user kernel name: this provides maximal compatibility. But it could be interesting to try using comparision according to canonical kernel names... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
| | | | | | | | | - a module KernelPair for improving sharing between constant and mind - shorter representation than a pair when possible - exports comparisions on constant and mind and ... - a kn_equal function instead of Int.equal (kn_ord ...) 0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
* v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)Gravatar herbelin2013-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2966 (de Bruijn error in computation of heads for coercions).Gravatar herbelin2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
| | | | | | | I hope I did not forget some [with] clauses. Otherwise, some stack frame will be missing from the debug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving formatting of output of "Test table".Gravatar herbelin2013-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16159 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
| | | | | | | | | | | | | native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of nameGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of LabelGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of dir_pathGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
| | | | | | | hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (library)Gravatar ppedrot2012-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (library)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15993 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphizationsGravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
| | | | | | | | | | | | | | | | | the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2926:Gravatar ppedrot2012-10-29
| | | | | | | Extend "Print Opaque Dependencies" for transparent dependencies as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
| | | | | | | | writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
| | | | | | | | | | | | | instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid using rectypes in nametab.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15867 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
| | | | | | peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
| | | | | | Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Assumption commands are now displayed as unsafe in Coqide.Gravatar aspiwack2012-08-24
| | | | | | | | They are still marked as safe if they are part of a module type, though. Also local assumptions such as "Hypothesis" or "Context" are displayed as unsafe if they happen to be defined without a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 22:34:43 +0000