Parameterizing default inhabitant for impossible cases with an environment.

6 files changed, 20 insertions, 20 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9fa8442f8a..54e847988b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -994,8 +994,8 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
   let k = length_of_tomatch_type_sign na t in
   (p+k,liftn_predicate (k-1) (p+1) ccl tms)
 
-let use_unit_judge evd =
-  let j, ctx = coq_unit_judge () in
+let use_unit_judge env evd =
+  let j, ctx = coq_unit_judge !!env in
   let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in
     evd', j
 
@@ -1024,7 +1024,7 @@ let adjust_impossible_cases sigma pb pred tomatch submat =
     | Evar (evk,_) when snd (evar_source evk sigma) == Evar_kinds.ImpossibleCase ->
         let sigma =
           if not (Evd.is_defined sigma evk) then
-            let sigma, default = use_unit_judge sigma in
+            let sigma, default = use_unit_judge pb.env sigma in
             let sigma = Evd.define evk default.uj_type sigma in
             sigma
           else sigma
@@ -2512,7 +2512,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env sigma = function
     | Some t ->	typing_function tycon env sigma t
-    | None -> use_unit_judge sigma in
+    | None -> use_unit_judge env sigma in
 
   (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env eqns in
@@ -2593,7 +2593,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
     
   let typing_function tycon env sigma = function
     | Some t -> typing_function tycon env sigma t
-    | None -> use_unit_judge sigma in
+    | None -> use_unit_judge env sigma in
 
   let pb =
     { env      = env;
@@ -2668,7 +2668,7 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
     (* A typing function that provides with a canonical term for absurd cases*)
     let typing_fun tycon env sigma = function
     | Some t -> typing_fun tycon env sigma t
-    | None -> use_unit_judge sigma in
+    | None -> use_unit_judge env sigma in
 
     let pb =
       { env       = env;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0dc5a9bad5..592057ab41 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -647,6 +647,7 @@ and detype_r d flags avoid env sigma t =
         else
 	  GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
     | Var id ->
+        (* Discriminate between section variable and non-section variable *)
 	(try let _ = Global.lookup_named id in GRef (VarRef id, None)
 	 with Not_found -> GVar id)
     | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 72d95f7eb1..f0ff1aa93b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -46,14 +46,14 @@ let _ = Goptions.declare_bool_option {
 (*******************************************)
 (* Functions to deal with impossible cases *)
 (*******************************************)
-let impossible_default_case () =
+let impossible_default_case env =
   let type_of_id =
     let open Names.GlobRef in
     match Coqlib.lib_ref "core.IDProp.type" with
     | ConstRef c -> c
     | VarRef _ | IndRef _ | ConstructRef _ -> assert false
   in
-  let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Coqlib.(lib_ref "core.IDProp.idProp")) in
+  let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in
   let (_, u) = Constr.destConst c in
   Some (c, Constr.mkConstU (type_of_id, u), ctx)
 
@@ -62,8 +62,8 @@ let coq_unit_judge =
   let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
   let na1 = Name (Id.of_string "A") in
   let na2 = Name (Id.of_string "H") in
-  fun () ->
-    match impossible_default_case () with
+  fun env ->
+    match impossible_default_case env with
     | Some (id, type_of_id, ctx) ->
       make_judge id type_of_id, ctx
     | None ->
@@ -1352,7 +1352,7 @@ let solve_unconstrained_impossible_cases env evd =
   Evd.fold_undefined (fun evk ev_info evd' ->
     match ev_info.evar_source with
     | loc,Evar_kinds.ImpossibleCase ->
-      let j, ctx = coq_unit_judge () in
+      let j, ctx = coq_unit_judge env in
       let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
       let ty = j_type j in
       let conv_algo = evar_conv_x full_transparent_state in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 20a4f34ec7..350dece28a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -80,4 +80,4 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
 (**/**)
 
 (** {6 Functions to deal with impossible cases } *)
-val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : env -> EConstr.unsafe_judgment Univ.in_universe_context_set
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3719f9302a..f8dc5ba4d6 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -230,8 +230,7 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections warn (con,ind) =
-  let env = Global.env () in
+let compute_canonical_projections env warn (con,ind) =
   let ctx = Environ.constant_context env con in
   let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
@@ -282,7 +281,10 @@ let warn_redundant_canonical_projection =
           ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
 
 let add_canonical_structure warn o =
-    let lo = compute_canonical_projections warn o in
+    (* XXX: Undesired global access to env *)
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let lo = compute_canonical_projections env warn o in
     List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
       let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
       let ocs = try Some (assoc_pat cs_pat l)
@@ -290,9 +292,6 @@ let add_canonical_structure warn o =
       in match ocs with
         | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
-              (* XXX: Undesired global access to env *)
-              let env = Global.env () in
-              let sigma = Evd.from_env env in
               let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF))
               and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF))
               in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4665486fc0..e3b942b610 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1417,7 +1417,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
 	      
   and mimick_undefined_evar evd flags hdc nargs sp =
     let ev = Evd.find_undefined evd sp in
-    let sp_env = Global.env_of_context (evar_filtered_hyps ev) in
+    let sp_env = reset_with_named_context (evar_filtered_hyps ev) env in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' CUMUL flags
@@ -1633,7 +1633,7 @@ let make_eq_test env evd c =
 let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
-    let x = id_of_name_using_hdchar (Global.env()) sigma t name in
+    let x = id_of_name_using_hdchar env sigma t name in
     let ids = Environ.ids_of_named_context_val (named_context_val env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context_val x (named_context_val env) then