aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* 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
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
| | | | | | This correspond to ocaml4 warning 6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
| | | | | | type in "cast" to activate the temporary interpretation scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 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
* Added a CString module.Gravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 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
* correcting a little bug in FunctionGravatar jforest2012-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Implicit: consider the parameters of a constructor (fix #2905)Gravatar letouzey2012-10-30
| | | | | | | | | | | | | | | The parameters of a constructor C are part of the type of C, we should take them in account when retrieving the argument(s) declared as implicit. This way, the Extraction Implicit should now be correct when given named arguments of constructors with parameters. When positional numbers are given to Extraction Implicit, these numbers should now be increased by the number of parameters for this constructor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid initial strange empty comments after Arnaud's hackGravatar letouzey2012-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix Separate extraction when a module-as-file is aliased (#2917)Gravatar letouzey2012-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15940 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
* 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
* 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 useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove dumptree.ml4Gravatar letouzey2012-10-06
| | | | | | | | | | | This file was providing the "Dump Tree" command to display the state of a proof in XML. This command has been broken since the integration of Arnaud's proof engine. Nobody cared enough to adapt this to the new framework, moreover the trend is rather now to use the xml-base dialog mode of coqtop, so I simply remove this obsolete code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
| | | | | | | | This instance of gen_tactic_expr was used only to decorate tactics via Refiner.abstract_tactics and alii, but these expressions are now ignored by the new proof-engine (no "info"...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof_type: rule now degenerates to prim_ruleGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 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
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
| | | | | | | Nested was never constructed, while the notion of abstract_tactic_box is obsolete (cf. Refiner.abstract_tactic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 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
* 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
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15838 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
* Fixing a bug introduced in Funind plugin when reorganizing the CListGravatar ppedrot2012-09-24
| | | | | | module. Cleaned the code btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15827 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning in CArray...Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15819 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
* 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
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix Extraction Implicit on axioms.Gravatar aspiwack2012-08-24
| | | | | | | There was a small bug causing the type in OCaml commentary not to honor the implicit declaration, whereas the rest of the code did. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental support for a comment in the files' preamble in extraction.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | | | | Scheme comments are output on a single line because Ocaml's Format module which serves as a backend to Pp has an integer, rather than a string as identation value, so we cannot make it so that each new line in the comment starts with ";; ". I've tried something with Pp.ifb but it was hackish at best and had somewhat strange results. Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed only once per Extraction command, even if it outputs several files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | | | | | | Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 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
* Fixup for macOS 10.8 & Ocaml 4.0Gravatar pboutill2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vecnacentries.dump_global silently ignores exceptionsGravatar pboutill2012-08-06
| | | | | | So PrintName and Extraction dump globals when they exist git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15691 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to make the use of Unix.lockf in micromega compatible with Win32Gravatar letouzey2012-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dump references in ExtractionGravatar pboutill2012-08-05
| | | | | | Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dump referencesGravatar pboutill2012-08-05
| | | | | | Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bigint: new functions of_int and to_int, 2nd arg of pow in intGravatar letouzey2012-08-02
| | | | | | | | | | | | * Many of_string and to_string could be replaced by of_int and to_int when the number isn't too large. NB: to_int may raise a Failure if the number is larger than max_int. * In numbers_syntax, computing the height of bigN trees via bigint is *really* overkill, int should be enough there : this limits printable/parsable bigN to (2^31)^(2^max_int) ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of the undocumented [complete] tactic, which wasGravatar ppedrot2012-07-19
| | | | | | | redundant with [solve]. The AST node still exists in Ltac, because this is used by the [assert ... by ...] tactical. Fixes #2847. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes r15610 (A new status Unsafe in Interface).Gravatar aspiwack2012-07-13
| | | | | | Two warnings had passed my sensors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15619 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:17:05 +0000