diff options
| author | Maxime Dénès | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /interp/stdarg.mli | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'interp/stdarg.mli')
| -rw-r--r-- | interp/stdarg.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 4792cda081..5e5e43ed38 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -41,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type -val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_sort_family : (Sorts.family, unit, unit) genarg_type @@ -53,7 +53,7 @@ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_red_expr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type @@ -63,10 +63,10 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type -val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type -val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type val wit_redexpr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type |