[econstr] Continue consolidation of EConstr API under `interp`.

This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.

The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.

We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.

In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.

Also, the new return type of `Pretyping.understand` should undergo
careful review.

We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.

Some TODOs are:

- impargs was calling whd_all, the Econstr equivalent can be either
  + Reductionops.whd_all [which does refolding and no sharing]
  + Reductionops.clos_whd_flags with all as a flag.

1 files changed, 32 insertions, 27 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index ea7ef21b19..bf39c726a8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -668,8 +668,8 @@ type scope_class = cl_typ
 let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
-let compute_scope_class t =
-  let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in
+let compute_scope_class sigma t =
+  let (cl,_,_) = find_class_type sigma t in
   cl
 
 module ScopeClassOrd =
@@ -698,22 +698,22 @@ let find_scope_class_opt = function
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
 
-let rec compute_arguments_classes t =
-  match Constr.kind (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
+let rec compute_arguments_classes sigma t =
+  match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with
     | Prod (_,t,u) ->
-	let cl = try Some (compute_scope_class t) with Not_found -> None in
-	cl :: compute_arguments_classes u
+        let cl = try Some (compute_scope_class sigma t) with Not_found -> None in
+        cl :: compute_arguments_classes sigma u
     | _ -> []
 
-let compute_arguments_scope_full t =
-  let cls = compute_arguments_classes t in
+let compute_arguments_scope_full sigma t =
+  let cls = compute_arguments_classes sigma t in
   let scs = List.map find_scope_class_opt cls in
   scs, cls
 
-let compute_arguments_scope t = fst (compute_arguments_scope_full t)
+let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
 
-let compute_type_scope t =
-  find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
+let compute_type_scope sigma t =
+  find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
 
 let current_type_scope_name () =
    find_scope_class_opt (Some CL_SORT)
@@ -779,20 +779,24 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
 let classify_arguments_scope (req,_,_,_,_ as obj) =
   if req == ArgsScopeNoDischarge then Dispose else Substitute obj
 
-let rebuild_arguments_scope (req,r,n,l,_) =
+let rebuild_arguments_scope sigma (req,r,n,l,_) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
-        let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in
-	(req,r,List.length scs,scs,cls)
+      let env = Global.env () in (*FIXME?*)
+      let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+      let scs,cls = compute_arguments_scope_full sigma typ in
+      (req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
-	(* Add to the manually given scopes the one found automatically
-           for the extra parameters of the section. Discard the classes
-           of the manually given scopes to avoid further re-computations. *)
-        let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in
-	let l1 = List.firstn n l' in
-        let cls1 = List.firstn n cls in
-	(req,r,0,l1@l,cls1)
+      (* Add to the manually given scopes the one found automatically
+         for the extra parameters of the section. Discard the classes
+         of the manually given scopes to avoid further re-computations. *)
+      let env = Global.env () in (*FIXME?*)
+      let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+      let l',cls = compute_arguments_scope_full sigma typ in
+      let l1 = List.firstn n l' in
+      let cls1 = List.firstn n cls in
+      (req,r,0,l1@l,cls1)
 
 type arguments_scope_obj =
     arguments_scope_discharge_request * global_reference *
@@ -807,7 +811,8 @@ let inArgumentsScope : arguments_scope_obj -> obj =
       subst_function = subst_arguments_scope;
       classify_function = classify_arguments_scope;
       discharge_function = discharge_arguments_scope;
-      rebuild_function = rebuild_arguments_scope }
+      (* XXX: Should we pass the sigma here or not, see @herbelin's comment in 6511 *)
+      rebuild_function = rebuild_arguments_scope Evd.empty }
 
 let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
 
@@ -819,7 +824,7 @@ let declare_arguments_scope local r scl =
   (* We empty the list of argument classes to disable further scope
      re-computations and keep these manually given scopes. *)
   declare_arguments_scope_gen req r 0 (scl,[])
-                              
+
 let find_arguments_scope r =
   try
     let (scl,cls,stamp) = Refmap.find r !arguments_scope in
@@ -832,12 +837,12 @@ let find_arguments_scope r =
       scl'
   with Not_found -> []
 
-let declare_ref_arguments_scope ref =
-  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
-  let (scs,cls as o) = compute_arguments_scope_full t in
+let declare_ref_arguments_scope sigma ref =
+  let env = Global.env () in (* FIXME? *)
+  let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in
+  let (scs,cls as o) = compute_arguments_scope_full sigma typ in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
-
 (********************************)
 (* Encoding notations as string *)