diff options
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/Setoid_ring_normalize.v | 2 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 2 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 2 |
3 files changed, 4 insertions, 2 deletions
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index 04e2aa16a..e49be3272 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -456,6 +456,8 @@ Proof. NewDestruct l;Trivial. Save. +(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *) + Lemma canonical_sum_merge_ok : (x,y:canonical_sum) (Aequiv (interp_cs (canonical_sum_merge x y)) (Aplus (interp_cs x) (interp_cs y))). diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 7908af7ec..10ca06b78 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -120,7 +120,7 @@ open Proof_type the constants are loaded in the environment *) let constant dir s = - let dir = "Coq"::"ring"::dir in + let dir = make_dirpath (List.map id_of_string ("Coq"::"ring"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index fad760cba..720c5a862 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -34,7 +34,7 @@ let mt_evd = Evd.empty let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com let constant dir s = - let dir = "Coq"::dir in + let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id |