documentation

CoqHott · Jul 11, 2023 · d2ed98d · d2ed98d
1 parent 9e4679f
commit d2ed98d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Decidability.v b/theories/Decidability.v
@@ -1,4 +1,4 @@
-(** * LogRel.Decidability: conversion and type-checking are decidable. *)
+(** * LogRel.Decidability: type-checking is decidable. *)
 From Equations Require Import Equations.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
 From LogRel Require Import Utils BasicAst Context Notations UntypedReduction DeclarativeTyping DeclarativeInstance GenericTyping NormalForms.