diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/extraction.ml | 1 | ||||
-rw-r--r-- | plugins/firstorder/formula.mli | 3 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 3 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 19 |
6 files changed, 13 insertions, 18 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dc2420c4..923743ece 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Declareops open Environ diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 6c7b09383..d306112ce 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Globnames val qflag : bool ref @@ -27,7 +26,7 @@ type counter = bool -> metavariable val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array val ind_hyps : int -> pinductive -> constr list -> - Proof_type.goal Tacmach.sigma -> rel_context array + Proof_type.goal Tacmach.sigma -> Context.Rel.t array type atoms = {positive:constr list;negative:constr list} 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 |