aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-10-23 the new .dir-locals.el thanks to Pierre Courtieupboutill
As it says : Set default directory to coq root ONLY IF variable coq-project-find-file is non nil. This should remain a user preference and not be set by default. This setting is redundant with compile-command above as M-x compile always CD's to default directory. To enable it add this to your emacs config: (setq coq-project-find-file t) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15924 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Text inserted by insert_this_phrase_on_success correct taggingpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15923 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Coqide for Gtk-mac-integration 2.0.0pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15922 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23RefMan-tac: fix a few glitches concerning the documentation of eqn:letouzey
These were introduced during Guillaume's backport to trunk of its improved tactic documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15920 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-22Fix bug #2892letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15916 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-22Coqide does not need dllcoqrun.sopboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15914 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Makefile.build: CONFIG is now in clibpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15909 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Do not install libcoqrun.so if compiled with -custompboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15908 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Cygwin gcc do not accept -mno-cygwin anymorepboutill
As far as I understand, the standard gcc in cygwin is not able anymore to build non cygwin executable. There is instead a special package with a special gcc that compiles executable that can be used out of cygwin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15907 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Fix test-suite output/* in benchpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Taking into account that ocamlfind might find a package w/o the filesherbelin
needed for compiling being present. Do the check by hand. Incidentally improved reporting messages. Also check gSourceview.cmi rather than gSourceview.mli for better guess that lablgtk sourceview bindings are there (I've seen installations where gSourceview.mli was here but not gSourceview.cmi). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15901 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Using weak tables instead of plain hash tables while hashconsing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Removing redundant definition of case_eq (see #2919).herbelin
Thanks to F. Blanqui for spotting it out. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15897 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.herbelin
Indeed r15885 still had problems (index contained referenced objects and not only defined objects, sorry). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Removed dead code about linking Module names in coqdoc.herbelin
Code was probably unused since scan_file made obsolete in r11024. See also r12890. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15892 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15891 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Egramml: minor simplificationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15890 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Stylistic improvement: avoid a "if match List.hd"letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15889 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Coq_makefile: easier compilation with timings info (from r15850)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Makefiles: Only -I required dirs (config, lib, ide) when compiling coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15887 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)pboutill
Allow to erase special $(CHKFLAGS) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15886 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵pboutill
introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev). Patch by Hugo Herbelin :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-14When loading a plugin, prefer .cma to .cmogareuselesinge
Imagine foo.cma contains foo_utils.cmo and foo.cmo. Also imagine that foo.cmo depends on foo_utils.cmo. With this patch, when asked to load foo, Coq loads the foo.cma archive. Loading simply foo.cmo would fail since foo_utils.cmo is needed to load foo.cmo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15883 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-08fix r15860 : no slash after $(COQLIB)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06restore compatibility with camlp5 < 6.00letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15881 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Coqmktop: a misplaced Filename.quote prevented temp file cleanupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15880 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Turn mltop.ml4 into a regular ocaml fileletouzey
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
2012-10-06ocamlbuild simplificationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15878 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Minor fix in the ./build wrapper for ocamlbuildletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15877 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06no need for camlp4 cma's in coq misc toolsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15876 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06still some more dead code removalletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06cosmetic concerning interp of TacShowHypsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15873 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06remove Refiner.abstract_tactic and similarletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06remove -rectypes except for term.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06remove dumptree.ml4letouzey
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
2012-10-06Adapt pieces of code needing -rectypesletouzey
* in Matching and Tacinterp : ad-hoc types for encoding matching result and "next" continuation * in Class_tactics, occurrences of types such as "type t = (foo * (unit->t) option" have been specialized to something like type t = TNone | TSome of foo * (unit -> t) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15869 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06avoid using rectypes in dnet.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15868 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06avoid using rectypes in nametab.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15867 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Tacexpr: revised version that doesn't need -rectypesletouzey
For that, gen_atomic_tactic_expr and gen_tactic_expr are now mutually recursive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15866 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
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
2012-10-06Proof_type: rule now degenerates to prim_ruleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
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
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
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
2012-10-05Fix a confusion between types of locations in an untyped part of the parserletouzey
after the migration of compat.ml4 This was leading to huge positions written to .glob files, making coqdoc loop forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15861 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-05Repair the configure after Hugo's last "repair" ;-)letouzey
Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH. But the last "repair" was worse, trying to write into non-existing file theories/config/coq_config.ml Things should be better now: * no more Coq_config.theories_dirs at all, since it was completely unused :-) * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins, hence keeping the "plugins/" part in their paths, and adapt accordingly the only use (!) of plugins_dirs, in coq_makefile Please run ./configure again after upgrading to this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-05coqtop -time : display per-command timingsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-05More accurate timings for "Time foo"letouzey
The elapsed time in seconds was computed via a difference of Unix.time(), but these Unix.time() aren't precise enough (just a number of seconds), and a difference is hence even less precise. We now use Unix.gettimeofday, and round the time difference to the millisecond. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15858 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:15:09 +0000