…in case of -warn-universe-inconsistency.
considered small, in the sense that a type in Set does not get equality in Prop. This is the desired behavior for the homotopy interpretation where Set cannot be interpreted, say, as the intersection of hset and the lowest universe. It would still be good to make absence of -relevant-equality contaminant so that we cannot accidentally use the standard library when the option is present. And yes, there is no hope of compiling the standard library with this option turned on.
Added an option -relevant-equality to Coq which makes the logic compatible with a model such as the univalent model where proofs of equality are informative as soon as they involve elements in some Type level. This has an effect on the level in which universe-polymorphic inductive types are placed, which can be higher than w/o the option, and on which singleton eliminations are allowed, which can be less than w/o the option. How indices contribute: - Indices in A:Prop do not contribute to the level of an inductive nor on whether singleton elimination is allowed or not. - We chose to interpret Set as a sort in which proofs of equality are irrelevant (i.e. a sort in which Streicher's K holds). Hence indices in A:Set do not contribute to the level of the inductive. In particular, elimination from "Inductive eq (A:Set) (a:A) : A -> Prop := refl : eq A a a." is unrestricted. Similarly, the default lower level of polymorphic "Inductive eq (A:Set) (a:A) : A -> Type := refl : eq A a a." is Prop. - Indices in A:Type contribute to raising the level of a universe-polymorphic type. E.g. "Inductive eq (A:Type (* u *) ) (a:A) : A -> Type := refl : eq A a a." is in "Type (* u *)". Similarly, singleton elimination is forbidden from "Inductive eq (A:Type) (a:A) : A -> Prop := refl : eq A a a.". Remarks: - The modification applies uniformly to all inductive types with indices, not only those resembling equality. - The standard library stops to compile when the option is activated. - We could have been finer, and only restrict singleton eliminations dynamically depending on the level of the effective sort used. E.g. with "Inductive eq (A:Type) (a:A) : A -> Prop := refl : eq A a a.", we could have allowed "eq nat" to be eliminable to every sorts (because nat can be finally be put in Set and not in some higher Type). With this, a larger amount of the standard library could be compiled by reasoning in Set rather than in Type. However, this is not implemented.
…ngs, not adding the "offending" constraints. Cannot be turned on to errors again.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15880 85f007b7-540e-0410-9357-904b9bb8a0f7
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
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
* 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
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
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
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
…parser 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
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
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
Sorry, was committed mistakenly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15856 85f007b7-540e-0410-9357-904b9bb8a0f7
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
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