aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml29
-rw-r--r--library/impargs.ml13
-rw-r--r--parsing/printer.ml32
-rw-r--r--parsing/printer.mli3
-rw-r--r--plugins/decl_mode/g_decl_mode.ml42
-rw-r--r--plugins/funind/recdef.ml3
-rw-r--r--plugins/xml/dumptree.ml44
-rw-r--r--pretyping/detyping.ml8
-rw-r--r--pretyping/namegen.ml45
-rw-r--r--pretyping/namegen.mli5
-rw-r--r--proofs/clenv.ml4
-rw-r--r--test-suite/output/names.out5
-rw-r--r--test-suite/output/names.v5
-rw-r--r--test-suite/success/apply.v14
-rw-r--r--toplevel/himsg.ml10
-rw-r--r--toplevel/ide_slave.ml2
16 files changed, 119 insertions, 65 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c08972ac1..9bcae183f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -943,21 +943,30 @@ let extern_glob_type vars c =
let loc = dummy_loc (* for constr and pattern, locations are lost *)
-let extern_constr_gen at_top scopt env t =
- let avoid = if at_top then ids_of_context env else [] in
- let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
+let extern_constr_gen goal_concl_style scopt env t =
+ (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
+ (* i.e.: avoid using the names of goal/section/rel variables and the short *)
+ (* names of global definitions of current module when computing names for *)
+ (* bound variables. *)
+ (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
+ (* those goal/section/rel variables that occurs in the subterm under *)
+ (* consideration; see namegen.ml for further details *)
+ let avoid = if goal_concl_style then ids_of_context env else [] in
+ let rel_env_names = names_of_rel_context env in
+ let r = Detyping.detype goal_concl_style avoid rel_env_names t in
let vars = vars_of_env env in
extern false (scopt,[]) vars r
-let extern_constr_in_scope at_top scope env t =
- extern_constr_gen at_top (Some scope) env t
+let extern_constr_in_scope goal_concl_style scope env t =
+ extern_constr_gen goal_concl_style (Some scope) env t
-let extern_constr at_top env t =
- extern_constr_gen at_top None env t
+let extern_constr goal_concl_style env t =
+ extern_constr_gen goal_concl_style None env t
-let extern_type at_top env t =
- let avoid = if at_top then ids_of_context env else [] in
- let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
+let extern_type goal_concl_style env t =
+ let avoid = if goal_concl_style then ids_of_context env else [] in
+ let rel_env_names = names_of_rel_context env in
+ let r = Detyping.detype goal_concl_style avoid rel_env_names t in
extern_glob_type (vars_of_env env) r
let extern_sort s = extern_glob_sort (detype_sort s)
diff --git a/library/impargs.ml b/library/impargs.ml
index b7dbd05fd..6b01c5fb1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -208,11 +208,10 @@ let rec is_rigid_head t = match kind_of_term t with
(* calcule la liste des arguments implicites *)
-let find_displayed_name_in all avoid na b =
- if all then
- compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
- else
- compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
+let find_displayed_name_in all avoid na (_,b as envnames_b) =
+ let flag = RenamingElsewhereFor envnames_b in
+ if all then compute_and_force_displayed_name_in flag avoid na b
+ else compute_displayed_name_in flag avoid na b
let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
@@ -220,7 +219,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in all avoid na b in
+ let na',avoid' = find_displayed_name_in all avoid na (names,b) in
add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
(aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
| _ ->
@@ -233,7 +232,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
in
match kind_of_term (whd_betadeltaiota env t) with
| Prod (na,a,b) ->
- let na',avoid = find_displayed_name_in all [] na b in
+ let na',avoid = find_displayed_name_in all [] na ([],b) in
let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
!rigid, Array.to_list v
| _ -> true, []
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3d2f3e089..dd17ee0c8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -36,13 +36,19 @@ let delayed_emacs_cmd s =
(**********************************************************************)
(** Terms *)
- (* [at_top] means ids of env must be avoided in bound variables *)
-let pr_constr_core at_top env t =
- pr_constr_expr (extern_constr at_top env t)
-let pr_lconstr_core at_top env t =
- pr_lconstr_expr (extern_constr at_top env t)
+(* [goal_concl_style] means that all names of goal/section variables
+ and all names of rel variables (if any) in the given env and all short
+ names of global definitions of the current module must be avoided while
+ printing bound variables.
+ Otherwise, short names of global definitions are printed qualified
+ and only names of goal/section variables and rel names that do
+ _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env t =
+ pr_constr_expr (extern_constr goal_concl_style env t)
+let pr_lconstr_core goal_concl_style env t =
+ pr_lconstr_expr (extern_constr goal_concl_style env t)
-let pr_lconstr_env_at_top env = pr_lconstr_core true env
let pr_lconstr_env env = pr_lconstr_core false env
let pr_constr_env env = pr_constr_core false env
@@ -69,12 +75,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en
let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
-let pr_type_core at_top env t =
- pr_constr_expr (extern_type at_top env t)
-let pr_ltype_core at_top env t =
- pr_lconstr_expr (extern_type at_top env t)
+let pr_type_core goal_concl_style env t =
+ pr_constr_expr (extern_type goal_concl_style env t)
+let pr_ltype_core goal_concl_style env t =
+ pr_lconstr_expr (extern_type goal_concl_style env t)
-let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_goal_concl_style_env env = pr_ltype_core true env
let pr_ltype_env env = pr_ltype_core false env
let pr_type_env env = pr_type_core false env
@@ -263,7 +269,7 @@ let default_pr_goal gs =
let preamb,thesis,penv,pc =
mt (), mt (),
pr_context_of env,
- pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+ pr_goal_concl_style_env env (Goal.V82.concl sigma g)
in
preamb ++
str" " ++ hv 0 (penv ++ fnl () ++
@@ -280,7 +286,7 @@ let pr_goal_tag g =
let pr_concl n sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
let env = Goal.V82.env sigma g in
- let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in
+ let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in
str (emacs_str "") ++
str "subgoal " ++ int n ++ pr_goal_tag g ++
str " is:" ++ cut () ++ str" " ++ pc
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 2d437c201..bbc3a6cad 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -26,7 +26,6 @@ open Tacexpr
(** Terms *)
val pr_lconstr_env : env -> constr -> std_ppcmds
-val pr_lconstr_env_at_top : env -> constr -> std_ppcmds
val pr_lconstr : constr -> std_ppcmds
val pr_constr_env : env -> constr -> std_ppcmds
@@ -44,7 +43,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds
-val pr_ltype_env_at_top : env -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> types -> std_ppcmds
val pr_ltype_env : env -> types -> std_ppcmds
val pr_ltype : types -> std_ppcmds
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b5a2ac82e..fd98d5457 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -29,7 +29,7 @@ let pr_goal gs =
(str " *** Declarative Mode ***" ++ fnl ()++fnl ()),
(str "thesis := " ++ fnl ()),
Printer.pr_context_of env,
- Printer.pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+ Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g)
in
preamb ++
str" " ++ hv 0 (penv ++ fnl () ++
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0f92378d6..872d3be4a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -128,7 +128,8 @@ let pf_get_new_ids idl g =
[]
let compute_renamed_type gls c =
- rename_bound_vars_as_displayed [] (pf_type_of gls c)
+ rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+ (pf_type_of gls c)
let h'_id = id_of_string "h'"
let heq_id = id_of_string "Heq"
let teq_id = id_of_string "teq"
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 69b9e6ea7..8415bbd10 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -107,7 +107,7 @@ let pr_context_xml env =
let pr_subgoal_metas_xml metas env=
let pr_one (meta, typ) =
- fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++
+ fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++
str "\"/>"
in
List.fold_left (++) (mt ()) (List.map pr_one metas)
@@ -117,7 +117,7 @@ let pr_goal_xml sigma g =
let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
if Decl_mode.try_get_info sigma g = None then
(hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
- xmlstream (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) ++
+ xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++
str "\"/>" ++
(pr_context_xml env)) ++
fnl () ++ str "</goal>")
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dc8957dd4..99d054e56 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -533,7 +533,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
buildrec [] [] avoid env construct_nargs branch
and detype_binder isgoal bk avoid env na ty c =
- let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+ let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
let na',avoid' =
if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
else compute_displayed_name_in flag avoid na c in
@@ -553,9 +553,11 @@ let rec detype_rel_context where avoid env sign =
| None -> na,avoid
| Some c ->
if b<>None then
- compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+ compute_displayed_let_name_in
+ (RenamingElsewhereFor (env,c)) avoid na c
else
- compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+ compute_displayed_name_in
+ (RenamingElsewhereFor (env,c)) avoid na c in
let b = Option.map (detype false avoid env) b in
let t = detype false avoid env t in
(na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 0d086919a..9a1425716 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -233,22 +233,27 @@ let make_all_name_different env =
looks for name of same base with lower available subscript beyond current
subscript *)
-let visibly_occur_id id c =
- let rec occur c = match kind_of_term c with
+let occur_rel p env id =
+ try lookup_name_of_rel p env = Name id
+ with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+ let rec occur n c = match kind_of_term c with
| Const _ | Ind _ | Construct _ | Var _
when shortest_qualid_of_global Idset.empty (global_of_constr c)
= qualid_of_ident id -> raise Occur
- | _ -> iter_constr occur c
+ | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+ | _ -> iter_constr_with_binders succ occur n c
in
- try occur c; false
+ try occur 1 c; false
with Occur -> true
| Not_found -> false (* Happens when a global is not in the env *)
-let next_ident_away_for_default_printing t id avoid =
- let bad id = List.mem id avoid or visibly_occur_id id t in
+let next_ident_away_for_default_printing env_t id avoid =
+ let bad id = List.mem id avoid or visibly_occur_id id env_t in
next_ident_away_from id bad
-let next_name_away_for_default_printing t na avoid =
+let next_name_away_for_default_printing env_t na avoid =
let id = match na with
| Name id -> id
| Anonymous ->
@@ -256,7 +261,7 @@ let next_name_away_for_default_printing t na avoid =
(* taken into account by the function compute_displayed_name_in; *)
(* just in case, invent a valid name *)
id_of_string "H" in
- next_ident_away_for_default_printing t id avoid
+ next_ident_away_for_default_printing env_t id avoid
(**********************************************************************)
(* Displaying terms avoiding bound variables clashes *)
@@ -279,13 +284,13 @@ let next_name_away_for_default_printing t na avoid =
type renaming_flags =
| RenamingForCasesPattern
| RenamingForGoal
- | RenamingElsewhereFor of constr
+ | RenamingElsewhereFor of (name list * constr)
let next_name_for_display flags =
match flags with
| RenamingForCasesPattern -> next_name_away_in_cases_pattern
| RenamingForGoal -> next_name_away_in_goal
- | RenamingElsewhereFor t -> next_name_away_for_default_printing t
+ | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
(* Remark: Anonymous var may be dependent in Evar's contexts *)
let compute_displayed_name_in flags avoid na c =
@@ -307,16 +312,20 @@ let compute_displayed_let_name_in flags avoid na c =
let fresh_id = next_name_for_display flags na avoid in
(Name fresh_id, fresh_id::avoid)
-let rec rename_bound_vars_as_displayed avoid c =
- let rec rename avoid c =
+let rec rename_bound_vars_as_displayed avoid env c =
+ let rec rename avoid env c =
match kind_of_term c with
| Prod (na,c1,c2) ->
- let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
- mkProd (na', c1, rename avoid' c2)
+ let na',avoid' =
+ compute_displayed_name_in
+ (RenamingElsewhereFor (env,c2)) avoid na c2 in
+ mkProd (na', c1, rename avoid' (add_name na' env) c2)
| LetIn (na,c1,t,c2) ->
- let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
- mkLetIn (na',c1,t, rename avoid' c2)
- | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+ let na',avoid' =
+ compute_displayed_let_name_in
+ (RenamingElsewhereFor (env,c2)) avoid na c2 in
+ mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+ | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
| _ -> c
in
- rename avoid c
+ rename avoid env c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 637cbf64d..6ca031463 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -70,7 +70,7 @@ val set_reserved_typed_name : (types -> name) -> unit
type renaming_flags =
| RenamingForCasesPattern (** avoid only global constructors *)
| RenamingForGoal (** avoid all globals (as in intro) *)
- | RenamingElsewhereFor of constr
+ | RenamingElsewhereFor of (name list * constr)
val make_all_name_different : env -> env
@@ -80,4 +80,5 @@ val compute_and_force_displayed_name_in :
renaming_flags -> identifier list -> name -> constr -> name * identifier list
val compute_displayed_let_name_in :
renaming_flags -> identifier list -> name -> constr -> name * identifier list
-val rename_bound_vars_as_displayed : identifier list -> types -> types
+val rename_bound_vars_as_displayed :
+ identifier list -> name list -> types -> types
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 417818abf..c4df5721f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -501,8 +501,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
let clause = mk_clenv_from_env env sigma n (c,t) in
clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
- let clause = mk_clenv_from_env env sigma n
- (c,rename_bound_vars_as_displayed [] t)
+ let clause = mk_clenv_from_env env sigma n
+ (c,rename_bound_vars_as_displayed [] [] t)
in clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
new file mode 100644
index 000000000..90ad4ba09
--- /dev/null
+++ b/test-suite/output/names.out
@@ -0,0 +1,5 @@
+The command has indeed failed with message:
+=> Error: In environment
+ y : nat
+ The term "a y" has type "{y0 : nat | y = y0}"
+ while it is expected to have type "{x : nat | x = y}".
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
new file mode 100644
index 000000000..b3b5071a0
--- /dev/null
+++ b/test-suite/output/names.v
@@ -0,0 +1,5 @@
+(* Test no clash names occur *)
+(* see bug #2723 *)
+
+Parameter a : forall x, {y:nat|x=y}.
+Fail Definition b y : {x:nat|x=y} := a y.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index e3183ef27..8e829e061 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -415,3 +415,17 @@ apply mapfuncomp.
Abort.
End A.
+
+(* Check "with" clauses refer to names as they are printed *)
+
+Definition hide p := forall n:nat, p = n.
+
+Goal forall n, (forall n, n=0) -> hide n -> n=0.
+unfold hide.
+intros n H H'.
+(* H is displayed as (forall n, n=0) *)
+apply H with (n:=n).
+Undo.
+(* H' is displayed as (forall n0, n=n0) *)
+apply H' with (n0:=0).
+Qed.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4306a9673..a0bffd4fb 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -32,7 +32,6 @@ open Evd
let pr_lconstr c = quote (pr_lconstr c)
let pr_lconstr_env e c = quote (pr_lconstr_env e c)
-let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t)
let pr_db env i =
@@ -826,8 +825,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
else
mt()) ++ str "."
+let pr_ltype_using_barendregt_convention_env env c =
+ (* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
+ quote (pr_goal_concl_style_env env c)
+
let error_bad_ind_parameters env c n v1 v2 =
- let pc = pr_lconstr_env_at_top env c in
+ let pc = pr_ltype_using_barendregt_convention_env env c in
let pv1 = pr_lconstr_env env v1 in
let pv2 = pr_lconstr_env env v2 in
str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
@@ -985,7 +988,8 @@ let explain_pattern_matching_error env = function
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,c,(env',e)) ->
- str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
+ str "The abstracted term" ++ spc () ++
+ quote (pr_goal_concl_style_env env c) ++
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' Evd.empty e
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4f365ebcf..7f01f0307 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -407,7 +407,7 @@ let process_goal sigma g =
let env = Goal.V82.env sigma g in
let ccl =
let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
- string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
+ string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in
let process_hyp h_env d acc =
let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
(string_of_ppcmds (pr_var_decl h_env d)) :: acc in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 07:16:37 +0000