diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/tacinvutils.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 758071bac2..5797ec639b 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -263,7 +263,7 @@ let def_of_const t = (* nom d'une constante. Must be a constante. x*) let name_of_const t = match (kind_of_term t) with - Const cst -> Names.string_of_label (Names.label cst) + Const cst -> Names.string_of_label (Names.con_label cst) |_ -> assert false ;; |