]> matita.cs.unibo.it Git - helm.git/commitdiff
reindent
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 5 Feb 2008 16:12:33 +0000 (16:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 5 Feb 2008 16:12:33 +0000 (16:12 +0000)
helm/software/components/ng_kernel/nCic.ml

index 9221ba8d4bd0ab336cccc03779002dc7acc5bb69..2ff591ffc3052c4ea73e10ae4fe4a1c45c917b83 100644 (file)
@@ -43,12 +43,12 @@ and term =
  | Prod     of name * term * term                     (* binder, source, target          *)
  | Lambda   of name * term * term                     (* binder, source, target          *)
  | LetIn    of name * term * term * term              (* binder, type, term, body        *)
- | Const    of NUriManager.reference                         (* reference contains indtypeno/constrno *)
+ | Const    of NUriManager.reference                  (* reference contains indtypeno/constrno *)
  | Sort     of sort                                   (* sort                            *)
  | Implicit of implicit_annotation                    (* ... *)
- | MutCase  of NUriManager.reference *                      (* ind. reference,             *)
-    term * term *                                   (*  outtype, ind. term   *)
-    term list                                       (*  patterns             *)
+ | MutCase  of NUriManager.reference *                (* ind. reference,             *)
+    term * term *                                     (*  outtype, ind. term   *)
+    term list                                         (*  patterns             *)
 
 and obj =
  | Constant of term option * term