Interp a definition with the implicit arguments of its local context

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13825 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 50 insertions, 50 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 55e545eda..52765ff12 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1617,12 +1617,12 @@ let my_intern_constr sigma env lvar acc c =
 
 let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
 
-let intern_context global_level sigma env params =
+let intern_context global_level sigma env impl_env params =
   let lvar = (([],[]), []) in
-    snd (List.fold_left
+  let lenv, bl = List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
-	      tmp_scope = None; scopes = []; impls = empty_internalization_env}, []) params)
+	      tmp_scope = None; scopes = []; impls = impl_env}, []) params in (lenv.impls, bl)
 
 let interp_rawcontext_gen understand_type understand_judgment env bl =
   let (env, par, _, impls) =
@@ -1647,15 +1647,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params =
-  let bl = intern_context global_level sigma env params in
-    interp_rawcontext_gen understand_type understand_judgment env bl
+let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
+  let int_env,bl = intern_context global_level sigma env impl_env params in
+    int_env, interp_rawcontext_gen understand_type understand_judgment env bl
 
-let interp_context ?(global_level=false) sigma env params =
+let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
   interp_context_gen (Default.understand_type sigma)
-    (Default.understand_judgment sigma) ~global_level sigma env params
+    (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params
 
-let interp_context_evars ?(global_level=false) evdref env params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
   interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
-    (Default.understand_judgment_tcc evdref) ~global_level !evdref env params
+    (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 97b0f4fd1..be78837ff 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -82,7 +82,7 @@ val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
     ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
 
-val intern_context : bool -> evar_map -> env -> local_binder list -> glob_binder list
+val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
 (** {6 Composing internalization with pretyping } *)
 
@@ -152,14 +152,14 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
 
 val interp_context_gen : (env -> glob_constr -> types) ->
   (env -> glob_constr -> unsafe_judgment) ->
-  ?global_level:bool ->
-  evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits
+  ?global_level:bool -> ?impl_env:internalization_env ->
+  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
   
-val interp_context : ?global_level:bool ->
-  evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits
+val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
+  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
-val interp_context_evars : ?global_level:bool ->
-  evar_map ref -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits
+val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
+  evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 640d3e60d..38f13a76e 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -34,9 +34,9 @@ let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internaliza
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
 let interp_context_evars evdref env params =
-  Constrintern.interp_context_gen
+  let impls_env, bl = Constrintern.interp_context_gen
     (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t)
-    (SPretyping.understand_judgment_tcc evdref) !evdref env params
+    (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl
 
 let type_ctx_instance evars env ctx inst subst =
   let rec aux (subst, instctx) l = function
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 6fe31646b..f02e83ad1 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -96,7 +96,7 @@ let interp_binder sigma env na t =
     SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
 
 let interp_context_evars evdref env params =
-  let bl = Constrintern.intern_context false !evdref env params in
+  let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 97ae56e16..19b4c3b2f 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -57,14 +57,14 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
   (H1: forall n (f: t n), P F1 (FS f))
   (H2: forall n (f: t n), P (FS f) F1)
   (HS: forall n (f g : t n), P f g -> P (FS f) (FS g)):
-    forall n (a b: t n), P n a b :=
-fix rect2_fix n (a: t n): forall (b: t n), P n a b :=
+    forall n (a b: t n), P a b :=
+fix rect2_fix n (a: t n): forall (b: t n), P a b :=
 match a with
   |F1 m => fun (b: t (S m)) => match b as b' in t n'
                    return match n' as n0
                           return t n0 -> Type with
                             |0 => fun _ => @ID
-                            |S n0 => fun b0 => P _ F1 b0
+                            |S n0 => fun b0 => P F1 b0
                           end b' with
                      |F1 m' => H0 m'
                      |FS m' b' => H1 m' b'
@@ -74,7 +74,7 @@ match a with
                              return t n0 -> Type with
                                |0 => fun _ => @ID
                                |S n0 => fun b0 =>
-                                 forall (a0: t n0), P _ (FS a0) b0
+                                 forall (a0: t n0), P (FS a0) b0
                              end b' with
                          |F1 m' => fun aa => H2 m' aa
                          |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b')
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 0fb6e7acb..807748edd 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -36,21 +36,21 @@ Section SCHEMES.
 Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (bas: forall a: A, P (a :: []))
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
- fix rectS_fix {n} (v: t A (S n)) : P n v :=
+ fix rectS_fix {n} (v: t A (S n)) : P v :=
  match v with
  |nil => @id
  |cons a 0 v =>
      match v as vnn in t _ nn
        return
          match nn as nnn return t A nnn -> Type with
-         |0 => fun vm => P 0 (a :: vm)
+         |0 => fun vm => P (a :: vm)
          |S _ => fun _ => ID
          end vnn
      with
      |nil => bas a
      |_ :: _ => @id
      end
- |cons a (S nn') v => rect a _ v (rectS_fix v)
+ |cons a (S nn') v => rect a v (rectS_fix v)
  end.
 
 (** An induction scheme for 2 vectors of same length *)
@@ -104,7 +104,7 @@ Definition hd {A} {n} (v:t A (S n)) := Eval cbv delta beta in
 
 (** The last element of an non empty vector *)
 Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in
-(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) _ v).
+(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) v).
 
 (** Build a vector of n{^ th} [a] *)
 Fixpoint const {A} (a:A) (n:nat) :=
@@ -147,7 +147,7 @@ Definition tl {A} {n} (v:t A (S n)) := Eval cbv delta beta in
 (** Remove last element of a non-empty vector *)
 Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n :=
 Eval cbv delta beta in (rectS (fun n _ => t A n) (fun a => [])
-  (fun h _ _ H => h :: H) _ v).
+  (fun h _ _ H => h :: H) v).
 
 (** Add an element at the end of a vector *)
 Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) :=
@@ -159,7 +159,7 @@ end.
 (** Copy last element of a vector *)
 Definition shiftrepeat {A} {n} (v:t A (S n)) : t A (S (S n)) :=
 Eval cbv delta beta in (rectS (fun n _ => t A (S (S n)))
-  (fun h =>  h :: h :: []) (fun h _ _ H => h :: H) _ v).
+  (fun h =>  h :: h :: []) (fun h _ _ H => h :: H) v).
 
 (** Remove [p] last elements of a vector *)
 Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
@@ -229,13 +229,13 @@ Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
 Definition map2 {A B C}{n} (g:A -> B -> C) (v1:t A n) (v2:t B n)
   : t C n :=
 Eval cbv delta beta in rect2 (fun n _ _ => t C n) (nil C)
-  (fun _ _ _ H a b => (g a b) :: H) _ v1 v2.
+  (fun _ _ _ H a b => (g a b) :: H) v1 v2.
 
 (** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *)
 Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B :=
-  fix fold_left_fix (b:B) n (v : t A n) : B := match v with
+  fix fold_left_fix (b:B) {n} (v : t A n) : B := match v with
     | [] => b
-    | a :: w => (fold_left_fix (f b a) _ w)
+    | a :: w => (fold_left_fix (f b a) w)
   end.
 
 (** fold_right f [x1 .. xn] b = f x1 (f x2 .. (f xn b) .. ) *)
@@ -251,7 +251,7 @@ Definition fold_right {A B : Type} (f : A->B->B) :=
 Definition fold_right2 {A B C} (g:A -> B -> C -> C) {n} (v:t A n)
   (w : t B n) (c:C) : C :=
 Eval cbv delta beta in rect2 (fun _ _ _ => C) c
-  (fun _ _ _ H a b => g a b H) _ v w.
+  (fun _ _ _ H a b => g a b H) v w.
 
 (** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *)
 Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) :=
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9b6c74398..3084da768 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -136,8 +136,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
-    let (env', ctx), imps = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in
+    let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
+    let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
@@ -276,7 +276,7 @@ let named_of_rel_context l =
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref Evd.empty in
-  let (env', fullctx), impls = interp_context_evars evars env l in
+  let _, ((env', fullctx), impls) = interp_context_evars evars env l in
   let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
   List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c180785d5..ae173f6c3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -67,11 +67,11 @@ let red_constant_entry n ce = function
 let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
-  let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
+  let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
   let imps,ce =
     match ctypopt with
       None ->
-	let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in
+	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	check_evars env Evd.empty !evdref body;
 	imps1@imps2,
@@ -79,8 +79,8 @@ let interp_definition bl red_option c ctypopt =
 	  const_entry_type = None;
           const_entry_opaque = false }
     | Some ctyp ->
-	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in
-	let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in
+	let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
+	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
 	check_evars env Evd.empty !evdref body;
@@ -221,7 +221,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref Evd.empty in
-  let (env_params, ctx_params), userimpls =
+  let _, ((env_params, ctx_params), userimpls) =
     interp_context_evars evdref env0 paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
@@ -451,8 +451,8 @@ type structured_fixpoint_expr = {
 
 let interp_fix_context evdref env isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
-  let (env', ctx), imps = interp_context_evars evdref env before in
-  let (env'', ctx'), imps' = interp_context_evars evdref env' after in
+  let impl_env, ((env', ctx), imps) = interp_context_evars evdref env before in
+  let _, ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), imps @ imps', annot)
       
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index c0ce16cea..2d904c554 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -313,8 +313,8 @@ let start_proof_com kind thms hook =
   let evdref = ref (create_evar_defs Evd.empty) in
   let env0 = Global.env () in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
-    let (env, ctx), imps = interp_context_evars evdref env0 bl in
-    let t', imps' = interp_type_evars_impls ~evdref env t in
+    let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
+    let t', imps' = interp_type_evars_impls ~impls ~evdref env t in
     Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
     let ids = List.map pi1 ctx in
       (compute_proof_name (fst kind) sopt,
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 74a33f6f9..0255e6504 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -33,7 +33,7 @@ let interp_evars evdref env impls k typ =
   let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
 
-let interp_fields_evars evars env nots l =
+let interp_fields_evars evars env impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
       let impl, t' = interp_evars evars env impls Pretyping.IsType t in
@@ -46,7 +46,7 @@ let interp_fields_evars evars env nots l =
       let d = (i,b',t') in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
-    (env, [], [], empty_internalization_env) nots l
+    (env, [], [], impls_env) nots l
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -69,11 +69,11 @@ let typecheck_params_and_fields id t ps nots fs =
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
   in 
-  let (env1,newps), imps = interp_context_evars evars env0 ps in
+  let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
   let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,impls,newfs,data =
-    interp_fields_evars evars env_ar nots (binders_of_decls fs)
+    interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
   in
   let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
   let evars = Typeclasses.resolve_typeclasses env_ar evars in