aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
| | | | | | | thunks. Move from [lazy] to [delayed] in subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13220 85f007b7-540e-0410-9357-904b9bb8a0f7
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
| | | | | | | | | | | | | | a 3 state type to allow: * KernelVerbose / KernelSilent : handle the display of messages launch by Coq * UserVerbose : handle the display of messages launch by user actions Coq will still behaves the same way (TODOs in the code mark the places where we can now change the behaviour). I'll remove them in a few days when we'll have agreed on the correct behaviour. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
| | | | | | | | | | | | them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: handling modules (not functors) in Haskell by name manglingGravatar letouzey2010-06-28
| | | | | | | | | | | | Module types are ignored, functors and module ident raise an error When dealing with simple modules, even nested, the structure hierarchy is removed, and names are arranged in the following way: - For the monolithic extraction, we simply use next_ident_away on short names, as we do when the same name appears in two .v. - For modular extraction, A.B.t become A__B__t or _A__B__t depending whether t is a type, a constructor or a constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: remove a useless matchGravatar letouzey2010-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13208 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug 2328 fixed: failure when polynomial not i idealGravatar pottier2010-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: nicer simple extraction of custom defs (fix #2204)Gravatar letouzey2010-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: replace unicode characters in ident by ascii encodings (fix ↵Gravatar letouzey2010-06-21
| | | | | | | | | | | | | | | | | | | #2158,#2179) Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is the hexa code for the unicode index of this character. For instance <alpha> is turned into __U03b1_. I know, this is ugly. Better solutions are welcome, but I'm afraid we can't do much better as long as ocaml and haskell don't accept unicode letters in idents. At least, this way we're pretty sure this translating won't create name conflit, as long as extraction users avoid __ in their names, something that they should already do btw (see for instance extraction of coinductive types in ocaml). Yes, I should add a test and a warning/error in case of use of __ someday. NB: this commit belongs proudly to the quick'n'dirty category git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: fix the eta reduction function used in code optimisationsGravatar letouzey2010-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: in support library, more and nicer big_intGravatar letouzey2010-06-15
| | | | | | | | | - we use a wrapper file big.ml to have short names about big_int and specialized functions for extraction - new files : ExtrOcamlZInt for Z==>int and N==>int, ExtrOcamlZBigInt for Z==>big_int and N==>big_int git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
| | | | | | | | | | checking function was used instead of a test of existence in the context. Also restricted constr_of_id which had no reason to interpret a posteriori an already interpreted identifier as a global reference. Consequently adapted funind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Implicits: can accept argument names instead of just positionsGravatar letouzey2010-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
| | | | | | | | products as implicit if they're part of a term and not a type (issue a warning instead). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing to use an ordering different than Lt with measureGravatar jforest2010-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using vernac parsing for FunctionGravatar jforest2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction with implicits: perform the occur-check after optimisationsGravatar letouzey2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
| | | | | | | people use the undocumented "Lemma foo x : t" feature in a way incompatible with this activation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in ExtrOcamlString: list char instead of char listGravatar letouzey2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13089 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
| | | | | | | binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: attempt to provide nice extraction of chars and strings for OcamlGravatar letouzey2010-06-04
| | | | | | | | | | | | | | When Requiring ExtrOcamlString : * ascii is mapped to Ocaml's char, the ugly translation of constructor and pattern-match should hopefully be seen very rarely (never ?). We add a hack in ocaml.ml for recognizing constant chars. * string is mapped to (list char). Extracting to Ocaml's string could be done, but would be really nasty (lots of non-trivial Extract Constant to add). For now, (list char) seems a good compromise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intGravatar letouzey2010-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
* plugins/xml: kill two warningsGravatar letouzey2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes related to new nsatz (and ocamlbuild)Gravatar letouzey2010-06-03
| | | | | | | | | - Kill a warning in ideal.ml corresponding to really brain-dead code. - Restore extraction/vo.otarget in pluginsvo.itarget - In fact, plugins/_tags can be merged into _tags with nice ** patterns - Update .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7
* nsatz ajouteGravatar pottier2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13058 85f007b7-540e-0410-9357-904b9bb8a0f7
* plugin groebner updated and renamed as nsatz; first version of the doc of ↵Gravatar pottier2010-06-03
| | | | | | nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typosGravatar glondu2010-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: start of a support libraryGravatar letouzey2010-06-02
| | | | | | | | | | | | - ExtrOcamlBasic: mapping of basic types to ocaml's ones - ExtrOcamlIntConv: conversion between int and coq's numerical types - ExtrOcamlBigIntConv: same with big_int (no overflow) - ExtrOcamlNatInt: realizes nat by int (unsafe) more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt, etc etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7
* A little bit of cleanup, and some annotations.Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modify the test for csdp and associated message.Gravatar fkirchne2010-05-28
| | | | | | Use the refactored system.ml function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13034 85f007b7-540e-0410-9357-904b9bb8a0f7
* ...Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
| | | | | | | | | | | For instance: Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n => if n=0 then fO () else fS (n-1))". See Extraction.v for more details and caveat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: various fixGravatar letouzey2010-05-19
| | | | | | | | | - transition to camlp4, with no compatibility for ocamlbuild+camlp5 (error message) - fix compilation of decl_mode : a forgotten include, and Decl_expr which is a pure .mli shouldn't be mentionned in the .mllib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
| | | | | | | | | | | | | | | | | | | | | In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm property of "u" in the analysis of "t". Commutative cuts aren't compatible with typing so we need to ensure that term of "x"'s type and term of "u"'s have the same subterm_spec. Consequently,declaration.MRec argument has changed to the inductive name instead of only the number of the inductive in the mutual_inductive family. In subterm_specif and check_rec_call, arguments are stored in a stack. At each lambda, one element is popped to add in renv a smarter subterm_spec for the variable. subterm_spec of constructor's argument was added this way, the job is now done more often. Some eta contracted match branches are now accepted but enforcing eta-expansion of branches might be anyway a recommended invariant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
* better detection of nested recursion in FunctionGravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of a bug pointed by P. Casteran.Gravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Trying to find a problem pointed by P. CasteranGravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of bug 2290 (removing stupid message)Gravatar jforest2010-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of bug 2290Gravatar jforest2010-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: fix type_expunge_from_sign broken in last commitGravatar letouzey2010-05-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: an experimental command to get rid of some cst/constructor argumentsGravatar letouzey2010-04-30
| | | | | | | | | | | | The command : Extraction Implicit foo [1 3]. will tell the extraction to consider fst and third arg of foo as implicit, and remove them, unless a final occur-check after extraction shows they are still there. Here, foo can be a inductive constructor or a global constant. This allow typicaly to extract vectors into usual list :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-28 21:39:18 +0000