13 files changed, 73 insertions, 73 deletions

diff --git a/src/Reflection/Named/CompileInterp.v b/src/Reflection/Named/CompileInterp.v
index 6cb075f08..100d53aa3 100644
--- a/src/Reflection/Named/CompileInterp.v
+++ b/src/Reflection/Named/CompileInterp.v
@@ -54,7 +54,7 @@ Section language.
         (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False)
     : Named.interpf (interp_op:=interp_op) (ctx:=ctx) v
       = Some (interpf interp_op e').
-  Proof.
+  Proof using ContextOk Name_dec base_type_dec.
     revert dependent ctx; revert dependent ls; induction Hwf;
       repeat first [ progress intros
                    | progress subst
@@ -135,7 +135,7 @@ Section language.
         (H : ocompile e ls = Some f)
     : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v
                 = Some (interp interp_op e' v).
-  Proof.
+  Proof using ContextOk Name_dec base_type_dec.
     revert H; destruct Hwf;
       repeat first [ progress simpl in *
                    | progress unfold option_map, Named.interp in *
@@ -179,7 +179,7 @@ Section language.
         (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False)
     : Named.interpf (interp_op:=interp_op) (ctx:=ctx) v
       = Some (interpf interp_op e').
-  Proof.
+  Proof using ContextOk Name_dec base_type_dec.
     eapply interpf_ocompilef; try eassumption.
     setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst.
     eauto.
@@ -192,5 +192,5 @@ Section language.
         (H : compile e ls = Some f)
     : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v
                 = Some (interp interp_op e' v).
-  Proof. eapply interp_ocompile; eassumption. Qed.
+  Proof using ContextOk Name_dec base_type_dec. eapply interp_ocompile; eassumption. Qed.
 End language.
diff --git a/src/Reflection/Named/CompileWf.v b/src/Reflection/Named/CompileWf.v
index 3f322aed5..5fb17b18d 100644
--- a/src/Reflection/Named/CompileWf.v
+++ b/src/Reflection/Named/CompileWf.v
@@ -55,7 +55,7 @@ Section language.
         (Hls : oname_list_unique ls)
         (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False)
     : prop_of_option (nwff ctx v).
-  Proof.
+  Proof using ContextOk Name_dec base_type_dec.
     revert dependent ctx; revert dependent ls; induction Hwf;
       repeat first [ progress intros
                    | progress subst
@@ -165,7 +165,7 @@ Section language.
         (Hls : oname_list_unique ls)
         (H : ocompile e ls = Some f)
     : nwf ctx f.
-  Proof.
+  Proof using ContextOk Name_dec base_type_dec.
     revert H; destruct Hwf;
       repeat first [ progress simpl in *
                    | progress unfold option_map, Named.interp in *
@@ -210,7 +210,7 @@ Section language.
         (Hls : name_list_unique ls)
         (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False)
     : prop_of_option (nwff ctx v).
-  Proof.
+  Proof using ContextOk Name_dec base_type_dec.
     eapply wff_ocompilef; try eassumption.
     setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst.
     eauto.
@@ -222,5 +222,5 @@ Section language.
         (Hls : name_list_unique ls)
         (H : compile e ls = Some f)
     : nwf ctx f.
-  Proof. eapply wf_ocompile; eassumption. Qed.
+  Proof using ContextOk Name_dec base_type_dec. eapply wf_ocompile; eassumption. Qed.
 End language.
diff --git a/src/Reflection/Named/ContextProperties.v b/src/Reflection/Named/ContextProperties.v
index 4bd0325fb..c031d0af2 100644
--- a/src/Reflection/Named/ContextProperties.v
+++ b/src/Reflection/Named/ContextProperties.v
@@ -31,7 +31,7 @@ Section with_context.
         T N t n v
     : lookupb (extend ctx N (t:=T) v) n t
       = find_Name_and_val t n N v (lookupb ctx n t).
-  Proof. revert ctx; induction T; t. Qed.
+  Proof using ContextOk. revert ctx; induction T; t. Qed.
 
   Lemma find_Name_and_val_Some_None
         {var' var''}
@@ -42,7 +42,7 @@ Section with_context.
         (H0 : @find_Name_and_val var' t n T N x default = Some v)
         (H1 : @find_Name_and_val var'' t n T N y default' = None)
     : default = Some v /\ default' = None.
-  Proof.
+  Proof using Type.
     revert dependent default; revert dependent default'; induction T; t.
   Qed.
 
@@ -54,7 +54,7 @@ Section with_context.
         (H : @find_Name n T N <> None)
     : @find_Name_and_val var' t n T N x default
       = @find_Name_and_val var' t n T N x None.
-  Proof. revert default; induction T; t. Qed.
+  Proof using Type. revert default; induction T; t. Qed.
   Hint Rewrite @find_Name_and_val_default_to_None using congruence : ctx_db.
 
   Lemma find_Name_and_val_different
@@ -64,7 +64,7 @@ Section with_context.
         {default}
         (H : @find_Name n T N = None)
     : @find_Name_and_val var' t n T N x default = default.
-  Proof. revert default; induction T; t. Qed.
+  Proof using Type. revert default; induction T; t. Qed.
   Hint Rewrite @find_Name_and_val_different using assumption : ctx_db.
 
   Lemma find_Name_and_val_wrong_type_iff
@@ -75,7 +75,7 @@ Section with_context.
         (H : @find_Name n T N = Some t')
     : t <> t'
       <-> @find_Name_and_val var' t n T N x default = None.
-  Proof. split; revert default; induction T; t. Qed.
+  Proof using Type. split; revert default; induction T; t. Qed.
   Lemma find_Name_and_val_wrong_type
         {var'}
         {t t' n T N}
@@ -84,14 +84,14 @@ Section with_context.
         (H : @find_Name n T N = Some t')
         (Ht : t <> t')
     : @find_Name_and_val var' t n T N x default = None.
-  Proof. eapply find_Name_and_val_wrong_type_iff; eassumption. Qed.
+  Proof using Type. eapply find_Name_and_val_wrong_type_iff; eassumption. Qed.
   Hint Rewrite @find_Name_and_val_wrong_type using congruence : ctx_db.
 
   Lemma find_Name_find_Name_and_val_wrong {var' n t' T V N}
     : find_Name n N = Some t'
       -> @find_Name_and_val var' t' n T N V None = None
       -> False.
-  Proof. induction T; t. Qed.
+  Proof using Type. induction T; t. Qed.
 
   Lemma find_Name_and_val_None_iff
         {var'}
@@ -101,7 +101,7 @@ Section with_context.
     : (@find_Name n T N <> Some t
        /\ (@find_Name n T N <> None \/ default = None))
       <-> @find_Name_and_val var' t n T N x default = None.
-  Proof.
+  Proof using Type.
     destruct (@find_Name n T N) eqn:?; unfold not; t;
       try solve [ eapply find_Name_and_val_wrong_type; [ eassumption | congruence ]
                 | eapply find_Name_find_Name_and_val_wrong; eassumption
@@ -117,14 +117,14 @@ Section with_context.
                      else None
         | None => default
         end.
-  Proof.
+  Proof using Type.
     t; erewrite find_Name_and_val_wrong_type by solve [ eassumption | congruence ]; reflexivity.
   Qed.
   Lemma find_Name_and_val_find_Name_Some
         {var' t n T N V v}
         (H : @find_Name_and_val var' t n T N V None = Some v)
     : @find_Name n T N = Some t.
-  Proof.
+  Proof using Type.
     rewrite find_Name_and_val_split in H; break_match_hyps; subst; congruence.
   Qed.
 End with_context.
diff --git a/src/Reflection/Named/ContextProperties/NameUtil.v b/src/Reflection/Named/ContextProperties/NameUtil.v
index c494acd2d..4853f9a41 100644
--- a/src/Reflection/Named/ContextProperties/NameUtil.v
+++ b/src/Reflection/Named/ContextProperties/NameUtil.v
@@ -46,7 +46,7 @@ Section with_context.
         (H : split_onames _ ls = (Some N, ls')%core)
     : (exists t, @find_Name n T N = Some t)
       <-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls).
-  Proof.
+  Proof using Type.
     revert dependent ls; intro ls; revert ls ls'; induction T; intros;
       [ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls)));
             specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ];
@@ -71,7 +71,7 @@ Section with_context.
         (H : split_onames _ ls = (Some N, ls')%core)
     : (exists t, @find_Name n T N = Some t)
       <-> List.In (Some n) ls /\ ~List.In (Some n) ls'.
-  Proof.
+  Proof using Type.
     rewrite (split_onames_find_Name (ls':=ls') (ls:=ls)) by assumption.
     rewrite (surjective_pairing (split_onames _ _)) in H.
     rewrite fst_split_onames_firstn, snd_split_onames_skipn in H.
@@ -86,7 +86,7 @@ Section with_context.
         (H : split_onames _ ls = (Some N, ls')%core)
         (Hfind : @find_Name n T N = Some t)
     : List.In (Some n) ls /\ ~List.In (Some n) ls'.
-  Proof.
+  Proof using Type.
     eapply split_onames_find_Name_Some_unique_iff; eauto.
   Qed.
 
@@ -96,7 +96,7 @@ Section with_context.
         (H : split_onames _ ls = (Some N, ls')%core)
     : @find_Name_and_val var' t n T N V None = Some v
       <-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V).
-  Proof.
+  Proof using Type.
     revert dependent ls; intro ls; revert ls ls'; induction T; intros;
       [ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls)));
             specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ];
diff --git a/src/Reflection/Named/ContextProperties/SmartMap.v b/src/Reflection/Named/ContextProperties/SmartMap.v
index fd2144bed..89d0d1c5d 100644
--- a/src/Reflection/Named/ContextProperties/SmartMap.v
+++ b/src/Reflection/Named/ContextProperties/SmartMap.v
@@ -25,7 +25,7 @@ Section with_context.
         (H1 : @find_Name_and_val var' t n T N V1 None = Some v1)
         (H2 : @find_Name_and_val var'' t n T N V2 None = Some v2)
     : List.In (existT (fun t => (var' t * var'' t)%type) t (v1, v2)) (Wf.flatten_binding_list V1 V2).
-  Proof.
+  Proof using Type.
     induction T;
       [ | | specialize (IHT1 (fst N) (fst V1) (fst V2));
             specialize (IHT2 (snd N) (snd V1) (snd V2)) ];
@@ -38,7 +38,7 @@ Section with_context.
     : @find_Name n (SmartFlatTypeMap f (t:=T) V)
                  (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None
       <-> find_Name n N = None.
-  Proof.
+  Proof using Type.
     split;
       (induction T;
        [ | | specialize (IHT1 (fst V) (fst N));
@@ -50,19 +50,19 @@ Section with_context.
     : @find_Name n (SmartFlatTypeMap f (t:=T) V)
                  (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None
       -> find_Name n N = None.
-  Proof. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed.
+  Proof using Type. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed.
   Hint Rewrite @find_Name_SmartFlatTypeMapInterp2_None using eassumption : ctx_db.
   Lemma find_Name_SmartFlatTypeMapInterp2_None' {var' n f T V N}
     : find_Name n N = None
       -> @find_Name n (SmartFlatTypeMap f (t:=T) V)
                     (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None.
-  Proof. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed.
+  Proof using Type. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed.
   Lemma find_Name_SmartFlatTypeMapInterp2_None_Some_wrong {var' n f T V N v}
     : @find_Name n (SmartFlatTypeMap f (t:=T) V)
                  (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None
       -> find_Name n N = Some v
       -> False.
-  Proof.
+  Proof using Type.
     intro; erewrite find_Name_SmartFlatTypeMapInterp2_None by eassumption; congruence.
   Qed.
   Local Hint Resolve @find_Name_SmartFlatTypeMapInterp2_None_Some_wrong.
@@ -77,7 +77,7 @@ Section with_context.
                      end
         | None => None
         end.
-  Proof.
+  Proof using Type.
     induction T;
       [ | | specialize (IHT1 (fst V) (fst N));
             specialize (IHT2 (snd V) (snd N)) ].
@@ -110,7 +110,7 @@ Section with_context.
       -> @find_Name_and_val
            var''' t n T N (SmartFlatTypeMapUnInterp (f:=f) g X) None = Some v'
       -> g t b v = v'.
-  Proof.
+  Proof using Type.
     induction T;
       [ | | specialize (IHT1 (fst V) (fst N) (fst X));
             specialize (IHT2 (snd V) (snd N) (snd X)) ];
@@ -134,7 +134,7 @@ Section with_context.
       -> @find_Name_and_val
            var''' t n T N (SmartFlatTypeMapUnInterp (f:=f) g X) None = Some v'
       -> g t b v = v'.
-  Proof.
+  Proof using Type.
     induction T;
       [ | | specialize (IHT1 (fst V) (fst N) (fst X));
             specialize (IHT2 (snd V) (snd N) (snd X)) ];
@@ -154,7 +154,7 @@ Section with_context.
         (H1 : @find_Name_and_val var'' t n T N y None = Some v1)
         (HR : interp_flat_type_rel_pointwise R x y)
     : R _ v0 v1.
-  Proof.
+  Proof using Type.
     induction T;
       [ | | specialize (IHT1 (fst N) (fst x) (fst y));
             specialize (IHT2 (snd N) (snd x) (snd y)) ];
@@ -182,7 +182,7 @@ Section with_context.
                         :> { b : _ & var'' (f _ b)})
         (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=f) (fun _ _ n => n) _ N)
     : b = h v /\ find_Name_and_val (f t (h v)) n N' V None = Some (i v).
-  Proof.
+  Proof using Type.
     induction T;
       [ | | specialize (IHT1 (fst N) (fst B) (fst V));
             specialize (IHT2 (snd N) (snd B) (snd V)) ];
diff --git a/src/Reflection/Named/FMapContext.v b/src/Reflection/Named/FMapContext.v
index b838c1b4f..e01186f2c 100644
--- a/src/Reflection/Named/FMapContext.v
+++ b/src/Reflection/Named/FMapContext.v
@@ -37,7 +37,7 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E).
             := W.remove n ctx;
             empty := W.empty _ |}.
     Lemma FMapContextOk : @ContextOk base_type_code W.key var FMapContext.
-    Proof.
+    Proof using E_eq_l base_type_code_lb.
       split;
         repeat first [ reflexivity
                      | progress simpl in *
diff --git a/src/Reflection/Named/InterpretToPHOASInterp.v b/src/Reflection/Named/InterpretToPHOASInterp.v
index 7dcdc198b..4f66e94d4 100644
--- a/src/Reflection/Named/InterpretToPHOASInterp.v
+++ b/src/Reflection/Named/InterpretToPHOASInterp.v
@@ -30,7 +30,7 @@ Section language.
           (Hwf : prop_of_option (Named.wff ctx e))
       : Named.interpf (interp_op:=interp_op) (ctx:=ctx) e
         = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)).
-    Proof.
+    Proof using Type.
       revert dependent ctx; induction e;
         repeat first [ progress intros
                      | progress subst
@@ -58,7 +58,7 @@ Section language.
           v
       : Named.interp (interp_op:=interp_op) (ctx:=ctx) e v
         = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v).
-    Proof.
+    Proof using Type.
       unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas; auto.
     Qed.
   End with_context.
@@ -75,7 +75,7 @@ Section language.
           v
       : Named.interp (interp_op:=interp_op) (ctx:=ctx _) e v
         = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v).
-    Proof. apply interp_interp_to_phoas; auto. Qed.
+    Proof using Type. apply interp_interp_to_phoas; auto. Qed.
 
     Lemma Interp_InterpToPHOAS
           {t} (e : @Named.expr base_type_code op Name t)
@@ -83,6 +83,6 @@ Section language.
           v
       : Named.interp (Context:=Context _) (interp_op:=interp_op) (ctx:=empty) e v
         = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v).
-    Proof. apply interp_interp_to_phoas; auto. Qed.
+    Proof using Type. apply interp_interp_to_phoas; auto. Qed.
   End all.
 End language.
diff --git a/src/Reflection/Named/InterpretToPHOASWf.v b/src/Reflection/Named/InterpretToPHOASWf.v
index 86887cdee..daab24b62 100644
--- a/src/Reflection/Named/InterpretToPHOASWf.v
+++ b/src/Reflection/Named/InterpretToPHOASWf.v
@@ -73,7 +73,7 @@ Section language.
           (Hctx1_ctx2 : forall n t,
               lookupb ctx1 n t = None <-> lookupb ctx2 n t = None)
       : wff G (interpf_to_phoas failb1 ctx1 e) (interpf_to_phoas failb2 ctx2 e).
-    Proof.
+    Proof using Context1Ok Context2Ok Name_dec base_type_code_dec.
       revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e;
         repeat first [ progress intros
                      | progress destruct_head' and
@@ -95,7 +95,7 @@ Section language.
           (Hctx1 : forall n t, lookupb ctx1 n t = None)
           (Hctx2 : forall n t, lookupb ctx2 n t = None)
       : wf (interp_to_phoas failb1 ctx1 e) (interp_to_phoas failb2 ctx2 e).
-    Proof.
+    Proof using Context1Ok Context2Ok Name_dec base_type_code_dec.
       constructor; intros.
       apply wff_interpf_to_phoas; t.
     Qed.
@@ -105,7 +105,7 @@ Section language.
           (Hwf1 : Named.wf (Context:=Context1) empty e)
           (Hwf2 : Named.wf (Context:=Context2) empty e)
       : wf (interp_to_phoas (Context:=Context1) failb1 empty e) (interp_to_phoas (Context:=Context2) failb2 empty e).
-    Proof.
+    Proof using Context1Ok Context2Ok Name_dec base_type_code_dec.
       apply wf_interp_to_phoas_gen; auto using lookupb_empty.
     Qed.
   End with_var.
@@ -121,7 +121,7 @@ Section language.
           (Hctx : forall var n t, lookupb (ctx var) n t = None)
           (Hwf : forall var, Named.wf (ctx var) e)
       : Wf (InterpToPHOAS_gen failb ctx e).
-    Proof.
+    Proof using ContextOk Name_dec base_type_code_dec.
       intros ??; apply wf_interp_to_phoas_gen; auto.
     Qed.
 
@@ -129,7 +129,7 @@ Section language.
           {t} (e : @Named.expr base_type_code op Name t)
           (Hwf : Named.Wf Context e)
       : Wf (InterpToPHOAS (Context:=Context) failb e).
-    Proof.
+    Proof using ContextOk Name_dec base_type_code_dec.
       intros ??; apply wf_interp_to_phoas; auto.
     Qed.
   End all.
diff --git a/src/Reflection/Named/MapCastInterp.v b/src/Reflection/Named/MapCastInterp.v
index 1fe175879..b7afa1494 100644
--- a/src/Reflection/Named/MapCastInterp.v
+++ b/src/Reflection/Named/MapCastInterp.v
@@ -210,7 +210,7 @@ Section language.
       r' (Hr':interpf (interp_op:=interp_op) (ctx:=newValues) e' = Some r')
     , interpf (interp_op:=interp_op_bounds) (ctx:=varBounds) e = Some b
       /\ @inbounds _ b r /\ cast_back _ _ r' = r.
-  Proof.
+  Proof using Type*.
     induction e; simpl interpf; simpl mapf_cast; unfold option_map, cast_back in *; intros;
       repeat (break_match_hyps; inversion_option; inversion_sigma; simpl in *; unfold option_map in *; subst; try tauto).
     { destruct (Hctx _ _ _ Hr) as [b' [Hb'[Hb'v[v'[Hv' Hv'v]]]]]; clear Hctx Hr; subst.
@@ -254,7 +254,7 @@ Section language.
         r' (Hr':interp (interp_op:=interp_op) (ctx:=newValues) e' v' = Some r')
         , interp (interp_op:=interp_op_bounds) (ctx:=varBounds) e input_bounds = Some b
           /\ @inbounds _ b r /\ cast_back _ _ r' = r.
-  Proof.
+  Proof using Type*.
     unfold map_cast, option_map, interp; simpl; intros.
     repeat first [ progress subst
                  | progress inversion_option
diff --git a/src/Reflection/Named/MapCastWf.v b/src/Reflection/Named/MapCastWf.v
index a3196dbcc..f05df34c1 100644
--- a/src/Reflection/Named/MapCastWf.v
+++ b/src/Reflection/Named/MapCastWf.v
@@ -227,7 +227,7 @@ Section language.
         (Hb : find_Name_and_val base_type_dec Name_dec t n N B None = Some b)
         (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=pick_typeb) (fun _ _ n => n) _ N)
     : b = projT1 v /\ find_Name_and_val base_type_dec Name_dec (pick_typeb t (projT1 v)) n N' V None = Some (projT2 v).
-  Proof.
+  Proof using Type.
     eapply (find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some base_type_dec Name_dec (h:=@projT1 _ _) (i:=@projT2 _ _) (f:=pick_typeb) (g:=fun _ => existT _));
       auto.
   Qed.
@@ -254,7 +254,7 @@ Section language.
             -> lookupb (t:=t) varBounds n = Some (projT1 v)
                /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)),
       prop_of_option (Named.wff newValues e').
-  Proof. induction e; t. Qed.
+  Proof using BoundsContextOk ContextOk FullContextOk Name_dec base_type_dec. induction e; t. Qed.
 
   Lemma wf_map_cast
         {t} (e:expr base_type_code op Name t)
@@ -270,7 +270,7 @@ Section language.
             -> lookupb (t:=t) varBounds n = Some (projT1 v)
                /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)),
       Named.wf newValues e'.
-  Proof.
+  Proof using BoundsContextOk ContextOk FullContextOk Name_dec base_type_dec.
     unfold Named.wf, map_cast, option_map, interp; simpl; intros.
     repeat first [ progress subst
                  | progress inversion_option
diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v
index 8dcf32ec5..9a52ff49d 100644
--- a/src/Reflection/Named/NameUtilProperties.v
+++ b/src/Reflection/Named/NameUtilProperties.v
@@ -27,7 +27,7 @@ Section language.
       : split_mnames force t ls
         = (fst (split_mnames force t (firstn (count_pairs t) ls)),
            skipn (count_pairs t) ls).
-    Proof.
+    Proof using Type.
       apply path_prod_uncurried; simpl.
       revert ls; induction t; split; split_prod;
         repeat first [ progress simpl in *
@@ -56,17 +56,17 @@ Section language.
     Lemma snd_split_mnames_skipn
           (t : flat_type base_type_code) (ls : list MName)
       : snd (split_mnames force t ls) = skipn (count_pairs t) ls.
-    Proof. rewrite split_mnames_firstn_skipn; reflexivity. Qed.
+    Proof using Type. rewrite split_mnames_firstn_skipn; reflexivity. Qed.
     Lemma fst_split_mnames_firstn
           (t : flat_type base_type_code) (ls : list MName)
       : fst (split_mnames force t ls) = fst (split_mnames force t (firstn (count_pairs t) ls)).
-    Proof. rewrite split_mnames_firstn_skipn at 1; reflexivity. Qed.
+    Proof using Type. rewrite split_mnames_firstn_skipn at 1; reflexivity. Qed.
 
     Lemma mname_list_unique_firstn_skipn n ls
       : mname_list_unique force ls
         -> (mname_list_unique force (firstn n ls)
             /\ mname_list_unique force (skipn n ls)).
-    Proof.
+    Proof using Type.
       unfold mname_list_unique; intro H; split; intros k N;
         rewrite <- ?firstn_map, <- ?skipn_map, ?skipn_skipn, ?firstn_firstn_min, ?firstn_skipn_add;
         intros; eapply H; try eassumption.
@@ -85,7 +85,7 @@ Section language.
       := fun H => proj2 (@mname_list_unique_firstn_skipn n ls H).
     Lemma mname_list_unique_nil
       : mname_list_unique force nil.
-    Proof.
+    Proof using Type.
       unfold mname_list_unique; simpl; intros ??.
       rewrite firstn_nil, skipn_nil; simpl; auto.
     Qed.
@@ -96,29 +96,29 @@ Section language.
     : split_onames t ls
       = (fst (split_onames t (firstn (count_pairs t) ls)),
          skipn (count_pairs t) ls).
-  Proof. apply split_mnames_firstn_skipn. Qed.
+  Proof using Type. apply split_mnames_firstn_skipn. Qed.
   Lemma snd_split_onames_skipn
         (t : flat_type base_type_code) (ls : list (option Name))
     : snd (split_onames t ls) = skipn (count_pairs t) ls.
-  Proof. apply snd_split_mnames_skipn. Qed.
+  Proof using Type. apply snd_split_mnames_skipn. Qed.
   Lemma fst_split_onames_firstn
         (t : flat_type base_type_code) (ls : list (option Name))
     : fst (split_onames t ls) = fst (split_onames t (firstn (count_pairs t) ls)).
-  Proof. apply fst_split_mnames_firstn. Qed.
+  Proof using Type. apply fst_split_mnames_firstn. Qed.
 
   Lemma oname_list_unique_firstn n (ls : list (option Name))
     : oname_list_unique ls -> oname_list_unique (firstn n ls).
-  Proof. apply mname_list_unique_firstn. Qed.
+  Proof using Type. apply mname_list_unique_firstn. Qed.
   Lemma oname_list_unique_skipn n (ls : list (option Name))
     : oname_list_unique ls -> oname_list_unique (skipn n ls).
-  Proof. apply mname_list_unique_skipn. Qed.
+  Proof using Type. apply mname_list_unique_skipn. Qed.
   Lemma oname_list_unique_specialize (ls : list (option Name))
     : oname_list_unique ls
       -> forall k n,
         List.In (Some n) (firstn k ls)
         -> List.In (Some n) (skipn k ls)
         -> False.
-  Proof.
+  Proof using Type.
     intros H k n; specialize (H k n).
     rewrite map_id in H; assumption.
   Qed.
@@ -131,25 +131,25 @@ Section language.
     : split_names t ls
       = (fst (split_names t (firstn (count_pairs t) ls)),
          skipn (count_pairs t) ls).
-  Proof. apply split_mnames_firstn_skipn. Qed.
+  Proof using Type. apply split_mnames_firstn_skipn. Qed.
   Lemma snd_split_names_skipn
         (t : flat_type base_type_code) (ls : list Name)
     : snd (split_names t ls) = skipn (count_pairs t) ls.
-  Proof. apply snd_split_mnames_skipn. Qed.
+  Proof using Type. apply snd_split_mnames_skipn. Qed.
   Lemma fst_split_names_firstn
         (t : flat_type base_type_code) (ls : list Name)
     : fst (split_names t ls) = fst (split_names t (firstn (count_pairs t) ls)).
-  Proof. apply fst_split_mnames_firstn. Qed.
+  Proof using Type. apply fst_split_mnames_firstn. Qed.
 
   Lemma name_list_unique_firstn n (ls : list Name)
     : name_list_unique ls -> name_list_unique (firstn n ls).
-  Proof.
+  Proof using Type.
     unfold name_list_unique; intro H; apply oname_list_unique_firstn with (n:=n) in H.
     rewrite <- firstn_map; assumption.
   Qed.
   Lemma name_list_unique_skipn n (ls : list Name)
     : name_list_unique ls -> name_list_unique (skipn n ls).
-  Proof.
+  Proof using Type.
     unfold name_list_unique; intro H; apply oname_list_unique_skipn with (n:=n) in H.
     rewrite <- skipn_map; assumption.
   Qed.
@@ -159,7 +159,7 @@ Section language.
         List.In n (firstn k ls)
         -> List.In n (skipn k ls)
         -> False.
-  Proof.
+  Proof using Type.
     intros H k n; specialize (H k n).
     rewrite !map_id, !firstn_map, !skipn_map in H.
     eauto using in_map.
@@ -170,7 +170,7 @@ Section language.
   Lemma length_fst_split_names_Some_iff
         (t : flat_type base_type_code) (ls : list Name)
     : fst (split_names t ls) <> None <-> List.length ls >= count_pairs t.
-  Proof.
+  Proof using Type.
     revert ls; induction t; intros;
       try solve [ destruct ls; simpl; intuition (omega || congruence) ].
     repeat first [ progress simpl in *
@@ -195,7 +195,7 @@ Section language.
   Lemma length_fst_split_names_None_iff
         (t : flat_type base_type_code) (ls : list Name)
     : fst (split_names t ls) = None <-> List.length ls < count_pairs t.
-  Proof.
+  Proof using Type.
     destruct (length_fst_split_names_Some_iff t ls).
     destruct (le_lt_dec (count_pairs t) (List.length ls)); specialize_by omega;
       destruct (fst (split_names t ls)); split; try intuition (congruence || omega).
@@ -204,7 +204,7 @@ Section language.
   Lemma split_onames_split_names (t : flat_type base_type_code) (ls : list Name)
     : split_onames t (List.map Some ls)
       = (fst (split_names t ls), List.map Some (snd (split_names t ls))).
-  Proof.
+  Proof using Type.
     revert ls; induction t;
       try solve [ destruct ls; reflexivity ].
     repeat first [ progress simpl in *
diff --git a/src/Reflection/Named/PositiveContext/DefaultsProperties.v b/src/Reflection/Named/PositiveContext/DefaultsProperties.v
index 0fb1254ce..435a4c74c 100644
--- a/src/Reflection/Named/PositiveContext/DefaultsProperties.v
+++ b/src/Reflection/Named/PositiveContext/DefaultsProperties.v
@@ -16,7 +16,7 @@ Section language.
 
   Lemma name_list_unique_map_pos_of_succ_nat_seq a b
     : name_list_unique (map BinPos.Pos.of_succ_nat (seq a b)).
-  Proof.
+  Proof using Type.
     unfold name_list_unique, oname_list_unique, mname_list_unique.
     intros k n.
     rewrite !map_map, firstn_map, skipn_map, firstn_seq, skipn_seq.
@@ -28,11 +28,11 @@ Section language.
 
   Lemma name_list_unique_default_names_forf {var dummy t e}
     : name_list_unique (@default_names_forf base_type_code op var dummy t e).
-  Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
+  Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
   Lemma name_list_unique_default_names_for {var dummy t e}
     : name_list_unique (@default_names_for base_type_code op var dummy t e).
-  Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
+  Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
   Lemma name_list_unique_DefaultNamesFor {t e}
     : name_list_unique (@DefaultNamesFor base_type_code op t e).
-  Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
+  Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
 End language.
diff --git a/src/Reflection/Named/WfInterp.v b/src/Reflection/Named/WfInterp.v
index 17fc43ca5..c5fe2bb3a 100644
--- a/src/Reflection/Named/WfInterp.v
+++ b/src/Reflection/Named/WfInterp.v
@@ -15,7 +15,7 @@ Section language.
   Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t}
         (Hwf : prop_of_option (wff ctx e))
     : @interpf base_type_code interp_base_type op Name Context interp_op ctx t e <> None.
-  Proof.
+  Proof using Type.
     revert dependent ctx; induction e;
       repeat first [ progress intros
                    | progress simpl in *
@@ -34,7 +34,7 @@ Section language.
         (Hwf : wf ctx e)
         v
     : @interp base_type_code interp_base_type op Name Context interp_op ctx t e v <> None.
-  Proof.
+  Proof using Type.
     destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto.
   Qed.
 End language.