diff options
| author | Pierre-Marie Pédrot | 2019-04-11 12:07:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-11 12:07:00 +0200 |
| commit | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (patch) | |
| tree | 73c615fe6e2853d5879eebbd034d18bdf8fd686b /plugins/funind | |
| parent | 36c15766a9295d980d142da0e42aebf1309f4eb4 (diff) | |
| parent | 9fe0932a7b04eecea35f98bc2b38beebb64d476a (diff) | |
Merge PR #9909: Remove all but one call to `Global` in the pretyper
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 275b58f0aa..45a4e61846 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl = Impargs.implicits_of_global constructref in let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) construct in @@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl = let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) in - cases_pattern_of_glob_constr Anonymous pat_as_term + cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term ) ind.Declarations.mind_consnames @@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function mkGVar id | PatCstr(constr,patternl,_) -> let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) constr in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 13ff19a46b..7b758da8e8 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function mkGVar id | PatCstr(constr,patternl,_) -> let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) constr in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a5c19f3217..e582362e25 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let _ = List.map_i (fun i x -> - let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in - let env = Global.env () in + let env = Global.env () in + let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in |