From: Ferruccio Guidi Date: Sun, 21 Jun 2009 08:21:50 +0000 (+0000) Subject: - cicNotationPp: bugfix in record syntax X-Git-Tag: make_still_working~3829 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5da590cb272fbe6d8e00b781ac40422ae1b816a;p=helm.git - cicNotationPp: bugfix in record syntax - lambda-delta: version update --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 0d868c002..5eb6b64d2 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -294,10 +294,12 @@ let pp_fields pp_term fields = (List.map (fun (name,ty,coercion,arity) -> " " ^ name ^ - if coercion then (":" ^ - if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^ - pp_term ty) fields) - + (if coercion then + (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ") + else ": ") ^ + pp_term ty) + fields) + let pp_obj pp_term = function | Ast.Inductive (params, types) -> let pp_constructors constructors = diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index eb185c828..4b11d9af6 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,15 +1,14 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicPp.cmi: nReference.cmi nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo +nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo +nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -28,12 +27,12 @@ oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.cmi nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi -nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \ - nCicEnvironment.cmi nCic.cmo nCicPp.cmi -nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicEnvironment.cmi \ + nCic.cmo nCicPp.cmi +nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicEnvironment.cmx \ + nCic.cmx nCicPp.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicPp.cmi nCicEnvironment.cmi nCic.cmo nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ @@ -44,13 +43,13 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicUntrusted.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmo \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicUntrusted.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCic.cmo nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCic.cmx nCicUntrusted.cmi +nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ + nCicUntrusted.cmi nCicPp.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmo \ + nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ + nCicUntrusted.cmx nCicPp.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ + nCicLibrary.cmi diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 7a854657e..5fbb8fc60 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,15 +1,14 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicPp.cmi: nReference.cmi nCic.cmx nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx +nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmx nCicUntrusted.cmi: nCic.cmx +nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -28,12 +27,12 @@ oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.cmi nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi -nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \ - nCicEnvironment.cmi nCic.cmx nCicPp.cmi -nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicEnvironment.cmi \ + nCic.cmx nCicPp.cmi +nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicEnvironment.cmx \ + nCic.cmx nCicPp.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicPp.cmi nCicEnvironment.cmi nCic.cmx nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ @@ -44,13 +43,13 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicUntrusted.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmx \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicUntrusted.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCic.cmx nCicUntrusted.cmi +nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ + nCicUntrusted.cmi nCicPp.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmx \ + nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ + nCicUntrusted.cmx nCicPp.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ + nCicLibrary.cmi diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index de064c2d6..22bd5cbc7 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -46,7 +46,7 @@ let bag_error s msg = let main = try - let version_string = "Helena Checker 0.8.0 M - December 2008" in + let version_string = "Helena 0.8.0 M - June 2009" in let stage = ref 3 in let meta_file = ref None in let set_hierarchy s = @@ -57,7 +57,7 @@ try H.graph_of_string f s in let set_summary i = L.level := i in - let print_version () = L.warn version_string; exit 0 in + let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_stage i = stage := i in let close = function | None -> ()