merge

4 files changed, 12 insertions, 15 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1474f1e93..4eab5f912 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -3,7 +3,6 @@ open Errors
 open Util
 open Term
 open Vars
-open Context
 open Namegen
 open Names
 open Declarations
@@ -230,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 
 
 
-let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
+let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
   let nochange ?t' msg  =
     begin
       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index bbe2f1a3a..e2c3bbb97 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -3,7 +3,6 @@ open Errors
 open Util
 open Term
 open Vars
-open Context
 open Namegen
 open Names
 open Pp
@@ -30,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env = Global.env () in
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context)  : rel_context =
+  let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t)  : Context.Rel.t =
     match predicates with
     | [] -> []
     |(Name x,v,t)::predicates ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5d92fca5e..80de8e764 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
   let new_env = add_pat_variables  env pat typ in
   let res =
     fst (
-      Context.fold_rel_context
+      Context.Rel.fold_outside
 	(fun (na,v,t) (env,ctxt) ->
 	 match na with
 	   | Anonymous -> assert false
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index e3455e770..be04728e0 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Context
 open Termops
 open Declarations
 open Glob_term
@@ -258,27 +257,27 @@ type merge_infos =
       lnk2: int merged_arg array;
 
       (** rec params which remain rec param (ie not linked) *)
-      recprms1: rel_declaration list;
-      recprms2: rel_declaration list;
+      recprms1: Context.Rel.Declaration.t list;
+      recprms2: Context.Rel.Declaration.t list;
       nrecprms1: int;
       nrecprms2: int;
 
       (** rec parms which became non parm (either linked to something
          or because after a rec parm that became non parm) *)
-      otherprms1: rel_declaration list;
-      otherprms2: rel_declaration list;
+      otherprms1: Context.Rel.Declaration.t list;
+      otherprms2: Context.Rel.Declaration.t list;
       notherprms1:int;
       notherprms2:int;
 
       (** args which remain args in merge *)
-      args1:rel_declaration list;
-      args2:rel_declaration list;
+      args1:Context.Rel.Declaration.t list;
+      args2:Context.Rel.Declaration.t list;
       nargs1:int;
       nargs2:int;
 
       (** functional result args *)
-      funresprms1: rel_declaration list;
-      funresprms2: rel_declaration list;
+      funresprms1: Context.Rel.Declaration.t list;
+      funresprms2: Context.Rel.Declaration.t list;
       nfunresprms1:int;
       nfunresprms2:int;
     }
@@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
   lident , bindlist , Some cstr_expr , lcstor_expr
 
 
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
+let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
         let traw = Detyping.detype false [] (Global.env()) Evd.empty t in