Merge pull request #866 from proux01/export-uniform-inductive-params

Replace #[global] with #[export] in derive.v

Author: gares

apps/derive/theories/derive.v

@@ -7,7 +7,7 @@
 (* since non-uniform inductive parameters are rarely used and the inference
    code from the kernel is not easily accessible, we require the user to
    be explicit about them, eg Inductive foo U1 U2 | NU1 NU2 := ... *)
-#[global] Set Uniform Inductive Parameters.
+#[export] Set Uniform Inductive Parameters.
 
 (** The derive command
    The derive command can be invoked in two ways.

apps/derive/theories/derive/eqType_ast.v

@@ -1,6 +1,6 @@
 From elpi Require Import elpi.
 From elpi.core Require Import PrimInt63 PrimFloat PrimString.
-From elpi.apps Require Import derive.
+From elpi.apps Require Export derive.
 
 From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType.
 From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook.

apps/derive/theories/derive/lens.v

@@ -7,7 +7,7 @@ From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook.
 From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
-From elpi.apps Require Import derive.
+From elpi.apps Require Export derive.
 
 (* Coq stdlib has no lens data type so we declare one here. To override with
   your own "copy", use Register as below *)