aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-04-08ocamlbuild: right symlink for csdpcertletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12074 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Take formatted into account in rules for dot.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12072 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Experimental support for automatic destruction of recursive calls andmsozeau
clearing of recursive protototypes in Program obligations. Relies on marking said prototypes with a particular constant and preprocessing obligation goals with an appropriate tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12071 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Fix bug #2083 for good: verify that the measure and relation aremsozeau
well-formed before doing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12070 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Some dead code removal + cleanupsletouzey
This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08ocamlbuild: tags for new file tactics/rewrite.ml4letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12068 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Change HTML paragraph output to avoid too much space after bulletedmsozeau
lists, patch by B. Pierce. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12067 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branchherbelin
(r12063) for smooth compilation/installation under Solaris (/bin/sh -> /bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than in if). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
it does not cause a time penalty. - Removing of get_type_of_with_meta made possible by the evar_defs/evar_map merge. - Adding unfolding of Meta in reductionops (this assumes that reduction does not move Metas across binders...) - Renaming newly created fold_map_rel_context into map_rel_context_in_env. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12061 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08A first pearl found by the Oug analyzer: there were two list_map_i in Utilletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12060 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
Not_found bug in Theorem with) from V8.2 to trunk. - Improving indentation in presence of tabulation and utf-8 when reporting error messages with "^^^^^^". - Updating a few svn:ignore properties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-07Fixes in Program: msozeau
- unnecessary and inefficient nf_evar_defs in coercion code - use new way of inferring match return clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12057 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-07Move setoid_rewrite to its own module and do some clean up inmsozeau
class_tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12056 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-06Fix behavior on newlines with parse-comments and also do [] escaping as msozeau
usual in this mode (report and request by B. Pierce). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12054 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-06correction bug 2085soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12052 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-05Display the content of the list instead of "<list>" when an idtacherbelin
argument is a variable bound to a list (see S. Lescuyer's message on coq-club, Apr 5, 2009). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12050 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-03Fix obvious bug in evars_of_named_context.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12049 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-03Ocamlbuild: option for (not) building coqide, better log messagesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12048 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-03Makefile: ocamlbuild's _build is not traversed by find, and removed by make ↵letouzey
clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12047 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-03Ocamlbuild: improvements suggested by N. Pouillardletouzey
* Import of Coq_config via myocamlbuild_config.ml, instead of my get_env * As a consequence, we enrich this Coq_config with stuff that was only in config/Makefile * replace the big ugly find by some dependencies against source files * by the way: build csdpcert, with the right aliases. I've tried to escape things properly for windows in ./configure, but this isn't fully tested yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-31Fix auto so that Extern tactics associated to no patterns can apply tomsozeau
goals having no head constants (e.g. if the goal starts with a match). Fix an ordering bug in the (as yet undocumented) [dependent_pattern] tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12045 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-31Committed patch sent by Samuel Bronson on Mar 14 2009 to take care ofherbelin
.bzr files (Bazaar management files) in VCS clause (see 12043 in v8.2 branch). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12044 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-31Complementary fix to have ocamlopt_shared_os5fix.sh working correctlyherbelin
(tested on MacOS 10.5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12042 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Update CHANGESglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12040 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Document new quote constructionglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12039 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Add tests for quoteglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12038 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Add a more general quote constructionglondu
"quote f [...] in c using t" will call t (must be an ltac function) with a X (of form "f x" or "f vm x") such that X converts to c. In particular, match goal with | H : ?x |- _ => quote f in x using (fun X => change X in H) end may be used as an equivalent of plain quote that acts on an hypothesis. The construction can be used in a more general way, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12037 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Fix some typos and spacesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12036 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29Csdpcert: adaptation after last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12035 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29Micromega: improvement of the code obtained by extractionletouzey
* In eval_cone and simpl_cone, default patterns were leading to duplicated computations. Adaptation of RingMicromega.v to prevent that. * Use the Ocaml builtin types (lists, pairs, bool, etc) and remove the useless conversion functions in mutils.ml and alii. * andb was extracted to a correctly lazy but ugly match. Let's rather use Ocaml's (&&). Remain to be done: take advantage of extraction during the build, - either directly if we are using plugins, (no dependency issues) - or if we compile statically, at least check later that the micromega.ml in the archive and the one auto-generated are in sync. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
{measure ms [id] [(rel)]}. Fix script of bug #2083 and test-suite file accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12032 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28Fix useless redeclaration of a tactic name when UpdateTac is replayed.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12031 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
- The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28Fix bug #2056 (discharge bug).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12029 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28Fix static compilation of numeral syntax (typo in _mod files, sorry ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12028 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28ZArith/Int: no need to load romega here (but rather in FullAVL)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28ZMicromega: useless dependency toward ZArith.Intletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12026 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-27Coqdep: some dead code and code move (first experiment with Oug)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12025 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
Idea: make coqtop more independant of the standard library. In the future, we can imagine loading the syntax for numerals right after their definition. For the moment, it is easier to stay lazy and load the syntax plugins slightly before the definitions. After this commit, the main (sole ?) references to theories/ from the core ml files are in Coqlib (but many parts of coqlib are only used by plugins), and it mainly concerns Init (+ Logic/JMeq and maybe a few others). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-27Remove unused mli filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12023 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-27GroebnerZ: no more admitted lemmasletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12022 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)letouzey
Dealing with .vo files was harder than anticipated (issues with coqdep_boot and the location of the .v files). Current solution cannot compete for a beauty prize, but well. Several other issues remain (see top and bottom of myocamlbuild.ml) - For the moment the coqlib / coqsrc in Coq_config is to be hacked by hand to add _build/ in it. - Parallelism is a "no go" for the moment. Ocamlbuild accepts a -j option, but it has almost no effect experimentally. (but at least it doesn't take more time than make -j1, i.e. about 14 min here, instead of about 7 for make -j2) - After a first full build, ocamlbuild is awfully slow to detect that nothing has to be redone (1 min 25 here) To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Fixes in Program well-founded definitions:msozeau
- de Bruijn bug #2083 - Avoid useless eta-expansion (bug #2060) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12020 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26ocamlbuild: coqide, coqchk, a bit of .voletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Coqdep_boot: one line with bad indentationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12018 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Protect typeset arguments in titles in LaTeX output (fixes compilationmsozeau
errors in Library.coqdoc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12017 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26clean revision and coqdep_boot, toolmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12016 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26bin/coq-{parser,interface}: use this coqtop, not the first in $PATHlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12015 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 15:06:55 +0000