Rinv typo fix

[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 8b8d0361acd756e0eee840e1d9432822371e6bb8..07373374f72d580163b43fb4cc3978b4d7dcb483 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -126,7 +126,7 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "opp",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+          None, Some "cic:/Coq/Reals/Rdefinitions/Ropp.con"))
      :: List.map acic2cexpr args));;
 
 (* exists *)