aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Removed a few calls to "Opaque" in Logic.v ineffective since at leastGravatar herbelin2012-10-24
| | | | | | V7.1. Thanks to Assia for reporting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqmktop: missing -I (fix #2851)Gravatar letouzey2012-10-23
| | | | | | | | | | | | The modules used in coqmktop's temporary main file should have their .cmi in the search path, hence a small set of -I is required: lib, toplevel. We do not place their the full list to avoid issues with the win32 command-line length Btw, coqmktop -boot now also builds its list of -I instead of receiving them via its command-line, it's simpler this way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
* the new .dir-locals.el thanks to Pierre CourtieuGravatar pboutill2012-10-23
| | | | | | | | | | | | 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
* Text inserted by insert_this_phrase_on_success correct taggingGravatar pboutill2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide for Gtk-mac-integration 2.0.0Gravatar pboutill2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15922 85f007b7-540e-0410-9357-904b9bb8a0f7
* RefMan-tac: fix a few glitches concerning the documentation of eqn:Gravatar letouzey2012-10-23
| | | | | | | 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
* Fix bug #2892Gravatar letouzey2012-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide does not need dllcoqrun.soGravatar pboutill2012-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: CONFIG is now in clibGravatar pboutill2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not install libcoqrun.so if compiled with -customGravatar pboutill2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cygwin gcc do not accept -mno-cygwin anymoreGravatar pboutill2012-10-17
| | | | | | | | 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
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
* Taking into account that ocamlfind might find a package w/o the filesGravatar herbelin2012-10-17
| | | | | | | | | | 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
* Using weak tables instead of plain hash tables while hashconsing.Gravatar ppedrot2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
| | | | | | 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
* 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
* Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.Gravatar herbelin2012-10-16
| | | | | | | 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
* Removed dead code about linking Module names in coqdoc.Gravatar herbelin2012-10-16
| | | | | | | 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
* Continue killing hidden tactics : no more generated h_xxxGravatar letouzey2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Egramml: minor simplificationGravatar letouzey2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stylistic improvement: avoid a "if match List.hd"Gravatar letouzey2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: easier compilation with timings info (from r15850)Gravatar pboutill2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefiles: Only -I required dirs (config, lib, ide) when compiling coqideGravatar pboutill2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)Gravatar pboutill2012-10-15
| | | | | | Allow to erase special $(CHKFLAGS) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵Gravatar pboutill2012-10-15
| | | | | | | | 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
* When loading a plugin, prefer .cma to .cmoGravatar gareuselesinge2012-10-14
| | | | | | | | | | 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
* fix r15860 : no slash after $(COQLIB)Gravatar letouzey2012-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
* restore compatibility with camlp5 < 6.00Gravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqmktop: a misplaced Filename.quote prevented temp file cleanupGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn mltop.ml4 into a regular ocaml fileGravatar letouzey2012-10-06
| | | | | | | | | | | | | | | | | | 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
* ocamlbuild simplificationsGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fix in the ./build wrapper for ocamlbuildGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15877 85f007b7-540e-0410-9357-904b9bb8a0f7
* no need for camlp4 cma's in coq misc toolsGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15876 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
* cosmetic concerning interp of TacShowHypsGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15873 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 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
* Adapt pieces of code needing -rectypesGravatar letouzey2012-10-06
| | | | | | | | | | | | * 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
* avoid using rectypes in dnet.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15868 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid using rectypes in nametab.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15867 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tacexpr: revised version that doesn't need -rectypesGravatar letouzey2012-10-06
| | | | | | | 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
* 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
* Fix a confusion between types of locations in an untyped part of the parserGravatar letouzey2012-10-05
| | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 15:03:56 +0000