diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /plugins/setoid_ring | |
| 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 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 4 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_ast.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_ast.mli | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 5e4c9214a..e9ce306e8 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -42,11 +42,11 @@ let pr_ring_mod = function | Ring_kind Abstract -> str "abstract" | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec |