aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-06-03Misc fixes related to new nsatz (and ocamlbuild)letouzey
- 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
2010-06-03Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13060 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03nsatz ajoutepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13058 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03ajout oubliepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13057 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of ↵pottier
nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix xml test in non-local modeglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13055 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Do not link system library into installed .cmaglondu
Linking a system library into a .cma can lead to some system module (such as Unix) being linked twice in an executable, resulting in possibly hard-to-debug errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13054 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix typosglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix test-suite cleaningglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13052 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Extraction: start of a support libraryletouzey
- 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
2010-06-01added -args option to coqide to pass options to coqtopsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13046 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13045 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-01restore handling of lexer errorsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13044 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31CoqIDE goes multiprocessvgross
This commit changes many things in CoqIDE, and several breakage are to be expected. So far, evaluation in standard tactic mode and backtracking seems to be working. Future work : - clean up the thread management crud remaining in ide/coqide.ml - rework the exception handling - rework the init system in Coqtop plus many other things git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31More indirection.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13042 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31deporting Coq specific code from ide to toplevel.vgross
Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31Modifying startup sequencevgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13039 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-29New pass on inductive schemesherbelin
- Made "is defined" message quiet when a tactic define (via find_scheme) a scheme for internal use (in ind_tables.ml) - Improved documentation of eqschemes.ml (and swiched l2r/r2l terminology when talking about rewriting in hypotheses) - Took benefit of the new support for commutative cuts in the fixpoint guard checker for reducing the collection of rewriting schemes needed to implement the various kinds of rewriting (dependent or not, with symmetrical equality or not, in hypotheses or in conclusion, from left-to-right or from right-to-left) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13038 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-29Typo in comment of proof.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13037 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28A little bit of cleanup, and some annotations.fkirchne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Account for Stephane Glondu's remarks.fkirchne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13035 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Modify the test for csdp and associated message.fkirchne
Use the refactored system.ml function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13034 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Use existing functions to reimplement search_exe.fkirchne
Most of the code in search_exe_in_path was about parsing the PATH into a list of directories, which is now done in function lpath_from_path. Existence of the file is checked using already existing functions, so that duplication is minimized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13033 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28...fkirchne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13032 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Correction program_simplify. Devrait corriger certaines contribs.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13031 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Generalized the formulation of classic_set in propositional contextsherbelin
(consequence of classical unique choice) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13030 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Minor fix in doc chapter on inference rules (added a missing space).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13029 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Documentation of pretype_id (minor commit).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13028 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-26Fixing Derive Inversion for new proof engineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13027 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-22Added UIP_dec on suggestion of Eelis on #coq irc.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13026 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
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
2010-05-20Added examples for checking that the guard condition excludes subtermsherbelin
in impredicative types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13024 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20Fix bug 2307pboutill
Evars of source "ImpossibleCase" that remain undefined at the end of case analysis are now defined to ID (forall A : Type, A -> A). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13023 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20fixed guard check with commutative cutsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20Mrec was not substituted correctlybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13021 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Ocamlbuild: various fixletouzey
- 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
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
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
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
Cf tok.ml, token isn't anymore string*string where first string encodes the kind of the token, but rather a nice sum type. Unfortunately, string*string (a.k.a Plexing.pattern) is still used in some places of Camlp5, so there's a few conversions back and forth. But the penalty should be quite low, and having nicer tokens helps in the forthcoming integration of support for camlp4 post 3.10 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13018 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Discontinue support for ocaml 3.09.*letouzey
Ocaml 3.10.0 is already three year old... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Remove compile-command pragmas for emacsletouzey
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
2010-05-18Some ocamldoc comments + Fixing name of .coqrc.version file in refmanpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
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
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
evar_map into a map for defined evars and a map for undefined evars. Even before Spiwack's new proof engine, some Evd.fold were very costly, e.g. in check_evars or progress_evar_map. With the new proof engine, undefined evars traversals are apparently even more common (at least, it improves significantly the complexity of some calls to omega in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained by removal of evar_merge in clenv_fchain in commit 13007, arriving to figures comparable to the 8.3 ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-12Missing warning flush in a lexer message + update of CHANGESherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13010 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-10Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13009 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-10Fix: Pfedit.get_current_goal_context when no goal is focused.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13008 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-10Removed an evar_merge in clenv_fchain which not only is incorrect butherbelin
is an important cause of inefficiency when the number of evars is large. It is wrong in the sense that it assumes the two sigma given to clenv_fchain to be disjoint. This is true for metas, but not for evars. It used to be useful in some respect when clenv bindings were represented by open_constr, each of them having private evars (see r10151 which introduced this evar_merge), but determining what evars were private which and were shared is hopeless. Since the removal of private sigmas in r12603, evars in clenv bindings are assumed to be extended monotonically and clenv_fchain should only have to take the most recent evars - assumed to be the first argument - instead of a union. The function clenv_fchain remains anyway fragile since it is asymmetric. More should be done to clean it up so that it receives only one - unambiguous - evars argument, what would mean actually, receiving only one clausenv and the second argument being just a template pair (t:T). The call to evar_merge was source of inefficiency. On some calls to omega in contrib JordanCurveTheorem, removing it reduces the execution time by a factor larger than 5 (from 400s down to 70s on my Core 2 Duo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13007 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:00:43 +0000