aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 11:25:26 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:35:30 +0000
commit4d916a65ef1274160a2ee9726b88de5245e800e8 (patch)
treea631d6f40c49d129ea638588e815764358ff5d1c
parentfb4571bf487fd590d5e64ee33b27a7212a491466 (diff)
Change non-documentation comment from ocamldoc style
-rw-r--r--intf/constrexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 0d5542277..647c01ff5 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