aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--intf/constrexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 0d5542277f..647c01ff52 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -121,7 +121,7 @@ and recursion_order_expr =
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
-(** Anonymous defs allowed ?? *)
+(* Anonymous defs allowed ?? *)
and local_binder_expr =
| CLocalAssum of lname list * binder_kind * constr_expr
| CLocalDef of lname * constr_expr * constr_expr option