Functionalizing calls to the environment in Himsg.

This shall eventually allow to call Himsg at any point of the
execution, independently of the exact current global environment.

4 files changed, 25 insertions, 25 deletions

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
     )