aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Repair the configure after Hugo's last "repair" ;-)Gravatar letouzey2012-10-05
| | | | | | | | | | | | | | | | | | 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
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
* More accurate timings for "Time foo"Gravatar letouzey2012-10-05
| | | | | | | | | 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
* Revert r15851 "En cours pour bug 2836".Gravatar herbelin2012-10-04
| | | | | | | | Sorry, was committed mistakenly. This reverts commit e9cb84af469519b824899c047eed1fed2f8d5af6. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "En cours pour 'generalize in clause' et 'induction in clause'"Gravatar herbelin2012-10-04
| | | | | | Sorry, was committed mistakenly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15856 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repaired configure damaged in r15748 for those bash users which haveGravatar herbelin2012-10-04
| | | | | | | CDPATH variable set. Indeed, command cd is verbose when CDPATH is set, what would introduce garbage in the generated file config/coq_config.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15855 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suggest to use clean rather than archclean before recompiling.Gravatar herbelin2012-10-04
| | | | | | | For instance, generated files depend on whether configuration is done with dynlink or not and they should be cleaned. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving error message when abtraction over goal (abstract_list_allGravatar herbelin2012-10-04
| | | | | | | used when applying schemes - induction, rewrite, ...) is well-typed but not of the right type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15853 85f007b7-540e-0410-9357-904b9bb8a0f7
* En cours pour 'generalize in clause' et 'induction in clause'Gravatar herbelin2012-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15852 85f007b7-540e-0410-9357-904b9bb8a0f7
* En cours pour bug 2836Gravatar herbelin2012-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: easier compilation with timings infoGravatar letouzey2012-10-04
| | | | | | | | | | | | | | | On a reasonable platform equipped with a /usr/bin/time, a simple "make TIMED=1" should provide you with timings of the .v compilations. If you don't have /usr/bin/time, or prefer a different output format, you can still do a "make TIMECMD='...'". For storing the timings in a spreadsheet, simply do: "make TIMED=1 2> timings.csv" and then import this csv in your favorite office program, with whitespace as separator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Compat in the checker.Gravatar ppedrot2012-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
| | | | | | | | things up. Records are used instead of their equivalents as tuples. This is maybe syntactically heavier, but this is semantically equivalent and easier to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 07:55:05 +0000