merging conflicts with the original "trunk__CLEANUP__Context__2" branch

1 files changed, 32 insertions, 28 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 86302dc6ce..c8f8a19e5b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -15,6 +15,7 @@ open Tactics
 open Indfun_common
 open Libnames
 open Globnames
+open Context.Rel.Declaration
 
 (* let msgnl = Pp.msgnl *)
 
@@ -304,11 +305,11 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     in
     let new_type_of_hyp,ctxt_size,witness_fun =
       List.fold_left_i
-	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
+	(fun i (end_of_type,ctxt_size,witness_fun) decl ->
 	   try
 	     let witness = Int.Map.find i sub in
-	     if not (Option.is_empty b') then anomaly (Pp.str "can not redefine a rel!");
-	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
+	     (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -536,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		(scan_type new_context new_t')
 	    with Failure "NoChange" ->
 	      (* Last thing todo : push the rel in the context and continue *)
-	      scan_type ((x,None,t_x)::context) t'
+	      scan_type (LocalAssum (x,t_x) :: context) t'
 	  end
       end
     else
@@ -736,7 +737,8 @@ let build_proof
 		      tclTHEN
 			(Proofview.V82.of_tactic intro)
 			(fun g' ->
-			   let (id,_,_) = pf_last_hyp g' in
+                           let open Context.Named.Declaration in
+			   let id = pf_last_hyp g' |> get_id in
 			   let new_term =
 			     pf_nf_betaiota g'
 			       (mkApp(dyn_infos.info,[|mkVar id|]))
@@ -921,7 +923,9 @@ let generalize_non_dep hyp g =
   let env = Global.env () in
   let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
   let to_revert,_ =
-    Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+    let open Context.Named.Declaration in
+    Environ.fold_named_context_reverse (fun (clear,keep) decl ->
+      let hyp = get_id decl in
       if Id.List.mem hyp hyps
         || List.exists (Termops.occur_var_in_decl env hyp) keep
 	|| Termops.occur_var env hyp hyp_typ
@@ -936,7 +940,7 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl (na,_,_) =  (Nameops.out_name na)
+let id_of_decl decl = Nameops.out_name (get_name decl)
 let var_of_decl decl = mkVar (id_of_decl decl)
 let revert idl =
   tclTHEN
@@ -1044,7 +1048,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       (
 	fun g' ->
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
-	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
+          let open Context.Named.Declaration in
+	  let just_introduced_id = List.map get_id just_introduced in
 	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
 		  (revert just_introduced_id) g'
       )
@@ -1069,11 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	 (Name new_id)
       )
     in
-    let fresh_decl =
-      (fun (na,b,t) ->
-	 (fresh_id na,b,t)
-      )
-    in
+    let fresh_decl = map_name fresh_id in
     let princ_info : elim_scheme =
       { princ_info with
 	  params = List.map fresh_decl princ_info.params;
@@ -1120,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1165,7 +1166,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    in
 	    let pte_to_fix,rev_info =
 	      List.fold_left_i
-		(fun i (acc_map,acc_info) (pte,_,_) ->
+		(fun i (acc_map,acc_info) decl ->
+		   let pte = get_name decl in
 		   let infos = info_array.(i) in
 		   let type_args,_ = decompose_prod infos.types in
 		   let nargs = List.length type_args in
@@ -1259,7 +1261,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		 let args = nLastDecls nb_args g in
 		 let fix_body = fix_info.body_with_param in
 (* 		 observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
-		 let args_id = List.map (fun (id,_,_) -> id) args in
+                 let open Context.Named.Declaration in
+		 let args_id = List.map get_id args in
 		 let dyn_infos =
 		   {
 		     nb_rec_hyps = -100;
@@ -1276,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
+			  (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1317,8 +1320,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    [
 	      tclDO nb_args (Proofview.V82.of_tactic intro);
 	      (fun g -> (* replacement of the function by its body *)
-		 let args = nLastDecls nb_args g in
-		 let args_id = List.map (fun (id,_,_) -> id) args in
+	         let args = nLastDecls nb_args g in
+                 let open Context.Named.Declaration in
+		 let args_id = List.map get_id args in
 		 let dyn_infos =
 		   {
 		     nb_rec_hyps = -100;
@@ -1520,7 +1524,7 @@ let prove_principle_for_gen
       avoid := new_id :: !avoid;
       Name new_id
   in
-  let fresh_decl (na,b,t) = (fresh_id na,b,t) in
+  let fresh_decl = map_name fresh_id in
   let princ_info : elim_scheme =
     { princ_info with
 	params = List.map fresh_decl princ_info.params;
@@ -1550,11 +1554,11 @@ let prove_principle_for_gen
   in
   let rec_arg_id =
     match List.rev post_rec_arg with
-      | (Name id,_,_)::_ -> id
+      | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
   let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
@@ -1582,7 +1586,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+  let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | None -> error "No tcc proof !!"
@@ -1629,7 +1633,7 @@ let prove_principle_for_gen
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
+	(List.rev_map (fun decl -> Nameops.out_name (get_name decl))
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1667,7 +1671,7 @@ let prove_principle_for_gen
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
 	 let predicates_names =
-	   List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
+	   List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
@@ -1683,7 +1687,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (fun (na,_,_) -> (Nameops.out_name na))
+			   (fun decl -> (Nameops.out_name (get_name decl)))
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1712,7 +1716,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
+	      (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'