Merge PR #10461: Simplify Declare.declare_variable

Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot

6 files changed, 41 insertions, 54 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index be8f99028c..68ade75815 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -375,20 +375,17 @@ let check_hidden_implicit_parameters ?loc id impls =
 let pure_push_name_env (id,implargs) env =
   {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
-let push_name_env ?(global_level=false) ntnvars implargs env =
+let push_name_env ntnvars implargs env =
   let open CAst in
   function
   | { loc; v = Anonymous } ->
-      if global_level then
-	user_err ?loc (str "Anonymous variables not allowed");
       env
   | { loc; v = Name id } ->
       check_hidden_implicit_parameters ?loc id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
       set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
-      if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var"
-      else Dumpglob.dump_binding ?loc id;
+      Dumpglob.dump_binding ?loc id;
       pure_push_name_env (id,implargs) env
 
 let remember_binders_impargs env bl =
@@ -400,7 +397,7 @@ let remember_binders_impargs env bl =
 let restore_binders_impargs env l =
   List.fold_right pure_push_name_env l env
 
-let intern_generalized_binder ?(global_level=false) intern_type ntnvars
+let intern_generalized_binder intern_type ntnvars
     env {loc;v=na} b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
@@ -410,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left
-    (fun env {loc;v=x} -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
+    (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
     env fvs in
   let bl = List.map
     CAst.(map (fun id ->
@@ -419,9 +416,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
   in
   let na = match na with
     | Anonymous ->
-	if global_level then na
-	else
-	  let name =
+          let name =
 	    let id =
 	      match ty with
               | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
@@ -430,7 +425,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-  in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
+  in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
 
 let intern_assumption intern ntnvars env nal bk ty =
   let intern_type env = intern (set_type_scope env) in
@@ -481,7 +476,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
   let na = make ?loc @@ Name id in
   env,((disjpat,il),id),na
 
-let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function
+let intern_local_binder_aux intern ntnvars (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern ntnvars env nal bk ty in
       let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
@@ -954,16 +949,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
     (* Is [id] a goal or section variable *)
     let _ = Environ.lookup_named_ctxt id namedctx in
       try
-	(* [id] a section variable *)
-	(* Redundant: could be done in intern_qualid *)
-	let ref = VarRef id in
-	let impls = implicits_of_global ref in
-	let scopes = find_arguments_scope ref in
-	Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	DAst.make ?loc @@ GRef (ref, us), impls, scopes, []
+        (* [id] a section variable *)
+        (* Redundant: could be done in intern_qualid *)
+        let ref = VarRef id in
+        let impls = implicits_of_global ref in
+        let scopes = find_arguments_scope ref in
+        Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *)
+        (* Someday we should stop relying on Dumglob raising exceptions *)
+        DAst.make ?loc @@ GRef (ref, us), impls, scopes, []
       with e when CErrors.noncritical e ->
-	(* [id] a goal variable *)
-	gvar (loc,id) us, [], [], []
+        (* [id] a goal variable *)
+        gvar (loc,id) us, [], [], []
 
 let find_appl_head_data c =
   match DAst.get c with
@@ -2424,12 +2420,12 @@ let interp_binder_evars env sigma na t =
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
-let intern_context global_level env impl_env binders =
+let intern_context env impl_env binders =
   try
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let lenv, bl = List.fold_left
 	    (fun (lenv, bl) b ->
-	       let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
+               let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
 	       (env, bl))
 	    ({ids = extract_ids env; unb = false;
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
@@ -2465,7 +2461,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
       (env,sigma,[],k+1,[]) (List.rev bl)
   in sigma, ((env, par), List.rev impls)
 
-let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
-  let int_env,bl = intern_context global_level env impl_env params in
+let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
+  let int_env,bl = intern_context env impl_env params in
   let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in
   sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6c1f4898d9..2e7b832e55 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -90,7 +90,7 @@ val intern_gen : typing_constraint -> env -> evar_map ->
 val intern_pattern : env -> cases_pattern_expr ->
   lident list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
+val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
+  ?program_mode:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
 
diff --git a/interp/decls.ml b/interp/decls.ml
index b802dbe9c3..d9d33b5e0b 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -59,27 +59,22 @@ type logical_kind =
 
 (** Data associated to section variables and local definitions *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 let vartab =
-  Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
+  Summary.ref (Id.Map.empty : (variable_data*DirPath.t) Id.Map.t) ~name:"VARIABLE"
 
-let add_variable_data id o = vartab := Id.Map.add id o !vartab
+let secpath () = drop_dirpath_prefix (Lib.library_dp()) (Lib.cwd())
+let add_variable_data id o = vartab := Id.Map.add id (o,secpath()) !vartab
 
-let variable_path id = let {path} = Id.Map.find id !vartab in path
-let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque
-let variable_kind id = let {kind} = Id.Map.find id !vartab in kind
-let variable_context id = let {univs} = Id.Map.find id !vartab in univs
-let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly
+let variable_opacity id = let {opaque},_ = Id.Map.find id !vartab in opaque
+let variable_kind id = let {kind},_ = Id.Map.find id !vartab in kind
 
 let variable_secpath id =
-  let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
+  let _, dir = Id.Map.find id !vartab in
   make_qualid dir id
 
 let variable_exists id = Id.Map.mem id !vartab
diff --git a/interp/decls.mli b/interp/decls.mli
index 05e4be0de6..56866aeb43 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -60,19 +60,13 @@ type logical_kind =
 
 (** Registration and access to the table of variable *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 val add_variable_data : variable -> variable_data -> unit
 
-(* Not used *)
-val variable_path : variable -> DirPath.t
-
 (* Only used in dumpglob *)
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
@@ -81,6 +75,4 @@ val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 
 (* Used in declare, very dubious *)
-val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 482303d935..dc6a1ae180 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -166,6 +166,9 @@ let dump_reference ?loc modpath ident ty =
   let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
   dump_ref ?loc filepath modpath ident ty
 
+let dump_secvar ?loc id =
+  dump_reference ?loc "<>" (Libnames.string_of_qualid (Decls.variable_secpath id)) "var"
+
 let dump_modref ?loc mp ty =
   let (dp, l) = Lib.split_modpath mp in
   let filepath = Names.DirPath.to_string dp in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index e0308b8afc..60d62a1cb2 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -32,6 +32,7 @@ val dump_definition : Names.lident -> bool -> string -> unit
 val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_modref  : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_reference  : ?loc:Loc.t -> string -> string -> string -> unit
+val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit
 val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit