aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn mltop.ml4 into a regular ocaml fileGravatar letouzey2012-10-06
| | | | | | | | | | | | | | | | | | The IFDEF's in mltop.ml4 were there to support platforms with a native ocaml compiler but no dynlink.cmxa, a situation that should be pretty rare in the Coq community nowadays (playing with coqtop on ARM, anyone ?). So we now refuse to build a native coqtop unless dynlink.cmxa exists (cf ./configure), and we explain how to create a dummy one if necessary (cf dev/dynlink.ml). This way, we can clean-up mltop.ml, and remove ugly special rules in Makefile and myocamlbuild NB: I checked that this shouldn't have any impact on Coq's debian packages on exotic architectures (arm, mips, ...), since apparently on these architectures no ocamlopt at all are shipped, and coq packages are already byte-only git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7
* still some more dead code removalGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
| | | | | | Btw, remove unused code in the xml plugin and in Tactic_printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
| | | | | | | | | | | | kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove broken makefile option NO_RECOMPILE_LIBGravatar letouzey2012-09-20
| | | | | | | | | | | | | | | The idea was to allow rebuilding coqtop without the whole stdlib, but it's not working anymore since the stdlib also depends on plugins .cmxs, hence its compilation will be triggered anyway. Since I've no idea how to restore the old behavior (except via hacking the output of coqdep with more ORDER_ONLY hack), I simply declare this option dead, and remove it for improving clarity. NB: an imperfect workaround is to touch all the .vo after rebuilding coqtop and the plugins... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15823 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 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
* 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
* 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
* 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
* No need anymore to refer to COQLIB in ocamldebug-coqGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 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
* Revert "Fixing include printers"Gravatar pboutill2012-08-05
| | | | | | | | | If you add Auto to dev/printers.mllib, then you have to add Tacmach, so you have to add Redexpr, consequently Vnorm is required, it depends on Vm, that include externals ! Let's revert commit 15675. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing include printersGravatar ppedrot2012-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bigint: avoid dependency over PpGravatar letouzey2012-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Severe reorganisation of the code of tactics in Proofview.Gravatar aspiwack2012-07-11
| | | | | | | | | | | All the purely monadic code has been moved to a new module Monads, where, I'm afraid to confess, I got to use a number of proof transformers to modularise the definition of tactics. It is still not easy to understand (why would it with backtracking support?) but at least it's more robust, cleaner, and more extensible. Plus there is now a Proofview.tclORELSE which will be used to interprete the Ltac tactical (t1 || t2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15596 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
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15393 85f007b7-540e-0410-9357-904b9bb8a0f7
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Split Egrammar into Egramml and EgramcoqGravatar letouzey2012-05-29
| | | | | | | | Two gains: - no Summary in Grammar.cma - get rid of the hack concerning error_invalid_pattern_notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7
* global_reference migrated from Libnames to new Globnames, less deps in ↵Gravatar letouzey2012-05-29
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Strongly reduce the dependencies of grammar.cma, modulo two hacksGravatar letouzey2012-05-29
| | | | | | | | | | | - in g_constr.ml4, we avoid a dependency on Notation_ops by copying the pseudo-ident hack ldots_var = ".." - in egrammar.ml4 we duplicate the error message error_invalid_pattern_notaition. To adapt via Errors.register_handler... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
| | | | | | Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
| | | | | | | NB: former Tacexpr.no_move is now Tacexpr.MoveLast (when introducing, intro with no move is intro as last) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
| | | | | | Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide MacOS integration refreshGravatar pboutill2012-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing Dhyp from debugger.Gravatar herbelin2012-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Everything compiles again.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* Debugger vs tracer: Two different behaviors wrt printing: The debuggerGravatar herbelin2012-02-01
| | | | | | | | | runs in separate process. It has no access to the global env and it should not request it. The tracer runs in the same process as Coq and has full access to the global env and to regular pretty-printing of global names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added new command "Set Parsing Explicit" for deactivating parsing (andGravatar herbelin2012-01-20
| | | | | | printing) of implicit arguments (a priori useful for teaching). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suspending declaration of undefined debug printers.Gravatar herbelin2011-12-18
| | | | | | (Matthieu, do you have a definition for these printers around?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14814 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
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
| | | | | | | | | | | | | | This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 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
* Revert "New evar_map printer ppevmfull which can typically be installed for"Gravatar herbelin2011-10-17
| | | | | | | | | This reverts commit 44a6b1a7dcc483a3ef762a83cae2f771cddb09b6. As kindly noticed to me by Arnaud, this function already existed. Sorry about the noise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14569 85f007b7-540e-0410-9357-904b9bb8a0f7
* New evar_map printer ppevmfull which can typically be installed forGravatar herbelin2011-10-17
| | | | | | debugging with full sigma (typically for debugging type inference). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14567 85f007b7-540e-0410-9357-904b9bb8a0f7
* dev/base_include: display a nice message at the end of the loadGravatar letouzey2011-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14563 85f007b7-540e-0410-9357-904b9bb8a0f7
* debugging.txt: no more typing of #use "include" if using .ocamlinitGravatar letouzey2011-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14562 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
| | | | | | for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01
| | | | | | obfuscate the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14505 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 08:08:00 +0000