aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/indrec.ml16
-rw-r--r--pretyping/indrec.mli2
-rw-r--r--tactics/inv.ml2
-rw-r--r--vernac/explainErr.ml4
-rw-r--r--vernac/himsg.ml28
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/indschemes.ml16
7 files changed, 35 insertions, 35 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index dc900ab814..418fdf2a26 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -40,7 +40,7 @@ type recursion_scheme_error =
| NotMutualInScheme of inductive * inductive
| NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
-exception RecursionSchemeError of recursion_scheme_error
+exception RecursionSchemeError of env * recursion_scheme_error
let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
let name_assumption env = function
@@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
if not (Sorts.List.mem kind (elim_sorts specif)) then
raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind)))
+ (env, NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind)))
in
let ndepar = mip.mind_nrealdecls + 1 in
@@ -490,7 +490,7 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
let build_case_analysis_scheme env sigma pity dep kind =
let (mib,mip) = lookup_mind_specif env (fst pity) in
if dep && not (Inductiveops.has_dependent_elim mib) then
- raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
+ raise (RecursionSchemeError (env, NotAllowedDependentAnalysis (false, fst pity)));
mis_make_case_com dep env sigma pity (mib,mip) kind
let is_in_prop mip =
@@ -550,9 +550,9 @@ let check_arities env listdepkind =
let kelim = elim_sorts (mibi,mipi) in
if not (Sorts.List.mem kind kelim) then raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u))))
+ (env, NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u))))
else if Int.List.mem ni ln then raise
- (RecursionSchemeError (NotMutualInScheme (mind,mind)))
+ (RecursionSchemeError (env, NotMutualInScheme (mind,mind)))
else ni::ln)
[] listdepkind
in true
@@ -561,7 +561,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
| ((mind,u),dep,s)::lrecspec ->
let (mib,mip) = lookup_mind_specif env mind in
if dep && not (Inductiveops.has_dependent_elim mib) then
- raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
+ raise (RecursionSchemeError (env, NotAllowedDependentAnalysis (true, mind)));
let (sp,tyi) = mind in
let listdepkind =
((mind,u),mib,mip,dep,s)::
@@ -572,7 +572,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
let (mibi',mipi') = lookup_mind_specif env mind' in
((mind',u'),mibi',mipi',dep',s')
else
- raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
+ raise (RecursionSchemeError (env, NotMutualInScheme (mind,mind'))))
lrecspec)
in
let _ = check_arities env listdepkind in
@@ -582,7 +582,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
let build_induction_scheme env sigma pind dep kind =
let (mib,mip) = lookup_mind_specif env (fst pind) in
if dep && not (Inductiveops.has_dependent_elim mib) then
- raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
+ raise (RecursionSchemeError (env, NotAllowedDependentAnalysis (true, fst pind)));
let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
sigma, List.hd l
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index de9d3a0abf..91a5651f7f 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -20,7 +20,7 @@ type recursion_scheme_error =
| NotMutualInScheme of inductive * inductive
| NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
-exception RecursionSchemeError of recursion_scheme_error
+exception RecursionSchemeError of env * recursion_scheme_error
(** Eliminations *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 43786c8e19..f718b13a63 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names =
(* Error messages of the inversion tactics *)
let wrap_inv_error id = function (e, info) -> match e with
| Indrec.RecursionSchemeError
- (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) ->
+ (_, Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) ->
Proofview.tclENV >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG (
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 7cf4e64805..b37fce645a 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -76,8 +76,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_module_error e)
| Modintern.ModuleInternalizationError e ->
wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
- | RecursionSchemeError e ->
- wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
+ | RecursionSchemeError (env,e) ->
+ wrap_vernac_error exn (Himsg.explain_recursion_scheme_error env e)
| Cases.PatternMatchingError (env,sigma,e) ->
wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
| Tacred.ReductionTacticError e ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 71155d7921..a4b3a75c9f 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -601,12 +601,12 @@ let explain_var_not_found env id =
spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."
let explain_wrong_case_info env (ind,u) ci =
- let pi = pr_inductive (Global.env()) ind in
+ let pi = pr_inductive env ind in
if eq_ind ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
spc () ++ pi ++ spc () ++ str "has invalid information."
else
- let pc = pr_inductive (Global.env()) ci.ci_ind in
+ let pc = pr_inductive env ci.ci_ind in
str "A term of inductive type" ++ spc () ++ pi ++ spc () ++
str "was given to a pattern-matching expression on the inductive type" ++
spc () ++ pc ++ str "."
@@ -1156,24 +1156,24 @@ let error_large_non_prop_inductive_not_in_type () =
(* Recursion schemes errors *)
-let error_not_allowed_case_analysis isrec kind i =
+let error_not_allowed_case_analysis env isrec kind i =
str (if isrec then "Induction" else "Case analysis") ++
strbrk " on sort " ++ pr_sort Evd.empty kind ++
strbrk " is not allowed for inductive definition " ++
- pr_inductive (Global.env()) (fst i) ++ str "."
+ pr_inductive env (fst i) ++ str "."
-let error_not_allowed_dependent_analysis isrec i =
+let error_not_allowed_dependent_analysis env isrec i =
str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++
strbrk " is not allowed for inductive definition " ++
- pr_inductive (Global.env()) i ++ str "."
+ pr_inductive env i ++ str "."
-let error_not_mutual_in_scheme ind ind' =
+let error_not_mutual_in_scheme env ind ind' =
if eq_ind ind ind' then
- str "The inductive type " ++ pr_inductive (Global.env()) ind ++
+ str "The inductive type " ++ pr_inductive env ind ++
str " occurs twice."
else
- str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++
- str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++
+ str "The inductive types " ++ pr_inductive env ind ++ spc () ++
+ str "and" ++ spc () ++ pr_inductive env ind' ++ spc () ++
str "are not mutually defined."
(* Inductive constructions errors *)
@@ -1194,12 +1194,12 @@ let explain_inductive_error = function
(* Recursion schemes errors *)
-let explain_recursion_scheme_error = function
+let explain_recursion_scheme_error env = function
| NotAllowedCaseAnalysis (isrec,k,i) ->
- error_not_allowed_case_analysis isrec k i
- | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind'
+ error_not_allowed_case_analysis env isrec k i
+ | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme env ind ind'
| NotAllowedDependentAnalysis (isrec, i) ->
- error_not_allowed_dependent_analysis isrec i
+ error_not_allowed_dependent_analysis env isrec i
(* Pattern-matching errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 02b3c45501..db05aaa125 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -29,7 +29,7 @@ val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list
val explain_typeclass_error : env -> typeclass_error -> Pp.t
-val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
+val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t
val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 0a74a8cc4a..3ee836a828 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -330,11 +330,10 @@ let declare_sym_scheme ind =
(* Scheme command *)
let smart_global_inductive y = smart_global_inductive y
-let rec split_scheme l =
- let env = Global.env() in
+let rec split_scheme env l =
match l with
| [] -> [],[]
- | (Some id,t)::q -> let l1,l2 = split_scheme q in
+ | (Some id,t)::q -> let l1,l2 = split_scheme env q in
( match t with
| InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
| CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
@@ -345,7 +344,7 @@ let rec split_scheme l =
requested
*)
| (None,t)::q ->
- let l1,l2 = split_scheme q in
+ let l1,l2 = split_scheme env q in
let names inds recs isdep y z =
let ind = smart_global_inductive y in
let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
@@ -408,12 +407,12 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let _ = List.fold_right2 declare listdecl lrecnames [] in
fixpoint_message None lrecnames
-let get_common_underlying_mutual_inductive = function
+let get_common_underlying_mutual_inductive env = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
| (_,ind')::_ ->
- raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
+ raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
| [] ->
if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
then user_err Pp.(str "A type occurs twice");
@@ -422,7 +421,8 @@ let get_common_underlying_mutual_inductive = function
(function (Some id,(_,i)) -> Some (i,id.CAst.v) | (None,_) -> None) all
let do_scheme l =
- let ischeme,escheme = split_scheme l in
+ let env = Global.env() in
+ let ischeme,escheme = split_scheme env l in
(* we want 1 kind of scheme at a time so we check if the user
tried to declare different schemes at once *)
if not (List.is_empty ischeme) && not (List.is_empty escheme)
@@ -431,7 +431,7 @@ tried to declare different schemes at once *)
else (
if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
else
- let mind,l = get_common_underlying_mutual_inductive escheme in
+ let mind,l = get_common_underlying_mutual_inductive env escheme in
declare_beq_scheme_with l mind;
declare_eq_decidability_scheme_with l mind
)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:39:52 +0000