From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 13 Jun 2018 00:22:57 +0200
Subject: 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.
---
 interp/stdarg.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'interp/stdarg.mli')

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
-- 
cgit v1.2.3