aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rlogic.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-16 13:56:19 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-16 13:56:19 +0000
commitc215c4429a85a6d73cc1a33041258cacbe4de199 (patch)
tree4af1be58159858191ab85936ac57bd042853a4ae /theories/Reals/Rlogic.v
parenta869d74f414ba786c66b8eb7450ff6343ff12ebd (diff)
Take advantage of natdynlink when available: almost all contribs become loadable plugins
- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rlogic.v')
-rw-r--r--theories/Reals/Rlogic.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 8aadf8f5d..e535a5568 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -177,7 +177,7 @@ assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
split;
intros H;
simpl; unfold g;
- destruct (eq_nat_dec 0 n); try reflexivity.
+ destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity.
elim f; auto with *.
elimtype False; omega.
destruct IHa as [IHa0 IHa1].