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.

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
     )